awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))
have fst : ((b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v) : B × F).1 =
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
fst :
  ((b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).1
⊢ (b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))
have snd : (b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v).2 =
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ((b, (contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v) : B × F).1 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).1
have fst : ((↑e.symm : B × F → TotalSpace F E) (b, v)).proj (E := E) ∈ e'.baseSet
Tactic: rw [e.mk_symm hb.1 v, e'.coe_fst', e.proj_symm_apply' hb.1]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
he' : e' ∈ a.pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ ((↑e.symm : B × F → TotalSpace F E) (b, v)).proj (E := E) ∈ e'.baseSet
have fst : b ∈ e'.baseSet
Tactic: rw [e.proj_symm_apply' hb.1]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this_2 : FiberBundle F E := a.toFiberBundle (E := E)
this : VectorBundle 𝕜 F E := ⋯
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := E)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
        F →L[𝕜] F))
    ((a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).baseSet ∩
      (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he').baseSet)
have refine : ∀ y ∈ e.baseSet ∩ e'.baseSet,
  (↑(Trivialization.coordChangeL 𝕜 (E := E)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') y) :
      F →L[𝕜] F) =
    contMDiffCoordChange n (E := E) IB a he he' y
Tactic: refine (a.contMDiffOn_contMDiffCoordChange he he').congr ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this_2 : FiberBundle F E := a.toFiberBundle (E := E)
this : VectorBundle 𝕜 F E := ⋯
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
⊢ (↑(Trivialization.coordChangeL 𝕜 (E := E)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
      F →L[𝕜] F) =
    contMDiffCoordChange n (E := E) IB a he he' b
have h : ∀ (v : F),
  Eq (α := F)
    (((↑(Trivialization.coordChangeL 𝕜 (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[𝕜] F) :
          (a : F) → F)
        v :
      F)
    ((contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this_2 : FiberBundle F E := a.toFiberBundle (E := E)
this : VectorBundle 𝕜 F E := ⋯
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL 𝕜 (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[𝕜] F) :
          (a : F) → F)
        v :
      F)
    ((contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v : F)
have h : ((↑(a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') : TotalSpace F E → B × F)
      (TotalSpace.mk (E := E) b
        ((a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).symm (E := E) b v))).2 =
  ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2
Tactic: rw [a.contMDiffCoordChange_apply he he' hb v, ContinuousLinearEquiv.coe_coe,
        Trivialization.coordChangeL_apply]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle 𝕜 F E
ha : IsContMDiff (E := E) IB a n
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this_2 : FiberBundle F E := a.toFiberBundle (E := E)
this : VectorBundle 𝕜 F E := ⋯
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h :
  ((↑(a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') : TotalSpace F E → B × F)
        (TotalSpace.mk (E := E) b
          ((a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).symm (E := E) b v))).2 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL 𝕜 (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[𝕜] F) :
          (a : F) → F)
        v :
      F)
    ((contMDiffCoordChange n (E := E) IB a he he' b : (a : F) → F) v : F)
have h₁ : b ∈
  (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).baseSet ∩
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he').baseSet
Tactic: rw [a.contMDiffCoordChange_apply he he' hb v, ContinuousLinearEquiv.coe_coe,
        Trivialization.coordChangeL_apply]
-- 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 : ∀
  (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₀)
  (ht :
    ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
      (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀),
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) u x₀
Tactic: rw [contMDiffWithinAt_section] at hs ht ⊢
Cleared hypotheses: hs, ht
-- 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 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
ht :
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, (s + t) 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₀)
  (ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀),
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) u x₀
Tactic: set e := trivializationAt F V x₀
Cleared hypotheses: hs, ht
-- 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
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₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) u x₀
have refine_1 : (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) =ᶠ[nhdsWithin x₀ u]
  HAdd.hAdd (α := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) fun (x : M) ↦
    ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2
Tactic: refine (hs.add ht).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 t : (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₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
refine_1 :
  (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) =ᶠ[nhdsWithin x₀ u]
    HAdd.hAdd (α := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) fun (x : M) ↦
      ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) u x₀
have refine_2 : ((↑e : TotalSpace F V → M × F) ⟨x₀, (s + t) x₀⟩).2 =
  HAdd.hAdd (α := M → F) (β := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2)
    (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) x₀
Tactic: refine (hs.add ht).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 t : (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₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
⊢ (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) =ᶠ[nhdsWithin x₀ u]
    HAdd.hAdd (α := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) fun (x : M) ↦
      ((↑e : TotalSpace F V → M × F) ⟨x, t 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 t : (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₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
refine_1 : e.baseSet ∈ nhdsWithin x₀ u
⊢ (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) =ᶠ[nhdsWithin x₀ u]
    HAdd.hAdd (α := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) fun (x : M) ↦
      ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2
have refine_1₁ : ∀ x ∈ e.baseSet,
  (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) x =
    HAdd.hAdd (α := M → F) (β := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2)
      (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t 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 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 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, ht