Raise the Hopf-Rinow development to Mathlib quality gates

.github/workflows/ci.yml

@@ -0,0 +1,22 @@
+name: CI
+
+on:
+  push:
+    branches: [main, feat/hopf-rinow]
+  pull_request:
+    branches: [main, feat/hopf-rinow]
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v6
+      - uses: leanprover/lean-action@v1
+        with:
+          build: true
+          test: true
+          lint: true
+          use-mathlib-cache: true
+      - name: Lint text style
+        run: lake exe lint-style OpenGALib

OpenGALib/Algebraic/BilinearForm/Basic.lean

@@ -75,37 +75,31 @@ theorem inner_smul_right (B : Form 𝕜 V) (c : 𝕜) (v w : V) :
   simp [inner_def, smul_eq_mul]
 
 /-- **Zero in left argument**. -/
-@[simp]
 theorem inner_zero_left (B : Form 𝕜 V) (w : V) :
     inner B 0 w = 0 := by
   simp [inner_def]
 
 /-- **Zero in right argument**. -/
-@[simp]
 theorem inner_zero_right (B : Form 𝕜 V) (v : V) :
     inner B v 0 = 0 := by
   simp [inner_def]
 
 /-- **Negation in left argument**. -/
-@[simp]
 theorem inner_neg_left (B : Form 𝕜 V) (v w : V) :
     inner B (-v) w = -inner B v w := by
   simp [inner_def, map_neg, LinearMap.neg_apply]
 
 /-- **Negation in right argument**. -/
-@[simp]
 theorem inner_neg_right (B : Form 𝕜 V) (v w : V) :
     inner B v (-w) = -inner B v w := by
   simp [inner_def, map_neg]
 
 /-- **Subtraction in left argument**. -/
-@[simp]
 theorem inner_sub_left (B : Form 𝕜 V) (v₁ v₂ w : V) :
     inner B (v₁ - v₂) w = inner B v₁ w - inner B v₂ w := by
   simp [inner_def, map_sub, LinearMap.sub_apply]
 
 /-- **Subtraction in right argument**. -/
-@[simp]
 theorem inner_sub_right (B : Form 𝕜 V) (v w₁ w₂ : V) :
     inner B v (w₁ - w₂) = inner B v w₁ - inner B v w₂ := by
   simp [inner_def, map_sub]

OpenGALib/MetricGeometry/ProperExhaustion.lean

@@ -5,7 +5,7 @@ import OpenGALib.Util.Attributes
 /-!
 # Properness via divergent compact exhaustions
 
-do Carmo, *Riemannian Geometry*, Ch. 7, Theorem 2.8, b) ⟺ e): a metric space
+do Carmo, *Riemannian Geometry*, Ch. 7, Theorem 2.8, b) ↔ e): a metric space
 has the Heine–Borel property (closed bounded sets are compact, i.e. it is a
 *proper* space) iff it admits a monotone exhaustion by compact sets `K n` such
 that every sequence escaping all the `K n` diverges in distance from a fixed
@@ -19,7 +19,7 @@ namespace OpenGA
 
 variable {α : Type*} [PseudoMetricSpace α]
 
-/-- **Math.** do Carmo Ch. 7, Theorem 2.8, b) ⟺ e). A pseudometric space is
+/-- **Math.** do Carmo Ch. 7, Theorem 2.8, b) ↔ e). A pseudometric space is
 **proper** (closed balls — equivalently closed bounded sets — are compact) iff
 there is a monotone exhaustion `K 0 ⊆ K 1 ⊆ ⋯`, `⋃ n, K n = univ`, by compact
 sets such that any sequence `q` with `q n ∉ K n` satisfies

OpenGALib/Riemannian/Connection/ChartChristoffel.lean

@@ -1,6 +1,5 @@
 import OpenGALib.Riemannian.TensorBundle.MusicalIso
 
-set_option linter.unusedSectionVars false
 
 /-!
 # Chart-coordinate Christoffel symbols
@@ -45,12 +44,14 @@ def chartGramOnE (g : RiemannianMetric I M) (α : M)
     (i j : Fin (Module.finrank ℝ E)) : E → ℝ :=
   fun y => chartGramMatrix (I := I) g α ((extChartAt I α).symm y) i j
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 @[simp] lemma chartGramOnE_def
     (g : RiemannianMetric I M) (α : M)
     (i j : Fin (Module.finrank ℝ E)) (y : E) :
     chartGramOnE (I := I) g α i j y =
       chartGramMatrix (I := I) g α ((extChartAt I α).symm y) i j := rfl
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** Symmetry of the chart Gram entries pulled back to `E`. -/
 lemma chartGramOnE_symm
     (g : RiemannianMetric I M) (α : M)
@@ -72,6 +73,7 @@ def chartChristoffel (g : RiemannianMetric I M) (α : M)
        partialDeriv (E := E) j (chartGramOnE (I := I) g α l i) y -
        partialDeriv (E := E) l (chartGramOnE (I := I) g α i j) y)
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 @[simp] lemma chartChristoffel_def
     (g : RiemannianMetric I M) (α : M)
     (i j k : Fin (Module.finrank ℝ E)) (y : E) :
@@ -82,6 +84,7 @@ def chartChristoffel (g : RiemannianMetric I M) (α : M)
            partialDeriv (E := E) j (chartGramOnE (I := I) g α l i) y -
            partialDeriv (E := E) l (chartGramOnE (I := I) g α i j) y) := rfl
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** **Symmetry of the Christoffel symbol** in the lower indices — the
 torsion-free property of the Levi-Civita connection, read off the coordinate
 formula. -/
@@ -104,6 +107,7 @@ theorem chartChristoffel_symm
     rw [hsym]]
   ring
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** **Christoffel contraction with the Gram matrix.** Contracting the
 Christoffel symbol `Γᵐ_{ki}` against the Gram matrix `G_{am}` recovers half the
 metric-derivative combination: `Σ_m G_{am} Γᵐ_{ki} = ½(∂_k G_{ai} + ∂_i G_{ak} −
@@ -156,6 +160,7 @@ lemma chartGram_christoffel_contraction (g : RiemannianMetric I M) (α : M)
         congr 1
         simp only [ite_mul, one_mul, zero_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true]
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** **Metric-compatibility in chart components.** The derivative of the
 Gram matrix is recovered from the Christoffel symbols:
 `∂_k G_{ij} = Σ_m (G_{mj} Γᵐ_{ki} + G_{im} Γᵐ_{kj})`. This is the coordinate form

OpenGALib/Riemannian/Connection/ChartChristoffelChange.lean

@@ -41,7 +41,6 @@ Reference: do Carmo, *Riemannian Geometry*, Ch. 2 (the connection in coordinates
 Lee, *Riemannian Manifolds*, Ch. 5 (transformation law for the Christoffel symbols).
 -/
 
-set_option linter.unusedSectionVars false
 
 noncomputable section
 
@@ -53,7 +52,7 @@ namespace Riemannian
 open Riemannian.Tensor
 
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [InnerProductSpace ℝ E]
-  [Module.Finite ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)]
+  [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)]
   {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
 
@@ -63,12 +62,14 @@ The coordinate functional `Geodesic.chartCoordFunctional` and the directional
 derivative expansion `fderiv_apply_eq_sum_partialDeriv` are provided by
 `Geodesic/CovariantDerivative.lean`. -/
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** The chart coordinates of a basis vector are Kronecker deltas. -/
 lemma chartCoord_finBasis (a b : Fin (Module.finrank ℝ E)) :
     Geodesic.chartCoord (E := E) a ((Module.finBasis ℝ E) b)
       = if b = a then (1 : ℝ) else 0 := by
   rw [Geodesic.chartCoord_def, Module.Basis.repr_self, Finsupp.single_apply]
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** Expansion of a continuous linear map through the chart basis, in
 coordinates: `(f v)^a = Σ_k v^k (f e_k)^a`. -/
 lemma chartCoord_clm_eq_sum (f : E →L[ℝ] E) (a : Fin (Module.finrank ℝ E)) (v : E) :
@@ -97,6 +98,7 @@ moving foot. The argument order matches `tangentCoordChange I β α`. -/
 def chartTransition (β α : M) : E → E :=
   extChartAt I α ∘ (extChartAt I β).symm
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 @[simp] lemma chartTransition_def (β α : M) (y : E) :
     chartTransition (I := I) β α y = extChartAt I α ((extChartAt I β).symm y) := rfl
 
@@ -105,20 +107,23 @@ coordinates: the source of the transition `chartTransition β α`. -/
 def chartTransitionSource (β α : M) : Set E :=
   ((extChartAt I β).symm.trans (extChartAt I α)).source
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 lemma chartTransitionSource_eq (β α : M) :
     chartTransitionSource (I := I) (M := M) β α
       = (extChartAt I β).target
           ∩ (extChartAt I β).symm ⁻¹' (chartAt H α).source := by
   unfold chartTransitionSource
   rw [PartialEquiv.trans_source, PartialEquiv.symm_source, extChartAt_source]
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] in
 /-- **Math.** The chart overlap is open in `β`-chart coordinates (boundaryless). -/
 lemma isOpen_chartTransitionSource (β α : M) :
     IsOpen (chartTransitionSource (I := I) (M := M) β α) := by
   rw [chartTransitionSource_eq]
   exact ContinuousOn.isOpen_inter_preimage (continuousOn_extChartAt_symm β)
     (isOpen_extChartAt_target β) (chartAt H α).open_source
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 /-- **Math.** On the overlap, the foot `(extChartAt I β).symm y` lies in the chart
 source at `β`. -/
 lemma extChartAt_symm_mem_chartAt_source_left {β α : M} {y : E}
@@ -128,6 +133,7 @@ lemma extChartAt_symm_mem_chartAt_source_left {β α : M} {y : E}
   have := (extChartAt I β).map_target hy.1
   rwa [extChartAt_source] at this
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 /-- **Math.** On the overlap, the foot `(extChartAt I β).symm y` lies in the chart
 source at `α`. -/
 lemma extChartAt_symm_mem_chartAt_source_right {β α : M} {y : E}
@@ -136,13 +142,15 @@ lemma extChartAt_symm_mem_chartAt_source_right {β α : M} {y : E}
   rw [chartTransitionSource_eq] at hy
   exact hy.2
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 /-- **Math.** On the overlap, the `β`-chart reading of the foot is `y` itself. -/
 lemma extChartAt_extChartAt_symm_of_mem {β α : M} {y : E}
     (hy : y ∈ chartTransitionSource (I := I) (M := M) β α) :
     extChartAt I β ((extChartAt I β).symm y) = y := by
   rw [chartTransitionSource_eq] at hy
   exact (extChartAt I β).right_inv hy.1
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 /-- **Math.** On the overlap, the transition image lies in the `α`-chart target. -/
 lemma chartTransition_mem_target {β α : M} {y : E}
     (hy : y ∈ chartTransitionSource (I := I) (M := M) β α) :
@@ -151,6 +159,7 @@ lemma chartTransition_mem_target {β α : M} {y : E}
   rw [extChartAt_source]
   exact extChartAt_symm_mem_chartAt_source_right (I := I) hy
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 /-- **Math.** On the overlap, pulling the transition image back through the `α`-chart
 recovers the common foot. -/
 lemma extChartAt_symm_chartTransition {β α : M} {y : E}
@@ -161,6 +170,7 @@ lemma extChartAt_symm_chartTransition {β α : M} {y : E}
   rw [extChartAt_source]
   exact extChartAt_symm_mem_chartAt_source_right (I := I) hy
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 /-- **Math.** Entry point from a manifold point: if `x` lies in both chart sources,
 its `β`-chart image lies in the overlap. -/
 lemma extChartAt_mem_chartTransitionSource {β α : M} {x : M}
@@ -172,6 +182,7 @@ lemma extChartAt_mem_chartTransitionSource {β α : M} {x : M}
   rw [mem_preimage, (extChartAt I β).left_inv hxβ']
   exact hxα
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 /-- **Math.** At the `β`-chart image of a common point `x`, the transition reads off
 the `α`-chart image of `x`. -/
 lemma chartTransition_extChartAt {β α : M} {x : M}
@@ -180,19 +191,22 @@ lemma chartTransition_extChartAt {β α : M} {x : M}
   have hxβ' : x ∈ (extChartAt I β).source := by rw [extChartAt_source]; exact hxβ
   rw [chartTransition_def, (extChartAt I β).left_inv hxβ']
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] [I.Boundaryless] in
 /-- **Math.** The transition map is `C^∞` on the overlap. -/
 lemma contDiffOn_chartTransition (β α : M) :
     ContDiffOn ℝ ∞ (chartTransition (I := I) β α)
       (chartTransitionSource (I := I) (M := M) β α) :=
   contDiffOn_ext_coord_change (I := I) α β
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** The transition map is `C^∞` at each point of the (open) overlap. -/
 lemma contDiffAt_chartTransition {β α : M} {y : E}
     (hy : y ∈ chartTransitionSource (I := I) (M := M) β α) :
     ContDiffAt ℝ ∞ (chartTransition (I := I) β α) y :=
   (contDiffOn_chartTransition (I := I) β α).contDiffAt
     ((isOpen_chartTransitionSource (I := I) β α).mem_nhds hy)
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** On the overlap, the transition map differentiates to the tangent
 coordinate change at the moving foot. -/
 lemma hasFDerivAt_chartTransition {β α : M} {y : E}
@@ -208,6 +222,7 @@ lemma hasFDerivAt_chartTransition {β α : M} {y : E}
   rw [extChartAt_extChartAt_symm_of_mem (I := I) hy] at hw
   exact hasFDerivWithinAt_univ.mp hw
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** The full-space `fderiv` of the transition on the overlap is the
 tangent coordinate change at the moving foot. -/
 lemma fderiv_chartTransition {β α : M} {y : E}
@@ -223,6 +238,7 @@ def transitionDeriv (β α : M) (a i : Fin (Module.finrank ℝ E)) (y : E) : ℝ
   Geodesic.chartCoord (E := E) a
     (fderiv ℝ (chartTransition (I := I) β α) y ((Module.finBasis ℝ E) i))
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 @[simp] lemma transitionDeriv_def (β α : M) (a i : Fin (Module.finrank ℝ E)) (y : E) :
     transitionDeriv (I := I) β α a i y
       = Geodesic.chartCoord (E := E) a
@@ -235,13 +251,15 @@ def transitionSndDeriv (β α : M) (a k i : Fin (Module.finrank ℝ E)) (y : E)
     (fderiv ℝ (fderiv ℝ (chartTransition (I := I) β α)) y ((Module.finBasis ℝ E) k)
       ((Module.finBasis ℝ E) i))
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] [IsManifold I ∞ M] [I.Boundaryless] in
 @[simp] lemma transitionSndDeriv_def (β α : M)
     (a k i : Fin (Module.finrank ℝ E)) (y : E) :
     transitionSndDeriv (I := I) β α a k i y
       = Geodesic.chartCoord (E := E) a
           (fderiv ℝ (fderiv ℝ (chartTransition (I := I) β α)) y
             ((Module.finBasis ℝ E) k) ((Module.finBasis ℝ E) i)) := rfl
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** **Schwarz symmetry** of the transition second derivative in the two
 differentiation directions: `∂²x^a/∂y^k∂y^i = ∂²x^a/∂y^i∂y^k` on the overlap. -/
 lemma transitionSndDeriv_symm {β α : M} {y : E}
@@ -255,6 +273,7 @@ lemma transitionSndDeriv_symm {β α : M} {y : E}
     exact WithTop.coe_le_coe.2 le_top
   rw [transitionSndDeriv_def, transitionSndDeriv_def, hsymm.eq]
 
+omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** The moving transition derivative `y ↦ Dτ(y)` is differentiable on the
 overlap (as a map into continuous linear maps), with derivative the second
 derivative of the transition. -/
@@ -267,6 +286,7 @@ lemma hasFDerivAt_fderiv_chartTransition {β α : M} {y : E}
     exact WithTop.coe_le_coe.2 le_top
   exact (h1.differentiableAt one_ne_zero).hasFDerivAt
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** The matrix-entry function `A^a_i` is differentiable on the overlap,
 with partial derivatives the second-derivative coefficients `B^a_{ki}`. -/
 lemma hasFDerivAt_transitionDeriv {β α : M} {y : E}
@@ -289,6 +309,7 @@ section GramChange
 
 variable [I.Boundaryless]
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** **The Gram change law through the transition map** (`E`-level form of
 `chartGramMatrix_change`): on the overlap, the `β`-chart Gram entry is the
 `α`-chart Gram entry at the transition image, conjugated by the transition
@@ -310,6 +331,7 @@ theorem chartGramOnE_chartTransition (g : RiemannianMetric I M) (α β : M) {y :
     transitionDeriv_def, transitionDeriv_def,
     fderiv_chartTransition (I := I) hy]
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** **Derivative of the Gram change law** (the first-order layer): on the
 overlap,
 `∂_k G^β_{ij} = Σ_{ab} [(Σ_c ∂_c G^α_{ab}(τ y) A^c_k) A^a_i A^b_j
@@ -411,6 +433,7 @@ section Contraction
 
 variable [I.Boundaryless]
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** Cancellation of the (invertible) transition derivative: a covector
 that annihilates every column `A e_a` of the transition derivative vanishes. -/
 lemma eq_zero_of_forall_sum_mul_transitionDeriv {β α : M} {y : E}
@@ -467,6 +490,7 @@ lemma eq_zero_of_forall_sum_mul_transitionDeriv {β α : M} {y : E}
   simp only [hite, mul_ite, mul_one, mul_zero] at hv2
   simpa [Fintype.sum_ite_eq] using hv2
 
+omit [I.Boundaryless] [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** Cancellation of the (invertible) Gram matrix: a vector annihilated by
 every row of `G^α` at a foot in the chart source vanishes. -/
 lemma eq_zero_of_forall_sum_chartGramOnE_mul (g : RiemannianMetric I M) {α : M}
@@ -511,6 +535,7 @@ lemma eq_zero_of_forall_sum_chartGramOnE_mul (g : RiemannianMetric I M) {α : M}
   simp only [step, h]
   simp
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** **The transported contraction identity** — the heart of the classical
 computation. Substituting the differentiated Gram change law into the
 `β`-contraction identity `Σ_m G^β_{am} Γ^{β,m}_{ki} = ½(∂_k G^β_{ai} + ∂_i G^β_{ak}
@@ -662,6 +687,7 @@ theorem sum_gram_mul_christoffel_transition (g : RiemannianMetric I M)
     (fun p c d => chartGram_christoffel_contraction (I := I) g α p c d
       (chartTransition (I := I) β α y) hfootα)
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** Direct expansion of the same contraction through the Gram change law:
 `Σ_m G^β_{am} Γ^{β,m}_{ki} = Σ_p A^p_a Σ_q G^α_{pq}(τ y) (Σ_m A^q_m Γ^{β,m}_{ki})`. -/
 theorem sum_gram_mul_christoffel_expand (g : RiemannianMetric I M)
@@ -703,6 +729,7 @@ theorem sum_gram_mul_christoffel_expand (g : RiemannianMetric I M)
   refine Finset.sum_congr rfl fun q _ => Finset.sum_congr rfl fun m _ => ?_
   ring
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** **Change-of-chart law for the chart Christoffel symbols, index form.**
 On the overlap, `Σ_m A^q_m Γ^{β,m}_{ki} = Σ_{cd} Γ^{α,q}_{cd}(τ y) A^c_k A^d_i
 + B^q_{ki}` — the classical inhomogeneous transformation law, with the second
@@ -780,6 +807,7 @@ section Bilinear
 
 variable [I.Boundaryless]
 
+omit [InnerProductSpace ℝ E] [NeZero (Module.finrank ℝ E)] in
 /-- **Math.** **Change-of-chart transformation law for the Christoffel contraction**
 (the toll-gate identity for chart-independence of the geodesic equation, inbox
 I-0100): at a common foot `x` of the charts at `β` and `α`, with