diff --git a/Mathlib.lean b/Mathlib.lean
index 05182daf14eb89..5386996fa63695 100644
--- a/Mathlib.lean
+++ b/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
diff --git a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean b/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
index 19a57d0c91d8d5..0f77ccf83303c0 100644
--- a/Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
+++ b/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'}
 
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/LeviCivita.lean b/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/LeviCivita.lean
new file mode 100644
index 00000000000000..afd52db1688b2b
--- /dev/null
+++ b/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/LeviCivita.lean
@@ -0,0 +1,868 @@
+/-
+Copyright (c) 2025 Michael Rothgang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot, Michael Rothgang, Heather Macbeth
+-/
+module
+
+public import Mathlib.Analysis.InnerProductSpace.Dual
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
+
+/-!
+# The Levi-Civita connection on a Riemannian manifold
+
+To be continued and polished!
+
+This file defines the Levi-Civita connection on a (finite-dimensional) Riemannian manifold `(M, g)`.
+connection `∇` on the tangent bundle of a Riemannian manifold `(M, g)` is called a
+*Levi-Civita connection* if and only if it is both compatible with the metric `g` and torsion-free.
+Any two such connections are equal (on differentiable vector fields), which is why one speaks of
+*the* Levi-Civita connection on `TM`.
+We construct a Levi-Civita connection and prove that is defines a compatible torsion-free
+connection.
+
+
+## Main definitions and results
+
+* `CovariantDerivative.IsLeviCivitaConnection`: a covariant derivative `∇` on `(M, g)` is a
+  Levi-Civita connection if and only if it is both torsion-free and compatible with `g`
+
+* `CovariantDerivative.IsLeviCivitaConnection.uniqueness`: a Levi-Civita connection on `(M, g)` is
+  uniquely determined on differentiable vector fields.
+
+* `CovariantDerivative.LeviCivitaConnection`: a choice of Levi-Civita connection on the tangent
+  bundle `TM` of a Riemannian manifold `(M, g)`: this is unique up to the value on
+  non-differentiable vector fields.
+  If you know the Levi-Civita connection already, you can use `IsLeviCivitaConnection` instead.
+* `CovariantDerivative.leviCivitaConnection_isLeviCivitaConnection`:
+  `LeviCivitaConnection` is a Levi-Civita connection (i.e., compatible and torsion-free)
+
+## Implementation notes
+* construction of LC using a tensoriality argument, and the musical isomorphism
+  (avoids the use of local frames and trivialisations)
+
+-/
+
+open Bundle FiberBundle Function NormedSpace
+open scoped Manifold ContDiff
+
+@[expose] public section -- TODO: think if we want to expose all definitions!
+
+-- TODO: revisit and fix this once the dust has settled
+set_option backward.isDefEq.respectTransparency false
+
+-- Let `(M, g)` be a `C^k` real manifold modeled on `(E, H)`, endowed with a Riemannian metric `g`.
+variable {n : WithTop ℕ∞}
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
+  {M : Type*} [EMetricSpace M] [ChartedSpace H M] [IsManifold I 2 M]
+  [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
+  {X X' X'' Y Y' Y'' Z Z' : Π x : M, TangentSpace I x}
+
+namespace CovariantDerivative
+
+-- Let `cov` be a covariant derivative on `TM`.
+-- TODO: include in cheat sheet!
+variable (cov : CovariantDerivative I E (TangentSpace I : M → Type _))
+
+/-- Local notation for a connection. Caution: `∇ Y, X` corresponds to `∇ₓ Y` in textbooks -/
+local notation "∇" Y "," X => fun (x:M) ↦ cov Y x (X x)
+
+variable [IsContMDiffRiemannianBundle I 1 E (fun (x : M) ↦ TangentSpace I x)]
+
+/-- A covariant derivative on a Riemannian bundle `TM` is called the **Levi-Civita connection**
+iff it is torsion-free and compatible with `g`.
+Note that the bundle metric on `TM` is implicitly hidden in this definition. See `TODO` for a
+version depending on a choice of Riemannian metric on `M`.
+-/
+def IsLeviCivitaConnection [FiniteDimensional ℝ E] : Prop :=
+  -- adaptation note: V used to be not required
+  cov.IsCompatible (V := (fun (x : M) ↦ TangentSpace I x)) ∧ cov.torsion = 0
+
+local notation "⟪" X ", " Y "⟫" => product X Y
+
+/- TODO: writing `hX.inner_bundle hY` or writing `by apply MDifferentiable.inner_bundle hX hY`
+yields an error
+synthesized type class instance is not definitionally equal to expression inferred by typing rules,
+synthesized
+  fun x ↦ instNormedAddCommGroupOfRiemannianBundle x
+inferred
+  fun b ↦ inst✝⁷
+Diagnose and fix this, and then replace the below by `MDifferentiable(At).inner_bundle! -/
+
+variable {I} in
+lemma _root_.MDifferentiable.inner_bundle' {X Y : Π x : M, TangentSpace I x}
+    (hX : MDiff (T% X)) (hY : MDiff (T% Y)) : MDiff ⟪X, Y⟫ :=
+  MDifferentiable.inner_bundle hX hY
+
+variable {I} in
+lemma _root_.MDifferentiableAt.inner_bundle' {x : M} {X Y : Π x : M, TangentSpace I x}
+    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) :
+    MDiffAt ⟪X, Y⟫ x :=
+  MDifferentiableAt.inner_bundle hX hY
+
+variable (X Y Z) in
+/-- The first term in the definition of the candidate Levi-Civita connection:
+`rhs_aux I X Y Z = X ⟨Y, Z⟩ = x ↦ d(⟨Y, Z⟩)_x (X x)`.
+
+This definition contains mild defeq abuse, which is invisible on paper:
+The function `⟨Y, Z⟩` maps `M` into `ℝ`, hence its differential at a point `x` maps `T_p M`
+to an element of the tangent space of `ℝ`. A summand `⟨Y, [X, Z]⟩`, however, yields an honest
+real number: Lean complains that these have different types.
+Fortunately, `ℝ` is defeq to its own tangent space; casting `rhs_aux` to the real numbers
+allows the addition to type-check. -/
+noncomputable abbrev rhs_aux : M → ℝ := fun x ↦ (mfderiv% ⟪Y, Z⟫ x (X x))
+
+section rhs_aux
+
+variable (Y Z) in
+omit [IsManifold I 2 M] in
+lemma rhs_aux_swap : rhs_aux I X Y Z = rhs_aux I X Z Y := by
+  ext x
+  simp only [rhs_aux]
+  congr 2
+  exact product_swap Z Y
+
+omit [IsManifold I 2 M] in
+variable (X X' Y Z) in
+lemma rhs_aux_addX : rhs_aux I (X + X') Y Z = rhs_aux I X Y Z + rhs_aux I X' Y Z := by
+  ext x
+  simp [rhs_aux]
+
+variable {x : M}
+
+variable (X) in
+@[simp]
+lemma rhs_aux_addY_apply (hY : MDiffAt (T% Y) x) (hY' : MDiffAt (T% Y') x) (hZ : MDiffAt (T% Z) x) :
+    rhs_aux I X (Y + Y') Z x = rhs_aux I X Y Z x + rhs_aux I X Y' Z x := by
+  simp only [rhs_aux]
+  rw [product_add_left, mfderiv_add (hY.inner_bundle' hZ) (hY'.inner_bundle' hZ)]
+  simp; congr
+
+variable (X) in
+lemma rhs_aux_addY (hY : MDiff (T% Y)) (hY' : MDiff (T% Y')) (hZ : MDiff (T% Z)) :
+    rhs_aux I X (Y + Y') Z = rhs_aux I X Y Z + rhs_aux I X Y' Z := by
+  ext x
+  exact rhs_aux_addY_apply I X (hY x) (hY' x) (hZ x)
+
+variable (X) in
+@[simp]
+lemma rhs_aux_addZ_apply (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) (hZ' : MDiffAt (T% Z') x) :
+  rhs_aux I X Y (Z + Z') x = rhs_aux I X Y Z x + rhs_aux I X Y Z' x := by
+  unfold rhs_aux
+  rw [product_add_right, mfderiv_add (hY.inner_bundle' hZ) (hY.inner_bundle' hZ')]; simp; congr
+
+variable (X) in
+lemma rhs_aux_addZ (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) (hZ' : MDiff (T% Z')) :
+    rhs_aux I X Y (Z + Z') = rhs_aux I X Y Z + rhs_aux I X Y Z' := by
+  ext x
+  exact rhs_aux_addZ_apply I X (hY x) (hZ x) (hZ' x)
+
+omit [IsManifold I 2 M] in
+variable (X Y Z) in
+lemma rhs_aux_smulX_apply (f : M → ℝ) (x) : rhs_aux I (f • X) Y Z x = f x * rhs_aux I X Y Z x := by
+  simp [rhs_aux]
+
+omit [IsManifold I 2 M] in
+variable (X Y Z) in
+lemma rhs_aux_smulX (f : M → ℝ) : rhs_aux I (f • X) Y Z = f * rhs_aux I X Y Z := by
+  ext x
+  exact rhs_aux_smulX_apply ..
+
+variable (X) in
+lemma rhs_aux_smulY_apply {f : M → ℝ}
+    (hf : MDiffAt f x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    letI A (x) := fromTangentSpace _ ((mfderiv% f x) (X x))
+    rhs_aux I X (f • Y) Z x = f x * rhs_aux I X Y Z x + A x * ⟪Y, Z⟫ x := by
+  rw [rhs_aux, product_smul_left, mfderiv_smul hf (hY.inner_bundle' hZ)]
+  rfl
+
+variable (X) in
+lemma rhs_aux_smulY {f : M → ℝ} (hf : MDiff f) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    letI A (x) := fromTangentSpace _ ((mfderiv% f x) (X x))
+    rhs_aux I X (f • Y) Z = f * rhs_aux I X Y Z + A * ⟪Y, Z⟫ := by
+  ext x
+  simp [rhs_aux_smulY_apply I X (hf x) (hY x) (hZ x)]
+
+variable (X) in
+lemma rhs_aux_smulY_const_apply {a : ℝ} (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    rhs_aux I X (a • Y) Z x = a * rhs_aux I X Y Z x := by
+  let f : M → ℝ := fun _ ↦ a
+  have h1 : rhs_aux I X (a • Y) Z x = rhs_aux I X (f • Y) Z x := by simp only [f]; congr
+  rw [h1, rhs_aux_smulY_apply I X mdifferentiableAt_const hY hZ]
+  simp [mfderiv_const]
+
+variable (X) in
+lemma rhs_aux_smulY_const {a : ℝ} (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    rhs_aux I X (a • Y) Z = a • rhs_aux I X Y Z := by
+  ext x
+  apply rhs_aux_smulY_const_apply I X (hY x) (hZ x)
+
+variable (X) in
+lemma rhs_aux_smulZ_apply {f : M → ℝ}
+    (hf : MDiffAt f x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    letI A (x) := fromTangentSpace _ ((mfderiv% f x) (X x))
+    rhs_aux I X Y (f • Z) x = f x * rhs_aux I X Y Z x + A x * ⟪Y, Z⟫ x := by
+  rw [rhs_aux_swap, rhs_aux_smulY_apply, rhs_aux_swap, product_swap]
+  exacts [hf, hZ, hY]
+
+variable (X) in
+lemma rhs_aux_smulZ {f : M → ℝ} (hf : MDiff f) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    letI A (x) := fromTangentSpace _ ((mfderiv% f x) (X x))
+    rhs_aux I X Y (f • Z) = f * rhs_aux I X Y Z + A * ⟪Y, Z⟫ := by
+  rw [rhs_aux_swap, rhs_aux_smulY, rhs_aux_swap, product_swap]
+  exacts [hf, hZ, hY]
+
+variable (X) in
+lemma rhs_aux_smulZ_const_apply {a : ℝ} (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    rhs_aux I X Y (a • Z) x = a * rhs_aux I X Y Z x := by
+  let f : M → ℝ := fun _ ↦ a
+  have h1 : rhs_aux I X Y (a • Z) x = rhs_aux I X Y (f • Z) x := by simp only [f]; congr
+  rw [h1, rhs_aux_smulZ_apply I X mdifferentiableAt_const hY hZ]
+  simp [mfderiv_const]
+
+variable (X) in
+lemma rhs_aux_smulZ_const {a : ℝ} (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    rhs_aux I X Y (a • Z) = a • rhs_aux I X Y Z := by
+  ext x
+  exact rhs_aux_smulZ_const_apply I X (hY x) (hZ x)
+
+end rhs_aux
+
+variable {x : M}
+
+variable (X Y Z) in
+/-- Auxiliary quantity used in the uniqueness proof of the Levi-Civita connection:
+If ∇ is a Levi-Civita connection on `TM`, then
+`2 ⟨∇ X Y, Z⟩ = leviCivitaRhs' I X Y Z` for all vector fields `Z`. -/
+noncomputable def leviCivitaRhs' : M → ℝ :=
+  rhs_aux I X Y Z + rhs_aux I Y Z X - rhs_aux I Z X Y
+  - ⟪Y ,(VectorField.mlieBracket I X Z)⟫
+  - ⟪Z, (VectorField.mlieBracket I Y X)⟫
+  + ⟪X, (VectorField.mlieBracket I Z Y)⟫
+
+variable (X Y Z) in
+/-- Auxiliary quantity used in the uniqueness proof of the Levi-Civita connection:
+If `∇` is a Levi-Civita connection on `TM`, then
+`⟨∇ X Y, Z⟩ = leviCivitaRhs I X Y Z` for all smooth vector fields `X`, `Y` and `Z`. -/
+noncomputable def leviCivitaRhs : M → ℝ := (1 / 2 : ℝ) • leviCivitaRhs' I X Y Z
+
+omit [IsManifold I 2 M] in
+lemma leviCivitaRhs_apply : leviCivitaRhs I X Y Z x = (1 / 2 : ℝ) • leviCivitaRhs' I X Y Z x :=
+  rfl
+
+section leviCivitaRhs
+
+@[simp]
+lemma leviCivitaRhs'_addX_apply [CompleteSpace E]
+    (hX : MDiffAt (T% X) x) (hX' : MDiffAt (T% X') x)
+    (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs' I (X + X') Y Z x =
+      leviCivitaRhs' I X Y Z x + leviCivitaRhs' I X' Y Z x := by
+  simp only [leviCivitaRhs', rhs_aux_addX, Pi.add_apply, Pi.sub_apply]
+  -- We have to rewrite back and forth: the Lie bracket is only additive at x,
+  -- as we are only asking for differentiability at x.
+  -- Fortunately, the `product_congr_right₂` lemma abstracts this very well.
+  rw [product_congr_right₂ (VectorField.mlieBracket_add_right (V := Y) hX hX'),
+    product_congr_right₂ (VectorField.mlieBracket_add_left (W := Z) hX hX'),
+    product_add_left_apply, rhs_aux_addY_apply, rhs_aux_addZ_apply] <;> try assumption
+  abel
+
+lemma leviCivitaRhs'_addX [CompleteSpace E]
+    (hX : MDiff (T% X)) (hX' : MDiff (T% X')) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    leviCivitaRhs' I (X + X') Y Z =
+      leviCivitaRhs' I X Y Z + leviCivitaRhs' I X' Y Z := by
+  ext x
+  simp [leviCivitaRhs'_addX_apply _ (hX x) (hX' x) (hY x) (hZ x)]
+
+lemma leviCivitaRhs_addX_apply [CompleteSpace E]
+    (hX : MDiffAt (T% X) x) (hX' : MDiffAt (T% X') x)
+    (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs I (X + X') Y Z x = leviCivitaRhs I X Y Z x + leviCivitaRhs I X' Y Z x := by
+  simp [leviCivitaRhs, leviCivitaRhs'_addX_apply I hX hX' hY hZ, left_distrib]
+
+lemma leviCivitaRhs_addX [CompleteSpace E]
+    (hX : MDiff (T% X)) (hX' : MDiff (T% X')) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    leviCivitaRhs I (X + X') Y Z = leviCivitaRhs I X Y Z + leviCivitaRhs I X' Y Z := by
+  ext x
+  simp [leviCivitaRhs_addX_apply _ (hX x) (hX' x) (hY x) (hZ x)]
+
+open VectorField NormedSpace
+
+variable {I} in
+lemma leviCivitaRhs'_smulX_apply [CompleteSpace E] {f : M → ℝ}
+    (hf : MDiffAt f x) (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs' I (f • X) Y Z x = f x • leviCivitaRhs' I X Y Z x := by
+  unfold leviCivitaRhs'
+  simp only [Pi.add_apply, Pi.sub_apply]
+  rw [rhs_aux_smulX, rhs_aux_smulY_apply, rhs_aux_smulZ_apply] <;> try assumption
+  -- TODO: add the right congr_right lemma to avoid the product_apply, ← product_apply dance!
+  simp only [product_apply, mlieBracket_smul_left (W := Z) hf hX,
+    mlieBracket_smul_right (V := Y) hf hX, inner_add_right]
+  -- Combining this line with the previous one fails.
+  simp only [← product_apply, neg_smul, inner_neg_right]
+  have h1 :
+      inner ℝ (Y x) ((fromTangentSpace _ (mfderiv% f x (Z x))) • X x) =
+        fromTangentSpace (f x) (mfderiv% f x (Z x)) * ⟪X, Y⟫ x := by
+    simp only [product]
+    rw [← real_inner_smul_left, real_inner_smul_right, real_inner_smul_left, real_inner_comm]
+  have h2 :
+      inner ℝ (Z x) (fromTangentSpace (f x) ((mfderiv% f x (Y x))) • X x) =
+        (fromTangentSpace (f x) (mfderiv% f x (Y x))) * ⟪Z, X⟫ x := by
+    simp only [product]
+    rw [← real_inner_smul_left, real_inner_smul_right, real_inner_smul_left]
+  rw [h1, h2]
+  --set dfY := fromTangentSpace (f x) ((mfderiv% f x (Y x)))--(mfderiv% f x) (Y x)
+  --set dfZ : ℝ := (mfderiv% f x) (Z x)
+  have h3 : ⟪f • X, mlieBracket I Z Y⟫ x = f x * ⟪X, mlieBracket I Z Y⟫ x := by
+    rw [product_apply, Pi.smul_apply', real_inner_smul_left]
+  have h4 : inner ℝ (Z x) (f x • mlieBracket I Y X x) = f x * ⟪Z, mlieBracket I Y X⟫ x := by
+    rw [product_apply, real_inner_smul_right]
+  rw [real_inner_smul_right (Y x), h3, h4]
+  -- Push all applications of `x` inwards, then it's indeed obvious.
+  simp
+  -- set A := ⟪Y, mlieBracket I X Z⟫ with hA
+  -- set B := ⟪Z, mlieBracket I X Y⟫
+  -- set C := ⟪X, mlieBracket I Z Y⟫
+  -- set R := dfZ * ⟪X, Y⟫ x with hR
+  -- set R' := dfY * ⟪Z, X⟫ x with hR'
+  -- set E := rhs_aux I X Y Z x
+  -- set F := rhs_aux I Y Z X x
+  -- set G := rhs_aux I Z X Y x
+  ring_nf
+
+variable {I} in
+lemma leviCivitaRhs_smulX_apply [CompleteSpace E] {f : M → ℝ}
+    (hf : MDiffAt f x) (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs I (f • X) Y Z x = f x • leviCivitaRhs I X Y Z x := by
+  simp only [leviCivitaRhs, one_div, Pi.smul_apply, smul_eq_mul]
+  simp_rw [leviCivitaRhs'_smulX_apply (I := I) hf hX hY hZ]
+  rw [← mul_assoc, mul_comm (f x), smul_eq_mul]
+  ring
+
+variable {I} in
+lemma leviCivitaRhs_smulX [CompleteSpace E] {f : M → ℝ}
+    (hf : MDiff f) (hX : MDiff (T% X)) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    leviCivitaRhs I (f • X) Y Z = f • leviCivitaRhs I X Y Z := by
+  ext x
+  exact leviCivitaRhs_smulX_apply (hf x) (hX x) (hY x) (hZ x)
+
+lemma leviCivitaRhs'_addY_apply [CompleteSpace E]
+    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x)
+    (hY' : MDiffAt (T% Y') x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs' I X (Y + Y') Z x = leviCivitaRhs' I X Y Z x + leviCivitaRhs' I X Y' Z x := by
+  simp only [leviCivitaRhs', Pi.add_apply, Pi.sub_apply, product_add_left_apply]
+  rw [rhs_aux_addX, rhs_aux_addY_apply, rhs_aux_addZ_apply] <;> try assumption
+  -- We have to rewrite back and forth: the Lie bracket is only additive at x,
+  -- as we are only asking for differentiability at x.
+  rw [product_congr_right₂ (mlieBracket_add_left (W := X) hY hY')]
+  rw [product_congr_right₂ (VectorField.mlieBracket_add_right (V := Z) hY hY')]
+  simp only [Pi.add_apply]
+  abel
+
+lemma leviCivitaRhs_addY_apply [CompleteSpace E]
+    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x)
+    (hY' : MDiffAt (T% Y') x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs I X (Y + Y') Z x = leviCivitaRhs I X Y Z x + leviCivitaRhs I X Y' Z x := by
+  simp [leviCivitaRhs, leviCivitaRhs'_addY_apply I hX hY hY' hZ, left_distrib]
+
+lemma leviCivitaRhs_addY [CompleteSpace E]
+    (hX : MDiff (T% X)) (hY : MDiff (T% Y)) (hY' : MDiff (T% Y')) (hZ : MDiff (T% Z)) :
+    leviCivitaRhs I X (Y + Y') Z = leviCivitaRhs I X Y Z + leviCivitaRhs I X Y' Z := by
+  ext x
+  simp [leviCivitaRhs_addY_apply I (hX x) (hY x) (hY' x) (hZ x)]
+
+variable {I} in
+lemma leviCivitaRhs'_smulY_const_apply [CompleteSpace E] {a : ℝ}
+    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs' I X (a • Y) Z x = a • leviCivitaRhs' I X Y Z x := by
+  simp only [leviCivitaRhs']
+  simp only [product_smul_const_left, Pi.add_apply, Pi.sub_apply, Pi.smul_apply]
+  rw [rhs_aux_smulY_const_apply I X hY hZ]
+  -- TODO: clean up this proof!
+  let f : M → ℝ := fun _ ↦ a
+  have : rhs_aux I (a • Y) Z X x = a • rhs_aux I Y Z X x := by
+    trans rhs_aux I (f • Y) Z X x
+    · rfl
+    rw [rhs_aux_smulX I Y (f := f) (Y := Z) (Z := X)]
+    rfl
+  rw [this, rhs_aux_smulZ_const_apply I _ hX hY]
+  -- is there a better abstraction for "Lie bracket conv mode"?
+  have : ⟪Z, mlieBracket I (a • Y) X⟫ x = a • ⟪Z, mlieBracket I Y X⟫ x := by
+    simp_rw [product_apply, mlieBracket_const_smul_left (W := X) hY, inner_smul_right_eq_smul]
+  rw [this]
+  have aux2 : ⟪X, mlieBracket I Z (a • Y)⟫ x = a • ⟪X, mlieBracket I Z Y⟫ x := by
+    simp_rw [product_apply,  mlieBracket_const_smul_right (V := Z) hY, inner_smul_right_eq_smul]
+  rw [aux2]
+  simp
+  ring
+
+variable {I} in
+lemma leviCivitaRhs_smulY_const_apply [CompleteSpace E] {a : ℝ}
+    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs I X (a • Y) Z x = a • leviCivitaRhs I X Y Z x := by
+  simp_rw [leviCivitaRhs, Pi.smul_apply]; rw [smul_comm]
+  congr
+  exact leviCivitaRhs'_smulY_const_apply hX hY hZ
+
+variable {I} in
+lemma leviCivitaRhs_smulY_const [CompleteSpace E] {a : ℝ}
+    (hX : MDiff (T% X)) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    leviCivitaRhs I X (a • Y) Z = a • leviCivitaRhs I X Y Z := by
+  ext x
+  exact leviCivitaRhs_smulY_const_apply (hX x) (hY x) (hZ x)
+
+lemma leviCivitaRhs'_smulY_apply [CompleteSpace E] {f : M → ℝ}
+    (hf : MDiffAt f x) (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs' I X (f • Y) Z x =
+      f x • leviCivitaRhs' I X Y Z x +
+        ((fromTangentSpace _).toFun <| mfderiv% f x (X x)) • 2 * ⟪Y, Z⟫ x := by
+  simp only [leviCivitaRhs']
+  simp_rw [rhs_aux_smulX I Y Z X f]
+  simp only [product_smul_left, Pi.add_apply, Pi.sub_apply, smul_eq_mul, Pi.mul_apply]
+  rw [rhs_aux_smulY_apply I X hf hY hZ, rhs_aux_smulZ_apply I Z hf hX hY]
+  -- TODO: is there a better abstraction for this kind of "Lie bracket conv mode"?
+  have h1 : ⟪Z, mlieBracket I (f • Y) X⟫ x =
+      - (fromTangentSpace _).toFun (((mfderiv% f x) (X x))) • ⟪Z, Y⟫ x
+      + f x • ⟪Z, mlieBracket I Y X⟫ x := by
+    simp_rw [product_apply, mlieBracket_smul_left (W := X) hf hY, inner_add_right]
+    congr
+    · simp only [neg_smul, inner_neg_right, fromTangentSpace, AddHom.toFun_eq_coe, AddHom.coe_mk,
+        smul_eq_mul, neg_mul, neg_inj]
+      rw [real_inner_smul_right]
+      rfl
+    · rw [inner_smul_right_eq_smul]
+  have h2 : ⟪X, mlieBracket I Z (f • Y)⟫ x =
+      (fromTangentSpace _).toFun (((mfderiv% f x) (Z x))) • ⟪X, Y⟫ x
+        + f x • ⟪X, mlieBracket I Z Y⟫ x := by
+    simp_rw [product_apply, mlieBracket_smul_right (V := Z) hf hY, inner_add_right]
+    congr
+    · simp only [fromTangentSpace, AddHom.toFun_eq_coe, AddHom.coe_mk, smul_eq_mul]
+      rw [real_inner_smul_right]
+      rfl
+    · rw [inner_smul_right_eq_smul]
+  rw [h1, h2, product_swap Y Z]
+  set A := rhs_aux I X Y Z x
+  set B := rhs_aux I Y Z X x
+  set C := rhs_aux I Z X Y x
+  set D := ⟪Y, mlieBracket I X Z⟫ x
+  set E := ⟪Z, mlieBracket I Y X⟫ x
+  set F := ⟪X, mlieBracket I Z Y⟫ x
+  set G1 := ⟪Y, Z⟫ x
+  set G2 := ⟪X, Y⟫ x
+  set dfx := (mfderiv I 𝓘(ℝ, ℝ) f x)
+  set H := (fromTangentSpace (f x)) (dfx (X x)) with H_eq
+  set K := (fromTangentSpace (f x)) (dfx (Z x)) with K_eq
+  change f x * A + (fromTangentSpace _).toFun (dfx (X x)) * G1 + f x * B
+    - (f x * C + (fromTangentSpace _).toFun (dfx (Z x)) * G2)
+    - f x * D - (-H * G1 + f x * E) + (K * G2 + f x * F) = _
+  dsimp
+  rw [← H_eq, ← K_eq]
+  ring
+
+lemma leviCivitaRhs_smulY_apply [CompleteSpace E] {f : M → ℝ}
+    (hf : MDiffAt f x) (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs I X (f • Y) Z x =
+      f x • leviCivitaRhs I X Y Z x
+        + ((fromTangentSpace _).toFun <| mfderiv% f x (X x)) • ⟪Y, Z⟫ x := by
+  simp only [leviCivitaRhs, Pi.smul_apply, leviCivitaRhs'_smulY_apply I hf hX hY hZ]
+  rw [smul_add, smul_comm]
+  congr 1
+  rw [← smul_eq_mul]
+  dsimp
+  field_simp
+
+lemma leviCivitaRhs'_addZ_apply [CompleteSpace E]
+    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x)
+    (hZ : MDiffAt (T% Z) x) (hZ' : MDiffAt (T% Z') x) :
+    leviCivitaRhs' I X Y (Z + Z') x =
+      leviCivitaRhs' I X Y Z x + leviCivitaRhs' I X Y Z' x := by
+  simp only [leviCivitaRhs', rhs_aux_addX, Pi.add_apply, Pi.sub_apply, product_add_left_apply]
+  rw [product_congr_right₂ (VectorField.mlieBracket_add_right (V := X) hZ hZ'),
+    product_congr_right₂ (VectorField.mlieBracket_add_left (W := Y) hZ hZ'),
+    rhs_aux_addY_apply, rhs_aux_addZ_apply] <;> try assumption
+  abel
+
+lemma leviCivitaRhs'_addZ [CompleteSpace E]
+    (hX : MDiff (T% X)) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) (hZ' : MDiff (T% Z')) :
+    leviCivitaRhs' I X Y (Z + Z') =
+      leviCivitaRhs' I X Y Z + leviCivitaRhs' I X Y Z' := by
+  ext x
+  exact leviCivitaRhs'_addZ_apply I (hX x) (hY x) (hZ x) (hZ' x)
+
+lemma leviCivitaRhs_addZ_apply [CompleteSpace E]
+    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x)
+    (hZ : MDiffAt (T% Z) x) (hZ' : MDiffAt (T% Z') x) :
+    leviCivitaRhs I X Y (Z + Z') x = leviCivitaRhs I X Y Z x + leviCivitaRhs I X Y Z' x := by
+  simp [leviCivitaRhs, leviCivitaRhs'_addZ_apply I hX hY hZ hZ', left_distrib]
+
+lemma leviCivitaRhs_addZ [CompleteSpace E]
+    (hX : MDiff (T% X)) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) (hZ' : MDiff (T% Z')) :
+    leviCivitaRhs I X Y (Z + Z') = leviCivitaRhs I X Y Z + leviCivitaRhs I X Y Z' := by
+  ext x
+  exact leviCivitaRhs_addZ_apply I (hX x) (hY x) (hZ x) (hZ' x)
+
+lemma leviCivitaRhs'_smulZ_apply [CompleteSpace E] {f : M → ℝ}
+    (hf : MDiffAt f x) (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs' I X Y (f • Z) x = f x • leviCivitaRhs' I X Y Z x := by
+  simp only [leviCivitaRhs', rhs_aux_smulX, Pi.add_apply, Pi.sub_apply]
+  rw [rhs_aux_smulY_apply _ _ hf hZ hX, rhs_aux_smulZ_apply _ _ hf hY hZ]
+  -- Apply the product rule for the lie bracket.
+  -- Let's encapsulate the going into the product and back out again.
+  have h1 : ⟪Y, mlieBracket I X (f • Z)⟫ x =
+      f x • ⟪Y, mlieBracket I X Z⟫ x + ⟪Y, fromTangentSpace _ (mfderiv% f x (X x)) • Z⟫ x := by
+    rw [product_apply, VectorField.mlieBracket_smul_right hf hZ, inner_add_right, add_comm,
+      inner_smul_right]
+    congr
+  have h2 : letI dfY := fromTangentSpace _ ((mfderiv% f x) (Y x));
+      ⟪X, mlieBracket I (f • Z) Y⟫ x = - dfY • ⟪X, Z⟫ x + f x • ⟪X, mlieBracket I Z Y⟫ x := by
+    rw [product_apply, VectorField.mlieBracket_smul_left hf hZ, inner_add_right, inner_smul_right,
+      inner_smul_right]
+    congr
+  rw [h1, h2, product_smul_left, product_swap X Z]
+  erw [product_smul_right]
+  simp
+  -- set A := rhs_aux I X Y Z x
+  -- set B := rhs_aux I Y Z X x
+  -- set C := rhs_aux I Z X Y x
+  -- set D := ⟪Y, mlieBracket I X Z⟫ x
+  -- set E := ⟪Z, mlieBracket I Y X⟫ x with E_eq
+  -- set F := ⟪X, mlieBracket I Z Y⟫ x
+  -- letI dfX : ℝ := (mfderiv I 𝓘(ℝ, ℝ) f x) (X x)
+  -- set G := dfX * ⟪Y, Z⟫ x
+  -- letI dfY : ℝ := (mfderiv I 𝓘(ℝ, ℝ) f x) (Y x)
+  -- set H := dfY * ⟪X, Z⟫ x
+  ring
+
+lemma leviCivitaRhs'_smulZ [CompleteSpace E] {f : M → ℝ}
+    (hf : MDiff f) (hX : MDiff (T% X)) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    leviCivitaRhs' I X Y (f • Z) = f • leviCivitaRhs' I X Y Z := by
+  ext x
+  exact leviCivitaRhs'_smulZ_apply I (hf x) (hX x) (hY x) (hZ x)
+
+lemma leviCivitaRhs_smulZ [CompleteSpace E] {f : M → ℝ}
+    (hf : MDiff f) (hX : MDiff (T% X)) (hY : MDiff (T% Y)) (hZ : MDiff (T% Z)) :
+    leviCivitaRhs I X Y (f • Z) = f • leviCivitaRhs I X Y Z := by
+  simp only [leviCivitaRhs]
+  rw [smul_comm, leviCivitaRhs'_smulZ I hf hX hY hZ]
+
+lemma leviCivitaRhs_smulZ_apply [CompleteSpace E] {f : M → ℝ}
+    (hf : MDiffAt f x) (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    leviCivitaRhs I X Y (f • Z) x = f x * leviCivitaRhs I X Y Z x := by
+  simp [leviCivitaRhs, leviCivitaRhs'_smulZ_apply I hf hX hY hZ]
+  ring
+
+end leviCivitaRhs
+
+variable [FiniteDimensional ℝ E] in
+lemma aux (h : cov.IsLeviCivitaConnection) {x : M}
+    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) : rhs_aux I X Y Z x =
+    ⟪∇ Y, X, Z⟫ x + ⟪Y, ∇ X, Z⟫ x + ⟪Y, VectorField.mlieBracket I X Z⟫ x := by
+  trans ⟪∇ Y, X, Z⟫ x + ⟪Y, ∇ Z, X⟫ x
+  · -- adaptation note: the following line fails with an error
+    /- synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
+      fun x ↦ instNormedAddCommGroupOfRiemannianBundleOfIsTopologicalAddGroupOfContinuousConstSMulReal x
+    inferred
+      fun b ↦ inst✝⁸ -/
+    sorry -- exact cov.isCompatible_iff.mp h.1 hX hY hZ
+  · simp [← cov.torsion_eq_zero_iff.mp h.2 hX hZ, product, inner_sub_right]
+
+variable {cov} in
+/-- Auxiliary lemma towards the uniquness of the Levi-Civita connection: expressing the term
+⟨∇ X Y, Z⟩ for all differentiable vector fields X, Y and Z, without reference to ∇. -/
+lemma IsLeviCivitaConnection.eq_leviCivitaRhs [FiniteDimensional ℝ E]
+    (h : cov.IsLeviCivitaConnection)
+    {x : M} (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) (hZ : MDiffAt (T% Z) x) :
+    ⟪∇ Y, X, Z⟫ x = leviCivitaRhs I X Y Z x := by
+  unfold leviCivitaRhs leviCivitaRhs'
+  have eq1 := aux I cov h hX hY hZ
+  have eq2 := aux I cov h hY hZ hX
+  have eq3 := aux I cov h hZ hX hY
+  simp [real_inner_comm, smul_eq_mul] at *
+  linear_combination - (eq1 + eq2 - eq3) / 2
+
+section
+
+omit [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E (TangentSpace I (M := M))] in
+variable {I} in
+lemma congr_of_forall_product_apply [FiniteDimensional ℝ E] {Y Y' : TangentSpace I x}
+    (h : ∀ Z : TangentSpace I x, inner ℝ Y Z = inner ℝ Y' Z) : Y = Y' := by
+  have : FiniteDimensional ℝ (TangentSpace I x) := inferInstanceAs (FiniteDimensional ℝ E)
+  have : CompleteSpace (TangentSpace I x) := FiniteDimensional.complete ℝ _
+  set Φ := InnerProductSpace.toDual ℝ (TangentSpace I x)
+  apply Φ.injective
+  ext Z₀
+  simpa [Φ, product] using h Z₀
+
+omit [IsContMDiffRiemannianBundle I 1 E (TangentSpace I (M := M))] in
+variable {I} in
+/-- If two vector fields `X` and `X'` on `M` satisfy the relation `⟨X, Z⟩ = ⟨X', Z⟩` for all
+vector fields `Z`, then `X = X'`. XXX up to differentiability? -/
+-- TODO: is this true if E is infinite-dimensional? trace the origin of the `Fintype` assumptions!
+lemma congr_of_forall_product [FiniteDimensional ℝ E]
+    (h : ∀ Z : Π x : M, TangentSpace I x, ⟪X, Z⟫ = ⟪X', Z⟫) : X = X' := by
+  ext1 x
+  apply congr_of_forall_product_apply
+  intro Z₀
+  simpa [product] using congr($(h (extend E Z₀)) x)
+
+/-- The Levi-Civita connection on `(M, g)` is uniquely determined,
+at least on differentiable vector fields. -/
+-- (probably not everywhere, as addition rules apply only for differentiable vector fields?)
+theorem IsLeviCivitaConnection.uniqueness [FiniteDimensional ℝ E]
+    {cov cov' : CovariantDerivative I E (TangentSpace I : M → Type _)}
+    (hcov : cov.IsLeviCivitaConnection) (hcov' : cov'.IsLeviCivitaConnection)
+    {X Y : Π x : M, TangentSpace I x} {x : M}
+    (hX : MDiffAt (T% X) x) (hY : MDiffAt (T% Y) x) :
+    cov Y x (X x) = cov' Y x (X x) := by
+  have : FiniteDimensional ℝ (TangentSpace I x) := inferInstanceAs (FiniteDimensional ℝ E)
+  have : CompleteSpace (TangentSpace I x) := FiniteDimensional.complete ℝ _
+  set Φ := InnerProductSpace.toDual ℝ (TangentSpace I x)
+  apply Φ.injective
+  ext Z₀
+  let Z := extend E Z₀
+  have hZ := mdifferentiableAt_extend I E Z₀
+  suffices inner ℝ (cov Y x (X x)) (Z x) = inner ℝ (cov' Y x (X x)) (Z x) by simpa [Φ, Z]
+  trans leviCivitaRhs I X Y Z x
+  · rw [← hcov.eq_leviCivitaRhs I hX hY hZ]
+  · rw [← hcov'.eq_leviCivitaRhs I hX hY hZ]
+
+open Classical in
+noncomputable def lcAux₀' (Y : Π x : M, TangentSpace I x) (x : M)
+    (X Z : Π x : M, TangentSpace I x) :=
+  if MDiffAt (T% X) x then if MDiffAt (T% Z) x then
+    leviCivitaRhs I X Y Z
+  else 0 else 0
+
+theorem leviCivitaRhs_tensorial₁ [FiniteDimensional ℝ E]
+    {Y : Π x : M, TangentSpace I x} (x : M) (hY : MDiffAt (T% Y) x) (Z : Π x, TangentSpace I x) :
+    TensorialAt I E (lcAux₀' I Y x · Z x) x where
+  smul hf hX := by
+    dsimp [lcAux₀']
+    rw [if_pos hX, if_pos]
+    · split_ifs with hZ
+      · exact leviCivitaRhs_smulX_apply hf hX hY hZ
+      · simp
+    · exact hf.smul_section hX
+  add hX₁ hX₂ := by
+    dsimp [lcAux₀']
+    rw [if_pos hX₁, if_pos hX₂, if_pos]
+    · split_ifs with hZ
+      · exact leviCivitaRhs_addX_apply I hX₁ hX₂ hY hZ
+      · simp
+    · exact mdifferentiableAt_add_section hX₁ hX₂
+
+theorem leviCivitaRhs_tensorial₂ [FiniteDimensional ℝ E]
+    {Y : Π x : M, TangentSpace I x} (x : M) (hY : MDiffAt (T% Y) x) (X : Π x, TangentSpace I x)
+    (hX : MDiffAt (T% X) x) :
+    TensorialAt I E (lcAux₀' I Y x X · x) x where
+  smul hf hZ := by
+    dsimp [lcAux₀']
+    rw [if_pos hX, if_pos hZ, if_pos, if_pos hX]
+    · exact leviCivitaRhs_smulZ_apply I hf hX hY hZ
+    · exact hf.smul_section hZ
+  add hZ₁ hZ₂ := by
+    dsimp [lcAux₀']
+    rw [if_pos hZ₁, if_pos hZ₂, if_pos hX, if_pos, if_pos hX, if_pos hX]
+    · exact leviCivitaRhs_addZ_apply I hX hY hZ₁ hZ₂
+    · exact mdifferentiableAt_add_section hZ₁ hZ₂
+
+open Classical in
+noncomputable def lcAux₀ [FiniteDimensional ℝ E]
+    {Y : Π x : M, TangentSpace I x} (x : M) (hY : MDiffAt (T% Y) x) :
+    TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ :=
+  TensorialAt.mkHom₂ _ (x := x)
+    (fun Z _ ↦ leviCivitaRhs_tensorial₁ _ _ hY Z)
+    (fun X hX ↦ leviCivitaRhs_tensorial₂ _ _ hY X hX)
+
+theorem lcAux₀_apply [FiniteDimensional ℝ E] {x : M}
+    {X : Π x : M, TangentSpace I x} (hX : MDiffAt (T% X) x)
+    {Y : Π x : M, TangentSpace I x} (hY : MDiffAt (T% Y) x)
+    {Z : Π x : M, TangentSpace I x} (hZ : MDiffAt (T% Z) x) :
+    lcAux₀ I x hY (X x) (Z x) = leviCivitaRhs I X Y Z x := by
+  unfold lcAux₀
+  rw [TensorialAt.mkHom₂_apply _ _ hX hZ, lcAux₀', if_pos hX, if_pos hZ]
+
+noncomputable def lcAux₁ [FiniteDimensional ℝ E]
+    {Y : Π x : M, TangentSpace I x} (x : M) (hY : MDiffAt (T% Y) x) :
+    TangentSpace I x →L[ℝ] TangentSpace I x :=
+  -- use the musical isomorphism to produce a candidate ∇ Y as a (1,1)-tensor
+  -- (rather than a 2-tensor)
+  have : FiniteDimensional ℝ (TangentSpace I x) := inferInstanceAs (FiniteDimensional ℝ E)
+  have : CompleteSpace (TangentSpace I x) := FiniteDimensional.complete ℝ _
+  (InnerProductSpace.toDual ℝ _).symm.toContinuousLinearEquiv.toContinuousLinearMap ∘L
+    (lcAux₀ I x hY)
+
+theorem lcAux₁_apply [FiniteDimensional ℝ E] {x : M}
+    {X : Π x : M, TangentSpace I x} (hX : MDiffAt (T% X) x)
+    {Y : Π x : M, TangentSpace I x} (hY : MDiffAt (T% Y) x)
+    {Z : Π x : M, TangentSpace I x} (hZ : MDiffAt (T% Z) x) :
+    inner ℝ (lcAux₁ I x hY (X x)) (Z x) = leviCivitaRhs I X Y Z x := by
+  simpa [lcAux₁] using lcAux₀_apply I hX hY hZ
+
+open Classical in
+noncomputable def lcAux [FiniteDimensional ℝ E]
+    (Y : Π x : M, TangentSpace I x) (x : M) :
+    TangentSpace I x →L[ℝ] TangentSpace I x :=
+  if hY : MDiffAt (T% Y) x then lcAux₁ I x hY else 0
+
+theorem lcAux_apply [FiniteDimensional ℝ E] {x : M}
+    {X : Π x : M, TangentSpace I x} (hX : MDiffAt (T% X) x)
+    {Y : Π x : M, TangentSpace I x} (hY : MDiffAt (T% Y) x)
+    {Z : Π x : M, TangentSpace I x} (hZ : MDiffAt (T% Z) x) :
+    inner ℝ (lcAux I Y x (X x)) (Z x) = leviCivitaRhs I X Y Z x := by
+  unfold lcAux
+  rw [dif_pos hY]
+  simpa [lcAux] using lcAux₁_apply I hX hY hZ
+
+lemma isCovariantDerivativeOn_lcAux [FiniteDimensional ℝ E] :
+    IsCovariantDerivativeOn E (lcAux I (M := M)) where
+  add {Y Y'} x hY hY' _ := by
+    unfold lcAux
+    rw [dif_pos hY, dif_pos hY', dif_pos (mdifferentiableAt_add_section hY hY')]
+    unfold lcAux₁
+    dsimp
+    rw [← ContinuousLinearMap.comp_add]
+    congr! 1
+    simp only [lcAux₀]
+    ext X₀ Y₀
+    simp only [TensorialAt.mkHom₂_apply_eq_extend, ContinuousLinearMap.add_apply, lcAux₀']
+    rw [if_pos, if_pos, if_pos, if_pos, if_pos, if_pos]
+    · exact leviCivitaRhs_addY_apply _ (FiberBundle.mdifferentiableAt_extend ..)
+        hY hY' (FiberBundle.mdifferentiableAt_extend ..)
+    · exact FiberBundle.mdifferentiableAt_extend ..
+    · exact FiberBundle.mdifferentiableAt_extend ..
+    · exact FiberBundle.mdifferentiableAt_extend ..
+    · exact FiberBundle.mdifferentiableAt_extend ..
+    · exact FiberBundle.mdifferentiableAt_extend ..
+    · exact FiberBundle.mdifferentiableAt_extend ..
+  leibniz {Y f x} hY hf _ := by
+    dsimp [lcAux]
+    rw [dif_pos hY, dif_pos]
+    · unfold lcAux₁
+      dsimp
+      rw [← ContinuousLinearMap.comp_smul]
+      have : FiniteDimensional ℝ (TangentSpace I x) := inferInstanceAs (FiniteDimensional ℝ E)
+      have : CompleteSpace (TangentSpace I x) := FiniteDimensional.complete ℝ _
+      set Φ := InnerProductSpace.toDual ℝ (TangentSpace I x)
+      ext X₀
+      apply Φ.injective
+      simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe,
+        LinearIsometryEquiv.coe_symm_toContinuousLinearEquiv, comp_apply,
+        LinearIsometryEquiv.apply_symm_apply, ContinuousLinearMap.comp_smulₛₗ, RingHom.id_apply,
+        ContinuousLinearMap.add_apply, ContinuousLinearMap.coe_smul', Pi.smul_apply,
+        map_add, map_smul]
+      ext Z₀
+      simp only [lcAux₀, lcAux₀', TensorialAt.mkHom₂_apply_eq_extend,
+        ContinuousLinearMap.add_apply, ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul]
+      rw [if_pos, if_pos, if_pos, if_pos]
+      · convert leviCivitaRhs_smulY_apply I hf (FiberBundle.mdifferentiableAt_extend I E X₀) hY
+          (FiberBundle.mdifferentiableAt_extend I E Z₀)
+        simp [Φ, product]
+      · exact FiberBundle.mdifferentiableAt_extend ..
+      · exact FiberBundle.mdifferentiableAt_extend ..
+      · exact FiberBundle.mdifferentiableAt_extend ..
+      · exact FiberBundle.mdifferentiableAt_extend ..
+    exact MDifferentiableAt.smul_section hf hY
+
+end
+
+-- TODO: make g part of the notation!
+variable (M) in
+/-- A choice of Levi-Civita connection on the tangent bundle `TM` of a Riemannian manifold `(M, g)`:
+this is unique up to the value on non-differentiable vector fields.
+If you know the Levi-Civita connection already, you can use `IsLeviCivitaConnection` instead. -/
+noncomputable def LeviCivitaConnection [FiniteDimensional ℝ E] :
+    CovariantDerivative I E (TangentSpace I : M → Type _) where
+  toFun := lcAux I
+  isCovariantDerivativeOnUniv := isCovariantDerivativeOn_lcAux I
+
+theorem leviCivitaConnection_apply [FiniteDimensional ℝ E] {x : M}
+    {X : Π x : M, TangentSpace I x} (hX : MDiffAt (T% X) x)
+    {Y : Π x : M, TangentSpace I x} (hY : MDiffAt (T% Y) x)
+    {Z : Π x : M, TangentSpace I x} (hZ : MDiffAt (T% Z) x) :
+    inner ℝ (LeviCivitaConnection I M Y x (X x)) (Z x) = leviCivitaRhs I X Y Z x :=
+  lcAux_apply _ hX hY hZ
+
+-- Side computation for `leviCivitaConnection_isCompatible`.
+omit [IsManifold I 2 M] in
+lemma leviCivitaConnection_isCompatible_aux
+    {x : M} {X Y Z : (x : M) → TangentSpace I x} :
+    leviCivitaRhs I X Y Z x + leviCivitaRhs I X Z Y x =
+    fromTangentSpace _ ((mfderiv% fun x ↦ inner ℝ (Y x) (Z x)) x (X x)) := by
+  simp only [leviCivitaRhs, Pi.smul_apply, ← smul_add,  leviCivitaRhs']
+  -- Normalise the expressions by swapping arguments for rhs_aux and mlieBracket,
+  -- until the swappable arguments are in order X < Y < Z.
+  rw [rhs_aux_swap I Z Y, rhs_aux_swap I Z X, rhs_aux_swap I Y X,
+    VectorField.mlieBracket_swap (V := Z) (W := Y),
+    VectorField.mlieBracket_swap (V := Y) (W := X),
+    VectorField.mlieBracket_swap (V := Z) (W := X)]
+  -- Observe that the right hand side is rhx_aux X Y Z; then we just need to simplify and rearrange.
+  trans 1 / 2 * (rhs_aux I X Y Z x + rhs_aux I X Y Z x)
+  · simp
+    abel
+  · rw [← two_mul, ← mul_assoc, one_div, inv_mul_cancel₀ (by simp), one_mul]
+    rfl
+
+-- Why is everything so slow?
+lemma leviCivitaConnection_isCompatible [FiniteDimensional ℝ E] :
+    -- adaptation note: specifying V used to be not necessary
+    (LeviCivitaConnection I M).IsCompatible (V := (fun (x : M) ↦ TangentSpace I x)) := by
+  rw [isCompatible_iff]
+  intro x X Y Z hX hY hZ
+  symm
+  unfold product
+  dsimp
+  rw [leviCivitaConnection_apply I hX hY hZ]
+  have : inner ℝ (Y x) (((LeviCivitaConnection I M) Z x) (X x)) =
+      inner ℝ (((LeviCivitaConnection I M) Z x) (X x)) (Y x) := by
+    rw [real_inner_comm]
+  -- TODO: why does the following line not work, but `rw [this]` does?
+  --rw [real_inner_comm]
+  rw [this]
+  have : inner ℝ (((LeviCivitaConnection I M) Z x) (X x)) (Y x) = leviCivitaRhs I X Z Y x := by
+    rw [leviCivitaConnection_apply I hX hZ hY]
+  rw [leviCivitaConnection_apply I hX hZ hY, leviCivitaConnection_isCompatible_aux]
+
+lemma leviCivitaConnection_torsion_eq_zero [FiniteDimensional ℝ E] :
+    (LeviCivitaConnection I M).torsion = 0 := by
+  have a := (LeviCivitaConnection I M).isCovariantDerivativeOnUniv
+  rw [CovariantDerivative.torsion_eq_zero_iff]
+  intro X Y x hX hY
+  apply congr_of_forall_product_apply
+  intro Z
+  trans (inner ℝ (((LeviCivitaConnection I M) Y x) (X x)) Z) -
+    (inner ℝ (((LeviCivitaConnection I M) X x) (Y x)) Z)
+  · apply inner_sub_left
+  have hZ' : extend E Z x = Z := extend_apply_self E Z
+  rw [← hZ']
+  rw [leviCivitaConnection_apply I hY hX (mdifferentiableAt_extend ..)]
+  rw [leviCivitaConnection_apply I hX hY (mdifferentiableAt_extend ..)]
+  simp only [leviCivitaRhs_apply]
+  -- XXX: should there be leviCivitaRhs'_apply?
+  simp only [leviCivitaRhs', Pi.add_apply, Pi.sub_apply, product_apply]
+  simp only [VectorField.mlieBracket_swap (V := Y) (W := X)]
+  simp only [Pi.neg_apply, inner_neg_right, sub_neg_eq_add]
+  set C := inner ℝ Z (VectorField.mlieBracket I X Y x)
+  set Z' := extend E Z
+  simp only [VectorField.mlieBracket_swap (V := Z') (W := X)]
+  simp only [VectorField.mlieBracket_swap (V := Z') (W := Y)]
+  simp only [Pi.neg_apply, inner_neg_right]
+  rw [rhs_aux_swap (Y := Z'), rhs_aux_swap (Y := Z'), rhs_aux_swap (X := Z')]
+  rw [real_inner_comm (Z' x) (VectorField.mlieBracket I X Y x)]
+  -- set A := inner ℝ (Z' x) (VectorField.mlieBracket I X Y x)
+  -- set B := inner ℝ (Y x) (VectorField.mlieBracket I X Z' x)
+  -- set C := inner ℝ (X x) (VectorField.mlieBracket I Y Z' x)
+  -- set D := rhs_aux I X Y Z' x
+  -- set E := rhs_aux I Y X Z' x
+  -- set F := rhs_aux I Z' X Y x
+  match_scalars <;> simp
+  norm_num
+
+/-- `LeviCivitaConnection` is a Levi-Civita connection (i.e., compatible and torsion-free) -/
+lemma leviCivitaConnection_isLeviCivitaConnection [FiniteDimensional ℝ E] :
+    (LeviCivitaConnection I M).IsLeviCivitaConnection :=
+  ⟨leviCivitaConnection_isCompatible I, leviCivitaConnection_torsion_eq_zero I⟩
+
+end CovariantDerivative
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean b/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean
new file mode 100644
index 00000000000000..300fc559a33d70
--- /dev/null
+++ b/Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Metric.lean
@@ -0,0 +1,278 @@
+/-
+Copyright (c) 2025 Michael Rothgang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot, Michael Rothgang, Heather Macbeth
+-/
+module
+
+public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
+public import Mathlib.Geometry.Manifold.VectorBundle.Riemannian
+public import Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
+
+/-! # Metric connections
+
+This file defines connections on a Riemannian vector bundle which are compatible with the ambient
+metric. A bundled connection `∇` on a Riemannian vector bundle `(V, g)` is compatible with the
+metric `g` if and only if the differentiated metric tensor `∇ g` (defined by
+`(X, σ, τ) ↦ ∇_X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)`) vanishes on all differentiable vector fields
+`X` and differentiable sections `σ`, `τ`.
+
+## Main definitions and results
+
+* `CovariantDerivative.compatibilityTensor`: the tensor
+  `(X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)` defining when a connection `∇` on a Riemannian
+  vector bundle `(V, g)` is compatible with the metric `g`.
+* `CovariantDerivative.compatibilityTensor_apply` and
+  `CovariantDerivative.compatibilityTensor_apply` give formulas for applying the compatibility
+  tensor at `x` to vector fields and sections which are differentiable at `x`,
+  resp. to extensions of tangent vectors and sections at `x` to differentiable vector fields and
+  sections near `x`.
+* `CovariantDerivative.IsCompatible`: predicate for a connection to be metric, namely that
+  `∇` is metric iff its `compatibilityTensor` vanishes
+
+## TODO
+
+* When Mathlib has a notion of parallel transport, prove the equivalence of
+ `CovariantDerivative.IsCompatible` with the characterisation that parallel transport be an
+  isometry.
+
+* Given connections on bundles `V` and `W`, there is an induced connnection on the bundle Hom(V, W).
+  When this induced connection has been defined in Mathlib, rephrase the definition of
+  `CovariantDerivative.compatibilityTensor`, to be simply the covariant derivative of the metric
+  tensor (considered as a section of Hom(V, Hom(V, ℝ))).
+
+-/
+open Bundle NormedSpace
+open scoped Manifold ContDiff
+
+@[expose] public section
+
+variable
+  -- Let `M` be a `C^k` real manifold modeled on `(E, H)`
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
+  {M : Type*}
+  -- Let `V` be a bundle over `M`, endowed with a Riemannian metric.
+  (F : Type*) [NormedAddCommGroup F] [NormedSpace ℝ F]
+  {V : M → Type*} [TopologicalSpace (TotalSpace F V)]
+  [∀ x, NormedAddCommGroup (V x)] [∀ x, InnerProductSpace ℝ (V x)]
+
+/-! # Compatible connections
+
+A connection on `V` is compatible with the metric on `V` iff `X ⟨σ, τ⟩ = ⟨∇_X σ, τ⟩ + ⟨σ, ∇_X τ⟩`
+holds for all sufficiently nice vector fields `X` on `M` and sections `σ`, `τ` of `V`.
+The left hand side is the pushforward of the function `⟨σ, τ⟩` along the vector field `X`:
+the left hand side at `x` is `df(X x)`, where `f := ⟨σ, τ⟩` (ie. `X` is seen a derivation on
+the algebra of function on the base manifold acting on the function `⟨σ, τ⟩`).
+In our definition, we ask for this identity to at each `x : M`, whenever `X`, `σ` and `τ` are
+differentiable at `x`.
+-/
+
+variable {σ σ' σ'' τ τ' τ'' : Π x : M, V x}
+
+/-- The scalar product of two sections. -/
+noncomputable abbrev product (σ τ : Π x : M, V x) : M → ℝ :=
+  fun x ↦ inner ℝ (σ x) (τ x)
+
+-- `product` is C^k if σ and τ are: this is shown in `Riemannian.lean`
+
+local notation "⟪" σ ", " τ "⟫" => product σ τ
+
+-- Basic API for the product of two sections.
+section product
+
+lemma product_apply (x) : ⟪σ, τ⟫ x = inner ℝ (σ x) (τ x) := rfl
+
+variable (σ σ' τ)
+
+lemma product_swap : ⟪τ, σ⟫ = ⟪σ, τ⟫ := by
+  ext x
+  apply real_inner_comm
+
+@[simp]
+lemma product_zero_left : ⟪0, σ⟫ = 0 := by
+  ext x
+  simp only [product, Pi.zero_apply, inner_zero_left]
+
+@[simp]
+lemma product_zero_right : ⟪σ, 0⟫ = 0 := by rw [product_swap, product_zero_left]
+
+lemma product_add_left : ⟪σ + σ', τ⟫ = ⟪σ, τ⟫ + ⟪σ', τ⟫ := by
+  ext x
+  simp [product, InnerProductSpace.add_left]
+
+@[simp]
+lemma product_add_left_apply (x) : ⟪σ + σ', τ⟫ x = ⟪σ, τ⟫ x + ⟪σ', τ⟫ x := by
+  simp [product, InnerProductSpace.add_left]
+
+lemma product_add_right : ⟪σ, τ + τ'⟫ = ⟪σ, τ⟫ + ⟪σ, τ'⟫ := by
+  rw [product_swap, product_swap τ, product_swap τ', product_add_left]
+
+@[simp]
+lemma product_add_right_apply (x) : ⟪σ, τ + τ'⟫ x = ⟪σ, τ⟫ x + ⟪σ, τ'⟫ x := by
+  rw [product_swap, product_swap τ, product_swap τ', product_add_left_apply]
+
+@[simp] lemma product_neg_left : ⟪-σ, τ⟫ = -⟪σ, τ⟫ := by ext x; simp [product]
+
+@[simp] lemma product_neg_right : ⟪σ, -τ⟫ = -⟪σ, τ⟫ := by ext x; simp [product]
+
+lemma product_sub_left : ⟪σ - σ', τ⟫ = ⟪σ, τ⟫ - ⟪σ', τ⟫ := by
+  ext x
+  simp [product, inner_sub_left]
+
+lemma product_sub_right : ⟪σ, τ - τ'⟫ = ⟪σ, τ⟫ - ⟪σ, τ'⟫ := by
+  ext x
+  simp [product, inner_sub_right]
+
+lemma product_smul_left (f : M → ℝ) : product (f • σ) τ = f • product σ τ := by
+  ext x
+  simp [product, real_inner_smul_left]
+
+@[simp]
+lemma product_smul_const_left (a : ℝ) : product (a • σ) τ = a • product σ τ := by
+  ext x
+  simp [product, real_inner_smul_left]
+
+lemma product_smul_right (f : M → ℝ) : product σ (f • τ) = f • product σ τ := by
+  ext x
+  simp [product, real_inner_smul_right]
+
+@[simp]
+lemma product_smul_const_right (a : ℝ) : product σ (a • τ) = a • product σ τ := by
+  ext x
+  simp [product, real_inner_smul_right]
+
+end product
+
+-- These lemmas are necessary as my Lie bracket identities (assuming minimal differentiability)
+-- only hold point-wise. They abstract the expanding and unexpanding of `product`.
+lemma product_congr_left {x} (h : σ x = σ' x) : product σ τ x = product σ' τ x := by
+  rw [product_apply, h, ← product_apply]
+
+lemma product_congr_left₂ {x} (h : σ x = σ' x + σ'' x) :
+    product σ τ x = product σ' τ x + product σ'' τ x := by
+  rw [product_apply, h, inner_add_left, ← product_apply]
+
+lemma product_congr_right {x} (h : τ x = τ' x) : product σ τ x = product σ τ' x := by
+  rw [product_apply, h, ← product_apply]
+
+lemma product_congr_right₂ {x} (h : τ x = τ' x + τ'' x) :
+    product σ τ x = product σ τ' x + product σ τ'' x := by
+  rw [product_apply, h, inner_add_right, ← product_apply]
+
+namespace CovariantDerivative
+
+-- Let `cov` be a covariant derivative on `V`.
+-- TODO: include in cheat sheet!
+variable [TopologicalSpace M] [ChartedSpace H M] [FiberBundle F V]
+  (cov : CovariantDerivative I F V)
+
+/-- Local notation for a covariant derivative on a vector bundle acting on a vector field and a
+section. -/
+local syntax "∇" term:arg term : term
+local macro_rules | `(∇ $X $σ) => `(fun (x : M) ↦ cov $σ x ($X x))
+
+variable {F}
+
+/-- The function defining the compatibility tensor for `∇` w.r.t. `g`:
+prefer using `compatibilityTensor` instead -/
+noncomputable def compatibilityTensorAux (σ τ : Π x : M, V x) :
+    Π (x : M), TangentSpace I x →L[ℝ] ℝ := fun x ↦
+  (NormedSpace.fromTangentSpace _).toContinuousLinearMap ∘L mfderiv% ⟪σ, τ⟫ x
+  - ((innerSL ℝ (τ x)) ∘L (cov σ x)) - ((innerSL ℝ (σ x)) ∘L (cov τ x))
+
+lemma compatibilityTensorAux_apply (σ τ : Π x : M, V x)
+    {x : M} (X₀ : TangentSpace I x) :
+    compatibilityTensorAux I cov σ τ x X₀ =
+      NormedSpace.fromTangentSpace _ (mfderiv% ⟪σ, τ⟫ x X₀)
+      - inner ℝ (cov σ x X₀) (τ x) - inner ℝ (σ x) (cov τ x X₀) := by
+  rw [real_inner_comm]
+  rfl
+
+variable [VectorBundle ℝ F V] [IsContMDiffRiemannianBundle I 1 F V] {x : M}
+
+theorem compatibilityTensorAux_tensorial₁ (τ : Π x, V x) (hτ : MDiffAt (T% τ) x) :
+    TensorialAt I F (compatibilityTensorAux I cov · τ x) x where
+  smul hf hσ := by
+    ext X₀
+    rw [compatibilityTensorAux_apply, product_smul_left,
+      fromTangentSpace_mfderiv_smul_apply hf (hσ.inner_bundle hτ)]
+    simp [compatibilityTensorAux_apply, cov.isCovariantDerivativeOn.leibniz hσ hf, inner_add_left,
+      inner_smul_left]
+    ring
+  add hσ hσ' := by
+    ext X₀
+    rw [compatibilityTensorAux_apply, product_add_left,
+      fromTangentSpace_mfderiv_add_apply (hσ.inner_bundle hτ) (hσ'.inner_bundle hτ)]
+    simp [compatibilityTensorAux_apply, cov.isCovariantDerivativeOn.add hσ hσ', inner_add_left]
+    abel
+
+theorem compatibilityTensorAux_tensorial₂ (σ : Π x, V x) (hσ : MDiffAt (T% σ) x) :
+    TensorialAt I F (compatibilityTensorAux I cov σ · x) x where
+  smul hf hτ := by
+    ext X₀
+    rw [compatibilityTensorAux_apply, product_smul_right,
+      fromTangentSpace_mfderiv_smul_apply hf (hσ.inner_bundle hτ)]
+    simp [compatibilityTensorAux_apply, cov.isCovariantDerivativeOn.leibniz hτ hf, inner_add_right,
+      inner_smul_right]
+    ring
+  add hτ hτ' := by
+    ext X₀
+    rw [compatibilityTensorAux_apply, product_add_right,
+      fromTangentSpace_mfderiv_add_apply (hσ.inner_bundle hτ) (hσ.inner_bundle hτ')]
+    simp [compatibilityTensorAux_apply, cov.isCovariantDerivativeOn.add hτ hτ', inner_add_right]
+    abel
+
+variable {I} [ContMDiffVectorBundle 1 F V I] in
+/-- The tensor `(X, σ, τ) ↦ X g(σ, τ) - g(∇_X σ, τ) - g(σ, ∇_X τ)` defining when a connection
+`∇` on a Riemannian bundle `(M, V)` is compatible with the metric `g`. -/
+@[no_expose] noncomputable def compatibilityTensor [FiniteDimensional ℝ F] (x : M) :
+    V x →L[ℝ] V x →L[ℝ] (TangentSpace I x →L[ℝ] ℝ) :=
+  TensorialAt.mkHom₂ (compatibilityTensorAux I cov · · x) _
+    (compatibilityTensorAux_tensorial₁ I cov) (compatibilityTensorAux_tensorial₂ I cov)
+
+variable {X : Π x : M, TangentSpace I x}
+
+variable {I} [ContMDiffVectorBundle 1 F V I] in
+theorem compatibilityTensor_apply [FiniteDimensional ℝ F] (x : M)
+    (hσ : MDiffAt (T% σ) x) (hτ : MDiffAt (T% τ) x) :
+    cov.compatibilityTensor x (σ x) (τ x) (X x) =
+    fromTangentSpace _ (mfderiv% ⟪σ, τ⟫ x (X x)) - ⟪∇ X σ, τ⟫ x - ⟪σ, ∇ X τ⟫ x := by
+  unfold compatibilityTensor
+  rw [TensorialAt.mkHom₂_apply _ _ hσ hτ, compatibilityTensorAux_apply]
+
+open FiberBundle in
+variable {I} [ContMDiffVectorBundle 1 F V I] in
+theorem compatibilityTensor_apply_eq_extend [FiniteDimensional ℝ F] (X₀ : TangentSpace I x)
+    (σ₀ τ₀ : V x) :
+    cov.compatibilityTensor x σ₀ τ₀ X₀ =
+      fromTangentSpace _ (mfderiv% ⟪(extend F σ₀), (extend F τ₀)⟫ x X₀)
+        - inner ℝ (cov (extend F σ₀) x X₀) τ₀
+        - inner ℝ σ₀ (cov (extend F τ₀) x X₀) := by
+  simp [compatibilityTensor, TensorialAt.mkHom₂_apply_eq_extend, compatibilityTensorAux_apply]
+
+variable {I} [ContMDiffVectorBundle 1 F V I] in
+/-- Predicate saying that a connection `∇` on a Riemannian bundle `(V, g)` is compatible with the
+ambient metric, i.e. for all differentiable vector fields `X` on `M` and sections `σ` and `τ` of
+`V`, we have `X ⟨σ, τ⟩ = ⟨∇_X σ, τ⟩ + ⟨σ, ∇_X τ⟩`. -/
+def IsCompatible [FiniteDimensional ℝ F] : Prop := compatibilityTensor cov = 0
+
+variable {I} [IsManifold I 1 M] [ContMDiffVectorBundle 1 F V I]
+
+open FiberBundle in
+lemma isCompatible_iff [FiniteDimensional ℝ F] :
+    cov.IsCompatible ↔ ∀ {x : M} {X : Π x, TangentSpace I x} {σ τ : (x : M) → V x},
+      MDiffAt (T% X) x → MDiffAt (T% σ) x → MDiffAt (T% τ) x →
+      fromTangentSpace _ (mfderiv% ⟪σ, τ⟫ x (X x)) = ⟪∇ X σ, τ⟫ x + ⟪σ, ∇ X τ⟫ x := by
+  refine ⟨fun hcov x X σ τ hX hσ hτ ↦ ?_, fun h ↦ ?_⟩
+  · have H := congr($hcov x (σ x) (τ x) (X x))
+    simp [compatibilityTensor_apply _ _ hσ hτ] at H
+    linear_combination H
+  ext x σ₀ τ₀ X₀
+  rw [compatibilityTensor_apply_eq_extend]
+  have h' := h (mdifferentiableAt_extend I E X₀) (mdifferentiableAt_extend I F σ₀)
+    (mdifferentiableAt_extend I F τ₀)
+  simp [product] at h' ⊢
+  linear_combination h'
+
+end CovariantDerivative