awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
⊢ ((↑e : TotalSpace F V → M × F) ⟨x₀, (f • s) x₀⟩).2 =
    HSMul.hSMul (β := M → F) f (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) x₀

Tactic:
apply (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).2

Premises used: FiberBundle.mem_baseSet_trivializationAt', Bundle.Trivialization.linear, IsLinearMap.map_smul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
x₀ : M
hf : ContMDiffAt I 𝓘(𝕜, 𝕜) n f x₀
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) Set.univ x₀

Tactic:
rw [← contMDiffWithinAt_univ] at hs ⊢

Premises used: contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
x₀ : M
hf : ContMDiffAt I 𝓘(𝕜, 𝕜) n f x₀
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) Set.univ x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (f • s) x⟩) Set.univ x₀

Tactic:
.smul_section hf hs

Premises used: ContMDiffWithinAt.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
x₀ : M
hf : ContMDiffAt I 𝓘(𝕜, 𝕜) n f x₀
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) Set.univ x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (f • s) x⟩) Set.univ x₀

Tactic:
exact .smul_section hf hs
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
u : Set M
hf : ContMDiffOn I 𝓘(𝕜, 𝕜) n f u
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (f • s) x⟩) u

Tactic:
fun x₀ hx₀ ↦ (hf x₀ hx₀).smul_section (hs x₀ hx₀)

Premises used: ContMDiffWithinAt.smul_section, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
f : M → 𝕜
s : (x : M) → V x
hf : ContMDiff I 𝓘(𝕜, 𝕜) n f
hs : ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, s x⟩
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, (f • s) x⟩

Tactic:
fun x₀ ↦ (hf x₀).smul_section (hs x₀)

Premises used: ContMDiff, ContMDiffAt.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
a : 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (a • s) x⟩) u x₀

Tactic:
contMDiffWithinAt_const.smul_section hs

Premises used: contMDiffWithinAt_const, ContMDiffWithinAt.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
a : 𝕜
s : (x : M) → V x
x₀ : M
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (a • s) x⟩) x₀

Tactic:
contMDiffAt_const.smul_section hs

Premises used: contMDiffAt_const, ContMDiffAt.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
a : 𝕜
s : (x : M) → V x
u : Set M
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (a • s) x⟩) u

Tactic:
contMDiffOn_const.smul_section hs

Premises used: contMDiffOn_const, ContMDiffOn.smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
a : 𝕜
s : (x : M) → V x
hs : ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, s x⟩
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, (a • s) x⟩

Tactic:
fun x₀ ↦ (hs x₀).const_smul_section

Premises used: ContMDiff, ContMDiffAt.const_smul_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
hs :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) ∅ i →
      ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) u x₀

Tactic:
simpa only [Finset.sum_empty] using contMDiffWithinAt_zeroSection ..

Premises used: Bundle.contMDiffWithinAt_zeroSection, Finset.sum_empty
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
i : ι
s : Finset ι
hi : i ∉ s
h :
  ∀ (hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
hs :
  ∀ i_1 ∈ Insert.insert i s,
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i_1 x⟩) u x₀
insert : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x + ∑ i ∈ s, t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ Insert.insert i s, t i x⟩) u x₀

Tactic:
simp only [Finset.sum_insert hi]

Premises used: Finset.sum_insert
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
i : ι
s : Finset ι
hi : i ∉ s
h :
  ∀ (hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
hs :
  ∀ i_1 ∈ Insert.insert i s,
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i_1 x⟩) u x₀
insert : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x + ∑ i ∈ s, t i x⟩) u x₀

Tactic:
apply (hs _ (s.mem_insert_self i)).add_section

Premises used: Finset.mem_insert_self, ContMDiffWithinAt.add_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
i : ι
s : Finset ι
hi : i ∉ s
h :
  ∀ (hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
hs : ∀ i_1 ∈ insert i s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i_1 x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀

Tactic:
h fun i a ↦ hs _ (s.mem_insert_of_mem a)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
i : ι
s : Finset ι
hi : i ∉ s
h :
  ∀ (hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
hs : ∀ i_1 ∈ insert i s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i_1 x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀

Tactic:
exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
empty :
  ∀
    (hs :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) u x₀
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (h :
      ∀ (hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
        ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀)
    (hs :
      ∀ i_1 ∈ Insert.insert i s,
        ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i_1 x⟩) u x₀),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ Insert.insert i s, t i x⟩) u
      x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀

Tactic:
induction s using Finset.induction_on with
  | empty =>
    simpa only [Finset.sum_empty] using contMDiffWithinAt_zeroSection ..
  | insert i s hi h =>
    simp only [Finset.sum_insert hi]
    apply (hs _ (s.mem_insert_self i)).add_section
    exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)

Premises used: Bundle.contMDiffWithinAt_zeroSection, Insert.insert, Finset.sum_empty
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
u : Set M
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀
empty :
  ∀
    (hs :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) u x₀
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
    (h :
      ∀ (hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) u x₀),
        ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀)
    (hs :
      ∀ i_1 ∈ Insert.insert i s,
        ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i_1 x⟩) u x₀),
    ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ Insert.insert i s, t i x⟩) u
      x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀

Tactic:
classical
  induction s using Finset.induction_on with
  | empty =>
    simpa only [Finset.sum_empty] using contMDiffWithinAt_zeroSection ..
  | insert i s hi h =>
    simp only [Finset.sum_insert hi]
    apply (hs _ (s.mem_insert_self i)).add_section
    exact h fun i a ↦ hs _ (s.mem_insert_of_mem a)

Premises used: Bundle.contMDiffWithinAt_zeroSection, Insert.insert, Finset.sum_empty
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) x₀
⊢ ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) Set.univ x₀

Tactic:
simp_rw [← contMDiffWithinAt_univ] at hs ⊢

Premises used: contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) Set.univ x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) Set.univ x₀

Tactic:
.sum_section hs

Premises used: ContMDiffWithinAt.sum_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
x₀ : M
ι : Type u_7
t : ι → (x : M) → V x
s : Finset ι
hs : ∀ i ∈ s, ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t i x⟩) Set.univ x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) Set.univ x₀

Tactic:
exact .sum_section hs