awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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 ∈ e'.baseSet
⊢ ((↑e.symm : B × F → TotalSpace F E) (b, v)).proj (E := E) ∈ e'.baseSet

Tactic:
rw [e.proj_symm_apply' hb.1]

Premises used: And.left, Bundle.Pretrivialization.proj_symm_apply'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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 ∈ e'.baseSet

Tactic:
hb.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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 ∈ e'.baseSet

Tactic:
exact hb.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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).2 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2

Tactic:
a.contMDiffCoordChange_apply he he' hb v

Premises used: VectorPrebundle.contMDiffCoordChange_apply
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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).2 =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2

Tactic:
exact a.contMDiffCoordChange_apply he he' hb v

Premises used: VectorPrebundle.contMDiffCoordChange_apply
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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)

Tactic:
(a.contMDiffOn_contMDiffCoordChange he he').congr ?_

Premises used: ContMDiffOn.congr, VectorPrebundle.contMDiffOn_contMDiffCoordChange
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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)
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
⊢ 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)

Tactic:
refine (a.contMDiffOn_contMDiffCoordChange he he').congr ?_

Premises used: ContMDiffOn.congr, VectorPrebundle.contMDiffOn_contMDiffCoordChange
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
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)
⊢ (↑(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

Tactic:
ext v
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
h₁ :
  b ∈
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).baseSet ∩
      (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he').baseSet
⊢ 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:
rw [a.contMDiffCoordChange_apply he he' hb v, ContinuousLinearEquiv.coe_coe,
        Trivialization.coordChangeL_apply]

Premises used: Bundle.Trivialization.coordChangeL_apply, ContinuousLinearEquiv.coe_coe, VectorPrebundle.contMDiffCoordChange_apply
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
⊢ ((↑(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:
rfl

Premises used: Bundle.Trivialization.symm, Bundle.Trivialization.toPretrivialization, rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
⊢ b ∈
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).baseSet ∩
      (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he').baseSet

Tactic:
hb

Premises used: Set.Mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
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
⊢ ((↑(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:
exacts [rfl, hb]

Premises used: rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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₀
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₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + t) x⟩) u x₀

Tactic:
rw [contMDiffWithinAt_section] at hs ht ⊢

Premises used: Bundle.contMDiffWithinAt_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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₀
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₀
⊢ 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:
set e := trivializationAt F V x₀

Premises used: FiberBundle.trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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₀

Tactic:
(hs.add ht).congr_of_eventuallyEq ?_ ?_

Premises used: ContMDiffWithinAt.add, ContMDiffWithinAt.congr_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
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₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) u x₀

Tactic:
refine (hs.add ht).congr_of_eventuallyEq ?_ ?_

Premises used: ContMDiffWithinAt.add, ContMDiffWithinAt.congr_of_eventuallyEq