awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
p : Z.TotalSpace
⊢ (↑(Z.localTrivAt (p.proj (E := Z.Fiber))) : TotalSpace F Z.Fiber → B × F) p =
    (p.proj (E := Z.Fiber), p.snd (E := Z.Fiber))

Tactic:
Z.toFiberBundleCore.localTrivAt_apply p

Premises used: VectorBundleCore.localTrivAt, VectorBundleCore.Fiber, VectorBundleCore.localTriv, FiberBundleCore.localTrivAt_apply, VectorBundleCore.toFiberBundleCore
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
⊢ (↑(Z.localTrivAt b) : TotalSpace F Z.Fiber → B × F) (TotalSpace.mk (E := Z.Fiber) b a) = (b, a)

Tactic:
Z.localTrivAt_apply _

Premises used: VectorBundleCore.localTrivAt_apply
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
⊢ b ∈ (Z.localTrivAt b).baseSet

Tactic:
Z.toFiberBundleCore.mem_localTrivAt_baseSet b

Premises used: Set.Mem, VectorBundleCore.toFiberBundleCore, FiberBundleCore.mem_localTrivAt_baseSet
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
⊢ trivializationAt F Z.Fiber b = Z.localTrivAt b

Tactic:
rfl

Premises used: VectorBundleCore.localTrivAt, VectorBundleCore.localTriv, FiberBundleCore.localTriv, FiberBundleCore.localTrivAt, rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
i_1 j i : ι
⊢ Trivialization.IsLinear R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)

Tactic:
apply localTriv.isLinear

Premises used: VectorBundleCore.localTriv.isLinear
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
i_1 j i i' : ι
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[R] F)
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
            (Z.toFiberBundleCore.localTriv i') b) :
        F →L[R] F))
    ((Z.toFiberBundleCore.localTriv i).baseSet ∩ (Z.toFiberBundleCore.localTriv i').baseSet)

Tactic:
(Z.continuousOn_coordChange i i').congr fun b hb => ?_

Premises used: ContinuousOn.congr, VectorBundleCore.continuousOn_coordChange
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b : B
a : F
i_1 j i i' : ι
refine :
  ∀ (b : B) (hb : b ∈ Z.baseSet i ∩ Z.baseSet i'),
    (↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i')
            b) :
        F →L[R] F) =
      Z.coordChange i i' b
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[R] F)
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
            (Z.toFiberBundleCore.localTriv i') b) :
        F →L[R] F))
    ((Z.toFiberBundleCore.localTriv i).baseSet ∩ (Z.toFiberBundleCore.localTriv i').baseSet)

Tactic:
refine (Z.continuousOn_coordChange i i').congr fun b hb => ?_

Premises used: ContinuousOn.congr, VectorBundleCore.continuousOn_coordChange
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b_1 : B
a : F
i_1 j i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
h :
  ∀ (v : F),
    Eq (α := F)
      (((↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
                  (Z.toFiberBundleCore.localTriv i') b) :
              F →L[R] F) :
            (a : F) → F)
          v :
        F)
      ((Z.coordChange i i' b : (a : F) → F) v : F)
⊢ (↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i) (Z.toFiberBundleCore.localTriv i')
          b) :
      F →L[R] F) =
    Z.coordChange i i' b

Tactic:
ext v
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b_1 : B
a : F
i_1 j i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
v : F
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
                (Z.toFiberBundleCore.localTriv i') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((Z.coordChange i i' b : (a : F) → F) v : F)

Tactic:
Z.localTriv_coordChange_eq i i' hb v

Premises used: VectorBundleCore.localTriv, Set.Mem, VectorBundleCore.localTriv_coordChange_eq
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : TopologicalSpace (TotalSpace F E)
inst_7 : (x : B) → TopologicalSpace (E x)
inst_8 : FiberBundle F E
ι : Type u_5
Z : VectorBundleCore R B F ι
b_1 : B
a : F
i_1 j i i' : ι
b : B
hb : b ∈ Z.baseSet i ∩ Z.baseSet i'
v : F
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL R (E := Z.Fiber) (Z.toFiberBundleCore.localTriv i)
                (Z.toFiberBundleCore.localTriv i') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((Z.coordChange i i' b : (a : F) → F) v : F)

Tactic:
exact Z.localTriv_coordChange_eq i i' hb v

Premises used: VectorBundleCore.localTriv_coordChange_eq
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
⊢ Continuous[_, inst_3] Z.proj

Tactic:
Z.toFiberBundleCore.continuous_proj

Premises used: VectorBundleCore.Fiber, VectorBundleCore.toFiberBundleCore, FiberBundleCore.continuous_proj
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
⊢ IsOpenMap Z.proj

Tactic:
Z.toFiberBundleCore.isOpenMap_proj

Premises used: VectorBundleCore.Fiber, VectorBundleCore.toFiberBundleCore, FiberBundleCore.isOpenMap_proj
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
h :
  ∀ (v : Z.Fiber b),
    Eq (α := F) ((Trivialization.continuousLinearMapAt R (E := Z.Fiber) (Z.localTriv i) b : (a : Z.Fiber b) → F) v : F)
      ((Z.coordChange (Z.indexAt b) i b : (a : Z.Fiber b) → F) v : F)
⊢ Trivialization.continuousLinearMapAt R (E := Z.Fiber) (Z.localTriv i) b = Z.coordChange (Z.indexAt b) i b

Tactic:
ext1 v
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
v : Z.Fiber b
h :
  Eq (α := F) ((Z.coordChange (Z.indexAt b) i b : (a : F) → F) v : F)
    ((Z.coordChange (Z.indexAt b) i b : (a : Z.Fiber b) → F) v : F)
⊢ Eq (α := F) ((Trivialization.continuousLinearMapAt R (E := Z.Fiber) (Z.localTriv i) b : (a : Z.Fiber b) → F) v : F)
    ((Z.coordChange (Z.indexAt b) i b : (a : Z.Fiber b) → F) v : F)

Tactic:
simp_all
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
v : Z.Fiber b
⊢ Eq (α := F) ((Z.coordChange (Z.indexAt b) i b : (a : F) → F) v : F)
    ((Z.coordChange (Z.indexAt b) i b : (a : Z.Fiber b) → F) v : F)

Tactic:
rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b₀ b : B
hb : b ∈ Trivialization.baseSet (trivializationAt F Z.Fiber b₀)
⊢ Trivialization.continuousLinearMapAt R (E := Z.Fiber) (trivializationAt F Z.Fiber b₀) b =
    Z.coordChange (Z.indexAt b) (Z.indexAt b₀) b

Tactic:
Z.localTriv_continuousLinearMapAt hb

Premises used: VectorBundleCore.localTriv, VectorBundleCore.localTriv_continuousLinearMapAt, FiberBundleCore.localTriv, FiberBundleCore.localTrivAt
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
h :
  ∀ (v : F),
    Eq (α := Z.Fiber b) ((Trivialization.symmL R (E := Z.Fiber) (Z.localTriv i) b : (a : F) → Z.Fiber b) v : Z.Fiber b)
      ((Z.coordChange i (Z.indexAt b) b : (a : F) → Z.Fiber b) v : Z.Fiber b)
⊢ Trivialization.symmL R (E := Z.Fiber) (Z.localTriv i) b = Z.coordChange i (Z.indexAt b) b

Tactic:
ext1 v
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
v : F
h :
  cast ⋯ (((↑(Z.localTriv i).symm : B × F → TotalSpace F Z.Fiber) (b, v)).snd (E := Z.Fiber)) =
    (Z.coordChange i (Z.indexAt b) b : (a : F) → Z.Fiber b) v
h₁ : b ∈ (Z.localTriv i).baseSet
⊢ Eq (α := Z.Fiber b) ((Trivialization.symmL R (E := Z.Fiber) (Z.localTriv i) b : (a : F) → Z.Fiber b) v : Z.Fiber b)
    ((Z.coordChange i (Z.indexAt b) b : (a : F) → Z.Fiber b) v : Z.Fiber b)

Tactic:
rw [(Z.localTriv i).symmL_apply R, (Z.localTriv i).symm_apply]

Premises used: VectorBundleCore.localTriv, Bundle.Trivialization.symm_apply, Bundle.Trivialization.symmL_apply
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
v : F
⊢ cast ⋯ (((↑(Z.localTriv i).symm : B × F → TotalSpace F Z.Fiber) (b, v)).snd (E := Z.Fiber)) =
    (Z.coordChange i (Z.indexAt b) b : (a : F) → Z.Fiber b) v

Tactic:
rfl

Premises used: VectorBundleCore.Fiber, FiberBundleCore.Fiber, cast, rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
v : F
⊢ b ∈ (Z.localTriv i).baseSet

Tactic:
hb
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ (Z.localTriv i).baseSet
v : F
⊢ cast ⋯ (((↑(Z.localTriv i).symm : B × F → TotalSpace F Z.Fiber) (b, v)).snd (E := Z.Fiber)) =
    (Z.coordChange i (Z.indexAt b) b : (a : F) → Z.Fiber b) v

Tactic:
exacts [rfl, hb]

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b₀ b : B
hb : b ∈ Trivialization.baseSet (trivializationAt F Z.Fiber b₀)
⊢ Trivialization.symmL R (E := Z.Fiber) (trivializationAt F Z.Fiber b₀) b = Z.coordChange (Z.indexAt b₀) (Z.indexAt b) b

Tactic:
Z.localTriv_symmL hb

Premises used: VectorBundleCore.localTriv, VectorBundleCore.localTriv_symmL, FiberBundleCore.localTriv, FiberBundleCore.localTrivAt
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField R
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace R F
inst_3 : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
b₀ b₁ b : B
hb : b ∈ Trivialization.baseSet (trivializationAt F Z.Fiber b₀) ∩ Trivialization.baseSet (trivializationAt F Z.Fiber b₁)
v : F
⊢ Eq (α := F)
    ((Trivialization.coordChangeL R (E := Z.Fiber) (trivializationAt F Z.Fiber b₀) (trivializationAt F Z.Fiber b₁) b :
          (a : F) → F)
        v :
      F)
    ((Z.coordChange (Z.indexAt b₀) (Z.indexAt b₁) b : (a : F) → F) v : F)

Tactic:
Z.localTriv_coordChange_eq _ _ hb v

Premises used: VectorBundleCore.localTriv, Set.Mem, VectorBundleCore.localTriv_coordChange_eq, FiberBundleCore.localTriv, FiberBundleCore.localTrivAt
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
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)
⊢ ContinuousOn (a.coordChange (E := E) he he') (e.baseSet ∩ e'.baseSet)

Tactic:
(Classical.choose_spec (a.exists_coordChange e he e' he')).1

Premises used: VectorPrebundle.coordChange, Classical.choose_spec, VectorPrebundle.exists_coordChange, And.left
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
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
⊢ (a.coordChange (E := E) he he' b : (a : F) → F) v =
    ((↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))).2

Tactic:
(Classical.choose_spec (a.exists_coordChange e he e' he')).2 b hb v

Premises used: Classical.choose_spec, VectorPrebundle.exists_coordChange, And.right
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
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, (a.coordChange (E := E) 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
snd :
  (b, (a.coordChange (E := E) 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
⊢ (b, (a.coordChange (E := E) he he' b : (a : F) → F) v) =
    (↑e' : TotalSpace F E → B × F) (TotalSpace.mk (E := E) b (e.symm (E := E) b v))

Tactic:
ext
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
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 : ((↑e.symm : B × F → TotalSpace F E) (b, v)).proj (E := E) ∈ e'.baseSet
⊢ ((b, (a.coordChange (E := E) 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:
rw [e.mk_symm hb.1 v, e'.coe_fst', e.proj_symm_apply' hb.1]

Premises used: And.left, Bundle.Pretrivialization.coe_fst', Bundle.Pretrivialization.proj_symm_apply', Bundle.Pretrivialization.mk_symm
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
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.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
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.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
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.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
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, (a.coordChange (E := E) 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.coordChange_apply he he' hb v

Premises used: VectorPrebundle.coordChange_apply
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
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, (a.coordChange (E := E) 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.coordChange_apply he he' hb v

Premises used: VectorPrebundle.coordChange_apply
-- Module: Mathlib.Topology.VectorBundle.Basic
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
⊢ ContinuousOn (Y := F) (fun (x : B × F) ↦ (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2)
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)

Tactic:
have : ContinuousOn (fun x : B × F ↦ a.coordChange he' he x.1 x.2)
          ((e'.baseSet ∩ e.baseSet) ×ˢ univ) :=
        isBoundedBilinearMap_apply.continuous.comp_continuousOn
          ((a.continuousOn_coordChange he' he).prodMap continuousOn_id)