awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (hypothesis)
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'
⊢ MDiffAt ψ x
have this₁ : (MDiffAt fun (_x : M) ↦ 1) x
Tactic: have : MDiffAt (fun (_x : M) ↦ (1 : 𝕜)) x := mdifferentiableAt_const
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (hypothesis)
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'
⊢ Φ σ = Φ σ'
have hψ' : MDiffAt ψ x
Tactic: 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'])
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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
⊢ Φ (ψ • σ) = Φ (ψ • σ')
have rw : Φ (ψ • σ') = Φ (ψ • σ')
Tactic: rw [funext this]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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
⊢ Φ σ = Φ σ'
have calc : Φ σ = Φ (ψ • σ)
Tactic: calc Φ σ
    _ = Φ (ψ • σ) := by simp [hΦ.smul hψ' hσ, hψx]
    _ = Φ (ψ • σ') := by rw [funext this]
    _ = Φ σ' := by simp [hΦ.smul hψ' hσ', hψx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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 : Φ σ = Φ (ψ • σ)
⊢ Φ σ = Φ σ'
have calc₁ : Φ (ψ • σ) = Φ (ψ • σ')
Tactic: calc Φ σ
    _ = Φ (ψ • σ) := by simp [hΦ.smul hψ' hσ, hψx]
    _ = Φ (ψ • σ') := by rw [funext this]
    _ = Φ σ' := by simp [hΦ.smul hψ' hσ', hψx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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₁ : Φ (ψ • σ) = Φ (ψ • σ')
⊢ Φ σ = Φ σ'
have calc₂ : Φ (ψ • σ') = Φ σ'
Tactic: calc Φ σ
    _ = Φ (ψ • σ) := by simp [hΦ.smul hψ' hσ, hψx]
    _ = Φ (ψ • σ') := by rw [funext this]
    _ = Φ σ' := by simp [hΦ.smul hψ' hσ', hψx]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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₂ : Φ σ = Φ σ'
⊢ Φ σ = Φ σ'
have Introduce₃ : let ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0;
∀ (hψx : ψ x = 1), Φ σ = Φ σ'
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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), Φ σ = Φ σ'
⊢ Φ σ = Φ σ'
have Introduce₄ : let ψ : (x' : M) → 𝕜 := fun (x' : M) ↦ if σ x' = σ' x' then 1 else 0;
∀ (hψx : ψ x = 1) (this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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'), Φ σ = Φ σ'
⊢ Φ σ = Φ σ'
have 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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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 = 0
have Φ₁ : Φ 0 = Φ (HSMul.hSMul (α := M → 𝕜) (β := (x : M) → V x) 0 0)
Tactic: calc
    Φ 0 = Φ ((0 : M → 𝕜) • (0 : Π x, V x)) := by simp
    _   = 0 • Φ 0 := hΦ.smul mdifferentiableAt_const (mdifferentiable_zeroSection ..)
    _   = 0 := by simp
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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)
⊢ Φ 0 = 0
have Φ₂ : HSMul.hSMul.{u_1, u_9, u_9} (α := 𝕜) 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
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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') = ∑ i ∈ ∅, Φ (σ i)
have empty : (Φ fun (x' : M) ↦ ∑ i ∈ ∅, σ i x') = 0
Tactic: rw [Finset.sum_empty]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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) ↦ ∑ i ∈ insert a s, σ i x') = ∑ i ∈ insert a s, Φ (σ i)
have insert : (Φ fun (x' : M) ↦ σ a x' + ∑ i ∈ s, σ i x') = Φ (σ a) + Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x'
Tactic: simp only [Finset.sum_insert ha, ← h]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
have empty : (Φ fun (x' : M) ↦ ∑ i ∈ ∅, σ i x') = ∑ i ∈ ∅, Φ (σ 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σ)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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)
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (h : (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)),
  (Φ fun (x' : M) ↦ ∑ i ∈ insert a s, σ i x') = ∑ i ∈ insert a 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σ)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
have empty : (Φ fun (x' : M) ↦ ∑ i ∈ ∅, σ i x') = ∑ i ∈ ∅, Φ (σ 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σ)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (goal)
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)
⊢ (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (h : (Φ fun (x' : M) ↦ ∑ i ∈ s, σ i x') = ∑ i ∈ s, Φ (σ i)),
  (Φ fun (x' : M) ↦ ∑ i ∈ insert a s, σ i x') = ∑ i ∈ insert a 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σ)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (hypothesis)
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
⊢ Φ σ = Φ σ'
have x_mem : x ∈ t.baseSet
Tactic: have x_mem : x ∈ t.baseSet := FiberBundle.mem_baseSet_trivializationAt F V x