awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
refine_1 : e.baseSet ∈ 𝓝[u] x₀
⊢ (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) =ᶠ[𝓝[u] x₀]
    HAdd.hAdd (α := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) fun (b : B) ↦
      ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2
have refine_1₁ : ∀ x ∈ e.baseSet,
  (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x =
    HAdd.hAdd (α := B → F) (β := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
      (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x
Tactic: apply eventually_of_mem (U := e.baseSet)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
ht : MDiffAt (T% t) x₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, (s + t) x⟩) x₀
have hs₁ : MDiffAt[univ] (T% s) x₀
Tactic: rw [← mdifferentiableWithinAt_univ] at hs ht ⊢
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
ht : MDiffAt (T% t) x₀
hs₁ : MDiffAt[univ] (T% s) x₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, (s + t) x⟩) x₀
have ht₁ : MDiffAt[univ] (T% t) x₀
Tactic: rw [← mdifferentiableWithinAt_univ] at hs ht ⊢
Cleared hypotheses: hs, ht
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (-s) x⟩) x₀
have rw : ∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀),
  (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀
Tactic: rw [mdifferentiableWithinAt_section] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀
have set : let e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀;
∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀),
  (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀
Tactic: set e := trivializationAt F E x₀
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀
have refine_1 : EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2)
  (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
Tactic: refine hs.neg.congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
refine_1 :
  EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2)
    (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀
have refine_2 : ((↑e : TotalSpace F E → B × F) ⟨x₀, (-s) x₀⟩).2 = (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
Tactic: refine hs.neg.congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2)
    (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
have refine_1 : e.baseSet ∈ 𝓝[u] x₀
Tactic: apply eventually_of_mem (U := e.baseSet)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
refine_1 : e.baseSet ∈ 𝓝[u] x₀
⊢ EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2)
    (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
have refine_1₁ : ∀ x ∈ e.baseSet,
  Eq.{u_4 + 1} (α := F) ((fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x)
    ((-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x)
Tactic: apply eventually_of_mem (U := e.baseSet)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, (-s) x⟩) x₀
have hs₁ : MDiffAt[univ] (T% s) x₀
Tactic: rw [← mdifferentiableWithinAt_univ] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
ht : MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (s - t) x⟩) x₀
have rw : (MDiffAt[u] fun (x : B) ↦ ⟨x, (s + -t) x⟩) x₀
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
ht : MDiffAt (T% t) x₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, (s - t) x⟩) x₀
have rw : (MDiffAt fun (x : B) ↦ ⟨x, (s + -t) x⟩) x₀
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
hs : MDiffAt[u] (T% s) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (f • s) x⟩) x₀
have rw : ∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀),
  (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2) x₀
Tactic: rw [mdifferentiableWithinAt_section] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2) x₀
have set : let e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀;
∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀),
  (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2) x₀
Tactic: set e := trivializationAt F E x₀
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2) x₀
have refine_1 : EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2)
  fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).2
Tactic: refine (hf.smul hs).congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
refine_1 :
  EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2)
    fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).2
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2) x₀
have refine_2 : ((↑e : TotalSpace F E → B × F) ⟨x₀, (f • s) x₀⟩).2 = f x₀ • ((↑e : TotalSpace F E → B × F) ⟨x₀, s x₀⟩).2
Tactic: refine (hf.smul hs).congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2)
    fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).2
have refine_1 : e.baseSet ∈ 𝓝[u] x₀
Tactic: apply eventually_of_mem (U := e.baseSet)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
refine_1 : e.baseSet ∈ 𝓝[u] x₀
⊢ EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2)
    fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).2
have refine_1₁ : ∀ x ∈ e.baseSet,
  Eq.{u_4 + 1} (α := F) ((fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2) x)
    ((fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).2) x)
Tactic: apply eventually_of_mem (U := e.baseSet)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
f : B → 𝕜
s : (x : B) → E x
x₀ : B
hf : MDiffAt f x₀
hs : MDiffAt (T% s) x₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, (f • s) x⟩) x₀
have hs₁ : MDiffAt[univ] (T% s) x₀
Tactic: rw [← mdifferentiableWithinAt_univ] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀
have empty : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) x₀
Tactic: 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
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
x₀ : B
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiffAt[u] (T% t) x₀
empty : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s) (h : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀),
  (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ insert i s, t i x⟩) x₀
Tactic: 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
Cleared hypotheses: s