awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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
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, (-s) x⟩) u x₀
have rw : ∀
  (hs :
    ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
      (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀),
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀
Tactic: rw [contMDiffWithinAt_section] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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
s : (x : M) → V x
u : Set M
x₀ : M
hs :
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀
have set : let 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₀),
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀
Tactic: set e := trivializationAt F V x₀
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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
s : (x : M) → V x
u : Set M
x₀ : M
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₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀
have refine_1 : EventuallyEq.{u_4, u_5} (β := F) (nhdsWithin x₀ u) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2)
  fun (x : M) ↦ -((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
Tactic: refine hs.neg.congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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
s : (x : M) → V x
u : Set M
x₀ : M
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₀
refine_1 :
  EventuallyEq.{u_4, u_5} (β := F) (nhdsWithin x₀ u) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2)
    fun (x : M) ↦ -((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀
have refine_2 : ((↑e : TotalSpace F V → M × F) ⟨x₀, (-s) x₀⟩).2 = -((↑e : TotalSpace F V → M × F) ⟨x₀, s x₀⟩).2
Tactic: refine hs.neg.congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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
s : (x : M) → V x
u : Set M
x₀ : M
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₀
⊢ EventuallyEq.{u_4, u_5} (β := F) (nhdsWithin x₀ u) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2)
    fun (x : M) ↦ -((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
have refine_1 : e.baseSet ∈ nhdsWithin x₀ u
Tactic: apply eventually_of_mem (U := e.baseSet)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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
s : (x : M) → V x
u : Set M
x₀ : M
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₀
refine_1 : e.baseSet ∈ nhdsWithin x₀ u
⊢ EventuallyEq.{u_4, u_5} (β := F) (nhdsWithin x₀ u) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2)
    fun (x : M) ↦ -((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
have refine_1₁ : ∀ x ∈ e.baseSet,
  Eq.{u_5 + 1} (α := F) ((fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) x)
    ((fun (x : M) ↦ -((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) x)
Tactic: apply eventually_of_mem (U := e.baseSet)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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
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, (-s) x⟩) x₀
have hs₁ : 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 ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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
s t : (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₀
ht : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s - t) x⟩) u x₀
have rw : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + -t) x⟩) u x₀
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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
s t : (x : M) → V x
x₀ : M
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) x₀
ht : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s - t) x⟩) x₀
have rw : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + -t) x⟩) x₀
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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₀
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, (f • s) x⟩) u x₀
have rw : ∀
  (hs :
    ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
      (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀),
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) u x₀
Tactic: rw [contMDiffWithinAt_section] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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₀
hs :
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) u x₀
have set : let 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₀),
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) u x₀
Tactic: set e := trivializationAt F V x₀
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) u x₀
have refine_1 : (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) =ᶠ[nhdsWithin x₀ u]
  HSMul.hSMul (β := M → F) f fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
Tactic: refine (hf.smul hs).congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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₀
refine_1 :
  (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) =ᶠ[nhdsWithin x₀ u]
    HSMul.hSMul (β := M → F) f fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) u x₀
have refine_2 : ((↑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: refine (hf.smul hs).congr_of_eventuallyEq ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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₀
⊢ (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) =ᶠ[nhdsWithin x₀ u]
    HSMul.hSMul (β := M → F) f fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
have refine_1 : e.baseSet ∈ nhdsWithin x₀ u
Tactic: apply eventually_of_mem (U := e.baseSet)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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₀
refine_1 : e.baseSet ∈ nhdsWithin x₀ u
⊢ (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) =ᶠ[nhdsWithin x₀ u]
    HSMul.hSMul (β := M → F) f fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
have refine_1₁ : ∀ x ∈ e.baseSet,
  (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) x =
    HSMul.hSMul (β := M → F) f (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) x
Tactic: apply eventually_of_mem (U := e.baseSet)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (f • s) x⟩) x₀
have hs₁ : 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 ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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 ∈ insert i s, t i x⟩) u x₀
have 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₀
Tactic: simp only [Finset.sum_insert hi]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection (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
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, t i x + ∑ i ∈ s, t i x⟩) u x₀
have insert : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, ∑ i ∈ s, t i x⟩) u x₀
Tactic: apply (hs _ (s.mem_insert_self i)).add_section