feat: the Levi-Civita connection on a manifold

Mathlib.lean

@@ -4487,6 +4487,8 @@ public import Mathlib.Geometry.Manifold.SmoothEmbedding
 public import Mathlib.Geometry.Manifold.StructureGroupoid
 public import Mathlib.Geometry.Manifold.VectorBundle.Basic
 public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
 public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
 public import Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
 public import Mathlib.Geometry.Manifold.VectorBundle.Hom

Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean

@@ -790,6 +790,20 @@ theorem mfderiv_add (hf : MDiffAt f z) (hg : MDiffAt g z) :
       (by exact mfderiv% f z) + (by exact mfderiv% g z) :=
   (hf.hasMFDerivAt.add hg.hasMFDerivAt).mfderiv
 
+open NormedSpace in
+theorem fromTangentSpace_mfderiv_add (hf : MDiffAt f z) (hg : MDiffAt g z) :
+    (fromTangentSpace _).toContinuousLinearMap ∘L (mfderiv% (f + g) z)
+    = (fromTangentSpace _).toContinuousLinearMap ∘L (mfderiv% f z)
+    + (fromTangentSpace _).toContinuousLinearMap ∘L (mfderiv% g z) :=
+  (hf.hasMFDerivAt.add hg.hasMFDerivAt).mfderiv
+
+open NormedSpace in
+theorem fromTangentSpace_mfderiv_add_apply (hf : MDiffAt f z) (hg : MDiffAt g z)
+    (v : TangentSpace I x) :
+    fromTangentSpace _ (mfderiv% (f + g) z v)
+    = fromTangentSpace _ (mfderiv% f z v) + fromTangentSpace _ (mfderiv% g z v) :=
+  congr($(fromTangentSpace_mfderiv_add hf hg) v)
+
 section sum
 variable {ι : Type} {t : Finset ι} {f : ι → M → E'} {f' : ι → TangentSpace I z →L[𝕜] E'}