awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : MDiffAt ψ x
⊢ Φ (ψ • σ') = Φ σ'

Tactic:
simp [hΦ.smul hψ' hσ', hψx]

Premises used: TensorialAt.smul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : MDiffAt ψ x
calc : Φ σ = Φ (ψ • σ)
calc₁ : Φ (ψ • σ) = Φ (ψ • σ')
calc₂ : Φ (ψ • σ') = Φ σ'
⊢ Φ σ = Φ σ'

Tactic:
calc Φ σ
    _ = Φ (ψ • σ) := by simp [hΦ.smul hψ' hσ, hψx]
    _ = Φ (ψ • σ') := by rw [funext this]
    _ = Φ σ' := by simp [hΦ.smul hψ' hσ', hψx]

Premises used: HSMul.hSMul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
Introduce Introduce₁ Introduce₂ : Φ σ = Φ σ'
Introduce₃ :
  let ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0;
  ∀ (hψx : ψ x = 1), Φ σ = Φ σ'
Introduce₄ :
  let ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0;
  ∀ (hψx : ψ x = 1) (this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'), Φ σ = Φ σ'
Introduce₅ :
  let ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0;
  ∀ (hψx : ψ x = 1) (this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x') (hψ' : MDiffAt ψ x), Φ σ = Φ σ'
⊢ Φ σ = Φ σ'

Tactic:
classical
  -- Introduce the indicator function of a neighbourhood `t` of `x` on which equality holds,
  -- and cut off the two sections `σ` and `σ'` using this indicator function.
  let ψ (x' : M) : 𝕜 := if σ x' = σ' x' then 1 else 0
  have hψx : ψ x = 1 := by simp [ψ, hσσ'.self_of_nhds]
  have (x' : M) : (ψ • σ) x' = (ψ • σ') x' := by
    dsimp [ψ]
    split_ifs with hx' <;> simp [hx']
  have hψ' : MDiffAt ψ x := by
    have : MDiffAt (fun (_x : M) ↦ (1 : 𝕜)) x := mdifferentiableAt_const
    exact this.congr_of_eventuallyEq (hσσ'.mono fun x' hx' ↦ by simp [ψ, hx'])
  calc Φ σ
    _ = Φ (ψ • σ) := by simp [hΦ.smul hψ' hσ, hψx]
    _ = Φ (ψ • σ') := by rw [funext this]
    _ = Φ σ' := by simp [hΦ.smul hψ' hσ', hψx]
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
⊢ Φ 0 = Φ (HSMul.hSMul (α := M → 𝕜) (β := (x : M) → V x) 0 0)

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
⊢ Φ (HSMul.hSMul (α := M → 𝕜) (β := (x : M) → V x) 0 0) = HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) 0 (Φ 0)

Tactic:
hΦ.smul mdifferentiableAt_const (mdifferentiable_zeroSection ..)

Premises used: mdifferentiableAt_const, Bundle.mdifferentiable_zeroSection, TensorialAt.smul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
⊢ HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) 0 (Φ 0) = 0

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
Φ₁ : Φ 0 = Φ (HSMul.hSMul (α := M → 𝕜) (β := (x : M) → V x) 0 0)
Φ₂ : HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) 0 (Φ 0) = 0
⊢ Φ 0 = 0

Tactic:
calc
    Φ 0 = Φ ((0 : M → 𝕜) • (0 : Π x, V x)) := by simp
    _   = 0 • Φ 0 := hΦ.smul mdifferentiableAt_const (mdifferentiable_zeroSection ..)
    _   = 0 := by simp

Premises used: mdifferentiableAt_const, HSMul.hSMul, OfNat.ofNat, Bundle.mdifferentiable_zeroSection, TensorialAt.smul
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
ι : Type u_10
σ : ι → (x : M) → V x
hσ : ∀ (i : ι), MDiffAt (T% σ) x
empty : (Φ fun (x' : M) ↦ ∑ i ∈ ∅, σ i x') = 0
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ ∅, σ i x') = ∑ i ∈ ∅, Φ (σ i)

Tactic:
rw [Finset.sum_empty]

Premises used: Finset.sum_empty
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
ι : Type u_10
σ : ι → (x : M) → V x
hσ : ∀ (i : ι), MDiffAt (T% σ) x
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ ∅, σ i x') = 0

Tactic:
hΦ.zero

Premises used: Multiset.sum, Multiset.foldr, TensorialAt.zero, List.foldr, Finset.sum
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
ι : Type u_10
σ : ι → (x : M) → V x
hσ : ∀ (i : ι), MDiffAt (T% σ) x
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ ∅, σ i x') = 0

Tactic:
exact hΦ.zero

Premises used: TensorialAt.zero
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
ι : Type u_10
σ : ι → (x : M) → V x
hσ : ∀ (i : ι), MDiffAt (T% σ) x
a : ι
s : Finset ι
ha : a ∉ s
h : (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
insert : (Φ fun (x' : M) ↦ σ a x' + ∑ i ∈ s, σ i x') = Φ (σ a) + Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x'
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ Insert.insert a s, σ i x') = ∑ i ∈ Insert.insert a s, Φ (σ i)

Tactic:
simp only [Finset.sum_insert ha, ← h]

Premises used: Finset.sum_insert
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
ι : Type u_10
σ : ι → (x : M) → V x
hσ : ∀ (i : ι), MDiffAt (T% σ) x
a : ι
s : Finset ι
ha : a ∉ s
h : (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
⊢ (Φ fun (x' : M) ↦ σ a x' + ∑ i ∈ s, σ i x') = Φ (σ a) + Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x'

Tactic:
hΦ.add (hσ a) (.sum_section hσ)

Premises used: MDifferentiableAt.sum_section, TensorialAt.add
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
ι : Type u_10
σ : ι → (x : M) → V x
hσ : ∀ (i : ι), MDiffAt (T% σ) x
a : ι
s : Finset ι
ha : a ∉ s
h : (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
⊢ (Φ fun (x' : M) ↦ σ a x' + ∑ i ∈ s, σ i x') = Φ (σ a) + Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x'

Tactic:
exact hΦ.add (hσ a) (.sum_section hσ)

Premises used: MDifferentiableAt.sum_section, TensorialAt.add
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
ι : Type u_10
s : Finset ι
σ : ι → (x : M) → V x
hσ : ∀ (i : ι), MDiffAt (T% σ) x
empty : (Φ fun (x' : M) ↦ ∑ i ∈ ∅, σ i x') = ∑ i ∈ ∅, Φ (σ i)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (h : (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)),
    (Φ fun (x' : M) ↦ ∑ i ∈ Insert.insert a s, σ i x') = ∑ i ∈ Insert.insert a s, Φ (σ i)
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)

Tactic:
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σ)

Premises used: Insert.insert, Finset.sum_empty, TensorialAt.zero
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
hΦ : TensorialAt I F (V := V) Φ x
ι : Type u_10
s : Finset ι
σ : ι → (x : M) → V x
hσ : ∀ (i : ι), MDiffAt (T% σ) x
empty : (Φ fun (x' : M) ↦ ∑ i ∈ ∅, σ i x') = ∑ i ∈ ∅, Φ (σ i)
insert :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (h : (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)),
    (Φ fun (x' : M) ↦ ∑ i ∈ Insert.insert a s, σ i x') = ∑ i ∈ Insert.insert a s, Φ (σ i)
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)

Tactic:
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σ)

Premises used: Insert.insert, Finset.sum_empty, TensorialAt.zero
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
inst_16 : CompleteSpace 𝕜
inst_17 : FiniteDimensional 𝕜 F
inst_18 : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
⊢ x ∈ t.baseSet

Tactic:
have x_mem : x ∈ t.baseSet := FiberBundle.mem_baseSet_trivializationAt F V x
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
inst_16 : CompleteSpace 𝕜
inst_17 : FiniteDimensional 𝕜 F
inst_18 : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) → (x : M) → V x := t.localFrame (V := V) b
c : (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) →
  (x : M) → LinearMap.{u_1, u_1, u_6, u_1} (RingHom.id 𝕜) (V x) 𝕜 :=
  Trivialization.localFrame_coeff I (V := V) t b
i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)
⊢ Ne (α := ℕ∞ω) 1 0

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
inst_16 : CompleteSpace 𝕜
inst_17 : FiniteDimensional 𝕜 F
inst_18 : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) → (x : M) → V x := t.localFrame (V := V) b
c : (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) →
  (x : M) → LinearMap.{u_1, u_1, u_6, u_1} (RingHom.id 𝕜) (V x) 𝕜 :=
  Trivialization.localFrame_coeff I (V := V) t b
⊢ ∀ (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)), MDiffAt (T% s) x

Tactic:
have hs (i) : MDiffAt (T% (s i)) x :=
    (contMDiffAt_localFrame_of_mem 1 _ b i x_mem).mdifferentiableAt (by simp)
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
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
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
A : Type u_9
inst_13 : AddCommGroup A
inst_14 : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
inst_15 : VectorBundle 𝕜 F V
inst_16 : CompleteSpace 𝕜
inst_17 : FiniteDimensional 𝕜 F
inst_18 : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F (V := V) Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5) → (x : M) → V x := t.localFrame (V := V) b
c : (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)) →
  (x : M) → LinearMap.{u_1, u_1, u_6, u_1} (RingHom.id 𝕜) (V x) 𝕜 :=
  Trivialization.localFrame_coeff I (V := V) t b
hs : ∀ (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)), MDiffAt (T% s) x
⊢ ∀ {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) (i : (↑(Basis.ofVectorSpaceIndex 𝕜 F) : Type u_5)),
    MDiffAt
        ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜) (c i) :
              ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
            (a : (x : M) → V x) → M → 𝕜)
          σ)
      x

Tactic:
have hc {σ : (x : M) → V x} (hσ : MDiffAt (T% σ) x) (i) :
      MDiffAt (LinearMap.piApply (c i) σ) x :=
    mdifferentiableAt_localFrame_coeff b x_mem hσ i