chore: fix differentiability of sums of sections lemmas (#41315)

They were assuming unnecessarily strong hypotheses: weaken them to what was inteded.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>

Author: PatrickMassot

Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

@@ -297,7 +297,7 @@ lemma mdifferentiableOn_of_coeff [FiniteDimensional 𝕜 F]
   have this (i) : MDiff[u] (T% ((LinearMap.piApply (hs.coeff i)) t • s i)) :=
     (h i).smul_section ((hs.contMDiffOn i).mdifferentiableOn one_ne_zero)
   have almost : MDiff[u] (T% (fun x ↦ ∑ i, hs.coeff i x (t x) • s i x)) :=
-    .sum_section (fun i _ hx ↦ this i _ hx)
+    .sum_section (fun i _ _ hx ↦ this i _ hx)
   apply almost.congr
   intro y hy
   simpa using congrArg (TotalSpace.mk' F y) (hs.coeff_sum_eq t hy)
@@ -309,7 +309,7 @@ lemma mdifferentiableAt_of_coeff [FiniteDimensional 𝕜 F]
     MDiffAt (T% t) x := by
   have := fintypeOfFiniteDimensional hs (mem_of_mem_nhds hu)
   have almost : MDiffAt (T% (fun x ↦ ∑ i, hs.coeff i x (t x) • s i x)) x :=
-    .sum_section (fun i ↦ (h i).smul_section <|
+    .sum_section (fun i _ ↦ (h i).smul_section <|
       ((hs.contMDiffOn i).mdifferentiableOn one_ne_zero).mdifferentiableAt hu)
   exact almost.congr_of_eventuallyEq <| (hs.eventually_eq_sum_coeff_smul t hu).mono (by simp)
 

Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

@@ -455,29 +455,30 @@ lemma mdifferentiable_smul_const_section
   fun x₀ ↦ (hs x₀).smul_const_section
 
 lemma MDifferentiableWithinAt.sum_section {ι : Type*} {s : Finset ι} {t : ι → (x : B) → E x}
-    (hs : ∀ i, MDiffAt[u] (T% (t i ·)) x₀) :
+    (hs : ∀ i ∈ s, MDiffAt[u] (T% (t i ·)) x₀) :
     MDiffAt[u] (T% (fun x ↦ ∑ i ∈ s, (t i x))) x₀ := by
   classical
   induction s using Finset.induction_on with
   | empty => simpa using! (contMDiffWithinAt_zeroSection 𝕜 E).mdifferentiableWithinAt one_ne_zero
   | insert i s hi h =>
-    simpa [Finset.sum_insert hi] using! mdifferentiableWithinAt_add_section (hs i) h
+    simp only [Finset.mem_insert, forall_eq_or_imp] at hs
+    simpa [Finset.sum_insert hi] using mdifferentiableWithinAt_add_section (hs.1) (h hs.2)
 
 lemma MDifferentiableAt.sum_section {ι : Type*} {s : Finset ι} {t : ι → (x : B) → E x} {x₀ : B}
-    (hs : ∀ i, MDiffAt (T% (t i ·)) x₀) :
+    (hs : ∀ i ∈ s, MDiffAt (T% (t i ·)) x₀) :
     MDiffAt (T% (fun x ↦ ∑ i ∈ s, (t i x))) x₀ := by
   simp_rw [← mdifferentiableWithinAt_univ] at hs ⊢
   exact MDifferentiableWithinAt.sum_section hs
 
 lemma MDifferentiableOn.sum_section {ι : Type*} {s : Finset ι} {t : ι → (x : B) → E x}
-    (hs : ∀ i, MDiff[u] (T% (t i ·))) :
+    (hs : ∀ i ∈ s, MDiff[u] (T% (t i ·))) :
     MDiff[u] (T% (fun x ↦ ∑ i ∈ s, (t i x))) :=
-  fun x₀ hx₀ ↦ .sum_section fun i ↦ hs i x₀ hx₀
+  fun x₀ hx₀ ↦ .sum_section fun i hi ↦ hs i hi x₀ hx₀
 
 lemma MDifferentiable.sum_section {ι : Type*} {s : Finset ι} {t : ι → (x : B) → E x}
-    (hs : ∀ i, MDiff (T% (t i ·))) :
+    (hs : ∀ i ∈ s, MDiff (T% (t i ·))) :
     MDiff (T% (fun x ↦ ∑ i ∈ s, (t i x))) :=
-  fun x₀ ↦ .sum_section fun i ↦ (hs i) x₀
+  fun x₀ ↦ .sum_section fun i hi ↦ (hs i) hi x₀
 
 /-- The scalar product `ψ • s` of a differentiable function `ψ : M → 𝕜` and a section `s` of a
 vector bundle `V → M` is differentiable once `s` is differentiable on an open set containing
@@ -510,7 +511,7 @@ lemma MDifferentiableWithinAt.sum_section_of_locallyFinite
   let s := {i | ((fun i ↦ {x | t i x ≠ 0}) i ∩ u').Nonempty}
   have := hfin.fintype
   have : MDiffAt[u ∩ u'] (T% (fun x ↦ ∑ i ∈ s, (t i x))) x₀ :=
-     .sum_section fun i ↦ ((ht' i).mono inter_subset_left)
+     .sum_section fun i _ ↦ ((ht' i).mono inter_subset_left)
   apply (mdifferentiableWithinAt_inter hu').mp
   apply this.congr' (fun y hy ↦ ?_) inter_subset_right (mem_of_mem_nhds hu')
   rw [TotalSpace.mk_inj, tsum_eq_sum']

Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean

@@ -110,16 +110,17 @@ theorem zero (hΦ : TensorialAt I F Φ x) : Φ 0 = 0 := by
 /-- A tensorial operation on sections of a vector bundle respects sums (since it respects binary
 addition). -/
 theorem sum (hΦ : TensorialAt I F Φ x) {ι : Type*} {s : Finset ι} (σ : ι → Π x : M, V x)
-    (hσ : ∀ i, MDiffAt (T% (σ i)) x) :
+    (hσ : ∀ i ∈ s, MDiffAt (T% (σ i)) x) :
     Φ (fun x' ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i) := by
   classical
   induction s using Finset.induction_on with
   | empty =>
       rw [Finset.sum_empty]
       exact hΦ.zero
   | insert a s ha h =>
-      simp only [Finset.sum_insert ha, ← h]
-      exact hΦ.add (hσ a) (.sum_section hσ)
+      simp only [Finset.mem_insert, forall_eq_or_imp] at hσ
+      simp only [Finset.sum_insert ha, ← h hσ.2]
+      exact hΦ.add (hσ.1) (.sum_section hσ.2)
 
 variable [CompleteSpace 𝕜] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 F']
   [ContMDiffVectorBundle 1 F V I] [ContMDiffVectorBundle 1 F' V' I]
@@ -147,7 +148,7 @@ lemma pointwise (hΦ : TensorialAt I F Φ x) {σ σ' : Π x : M, V x}
   have hΦ_eq {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) :
       Φ σ = Φ (fun x' ↦ ∑ i, c i x' (σ x') • s i x') :=
     hΦ.local hσ
-      (.sum_section fun i ↦ (hc hσ i).smul_section (hs i))
+      (.sum_section fun i _ ↦ (hc hσ i).smul_section (hs i))
       (t.eventually_eq_localFrame_sum_coeff_smul b x_mem)
   -- Now evaluate using the tensoriality properties.
   rw [hΦ_eq hσ, hΦ_eq hσ', hΦ.sum, hΦ.sum]
@@ -157,8 +158,8 @@ lemma pointwise (hΦ : TensorialAt I F Φ x) {σ σ' : Π x : M, V x}
       _ = c i x (σ' x) • Φ (s i) := by rw [hσσ']
       _ = Φ ((LinearMap.piApply (c i) σ') • (s i)) :=
           hΦ.smul (hc hσ' i) (hs i) |>.symm
-  · exact fun i ↦ (hc hσ' i).smul_section (hs i)
-  · exact fun i ↦ (hc hσ i).smul_section (hs i)
+  · exact fun i _ ↦ (hc hσ' i).smul_section (hs i)
+  · exact fun i _ ↦ (hc hσ i).smul_section (hs i)
 
 /-- If the operation `Φ` on sections of vector bundles `V` and `V'` is tensorial at `x` in each
 argument, then it depends only on the value of the sections at `x`. -/