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
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)
this :
  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)
rw :
  ContinuousOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
⊢ ContinuousOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
    (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)

Tactic:
rw [e.target_inter_preimage_symm_source_eq e', inter_comm]

Premises used: Set.inter_comm, Bundle.Pretrivialization.target_inter_preimage_symm_source_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 : (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)
this :
  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)
⊢ ContinuousOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)

Tactic:
(continuousOn_fst.prodMk this).congr ?_

Premises used: continuousOn_fst, ContinuousOn.congr, ContinuousOn.prodMk
-- 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)
this :
  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)
refine :
  EqOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
    (fun (x : B × F) ↦ (x.1, (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2))
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)
⊢ ContinuousOn ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E))
    (SProd.sprod (β := Set F) (e'.baseSet ∩ e.baseSet) univ)

Tactic:
refine (continuousOn_fst.prodMk this).congr ?_

Premises used: continuousOn_fst, ContinuousOn.congr, ContinuousOn.prodMk
-- 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)
this :
  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)
b : B
f : F
hb : (b, f).1 ∈ e'.baseSet ∩ e.baseSet
dsimp :
  (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
    (b, (a.coordChange (E := E) he' he b : (a : F) → F) f)
⊢ ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E)) (b, f) =
    (fun (x : B × F) ↦ ((x.1, (a.coordChange (E := E) he' he x.1 : (a : F) → F) x.2) : B × F)) (b, f)

Tactic:
dsimp only [Function.comp_def, Prod.map]

Premises used: Prod.map, Function.comp_def
-- 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)
this :
  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)
b : B
f : F
hb : (b, f).1 ∈ e'.baseSet ∩ e.baseSet
rw :
  (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
    (↑e : TotalSpace F E → B × F) (TotalSpace.mk (E := E) (b, f).1 (e'.symm (E := E) (b, f).1 f))
rw₁ rw₂ :
  (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
    (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) ((b, f).1, f))
⊢ (↑e : TotalSpace F E → B × F) ((↑e'.symm : B × F → TotalSpace F E) (b, f)) =
    (b, (a.coordChange (E := E) he' he b : (a : F) → F) f)

Tactic:
rw [a.mk_coordChange _ _ hb, e'.mk_symm hb.1]

Premises used: And.left, VectorPrebundle.mk_coordChange, 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 : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
⊢ Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he)

Tactic:
letI := a.totalSpaceTopology
  { linear := (a.pretrivialization_linear' e he).linear }

Premises used: Bundle.Pretrivialization.IsLinear.linear, Bundle.Trivialization.IsLinear.mk
-- 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
b : B
x : E b
⊢ TotalSpace.mk (E := E) b x ∈ (a.pretrivializationAt (E := E) b).source

Tactic:
a.toFiberPrebundle.mem_pretrivializationAt_source b x

Premises used: FiberPrebundle.mem_pretrivializationAt_source, Set.Mem, VectorPrebundle.toFiberPrebundle
-- 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
b : B
⊢ TotalSpace.mk (E := E) b ⁻¹' (a.pretrivializationAt (E := E) b).source = univ

Tactic:
a.toFiberPrebundle.totalSpaceMk_preimage_source b

Premises used: VectorPrebundle.toFiberPrebundle, FiberPrebundle.totalSpaceMk_preimage_source
-- 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
b : B
⊢ Continuous[inst_6 b, a.totalSpaceTopology] (TotalSpace.mk (E := E) b)

Tactic:
a.toFiberPrebundle.continuous_totalSpaceMk b

Premises used: FiberPrebundle.continuous_totalSpaceMk, VectorPrebundle.toFiberPrebundle
-- 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
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
⊢ Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)

Tactic:
apply linear_trivializationOfMemPretrivializationAtlas

Premises used: VectorPrebundle.linear_trivializationOfMemPretrivializationAtlas
-- 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
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := 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)
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[R] F)
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL R (E := E)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
        F →L[R] F))
    ((a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).baseSet ∩
      (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he').baseSet)

Tactic:
(a.continuousOn_coordChange he he').congr fun b hb ↦ ?_

Premises used: ContinuousOn.congr, VectorPrebundle.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 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := 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 :
  ∀ (b : B) (hb : b ∈ e.baseSet ∩ e'.baseSet),
    (↑(Trivialization.coordChangeL R (E := E)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
        F →L[R] F) =
      a.coordChange (E := E) he he' b
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[R] F)
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL R (E := E)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
            (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
        F →L[R] F))
    ((a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).baseSet ∩
      (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he').baseSet)

Tactic:
refine (a.continuousOn_coordChange he he').congr fun b hb ↦ ?_

Premises used: ContinuousOn.congr, VectorPrebundle.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 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := 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 R (E := E)
                  (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                  (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
              F →L[R] F) :
            (a : F) → F)
          v :
        F)
      ((a.coordChange (E := E) he he' b : (a : F) → F) v : F)
⊢ (↑(Trivialization.coordChangeL R (E := E)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
          (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
      F →L[R] F) =
    a.coordChange (E := E) he he' 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 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := 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
⊢ Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he)

Tactic:
haveI h₁ := a.linear_trivializationOfMemPretrivializationAtlas he
-- 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
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := 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₁ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he)
⊢ Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he')

Tactic:
haveI h₂ := a.linear_trivializationOfMemPretrivializationAtlas he'
-- 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
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := 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₁ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he)
h₂ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he')
⊢ Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)

Tactic:
rw [trivializationOfMemPretrivializationAtlas] at h₁ h₂

Premises used: VectorPrebundle.trivializationOfMemPretrivializationAtlas
-- 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
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := 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₁ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he)
h₂ : Trivialization.IsLinear R (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he')
h₃ :
  Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
⊢ Trivialization.IsLinear R (E := E)
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he')

Tactic:
rw [trivializationOfMemPretrivializationAtlas] at h₁ h₂

Premises used: VectorPrebundle.trivializationOfMemPretrivializationAtlas
-- 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
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := 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₁ :
  Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
h₂ :
  Trivialization.IsLinear R (E := E)
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he')
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 R (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((a.coordChange (E := E) he he' b : (a : F) → F) v : F)

Tactic:
rw [a.coordChange_apply he he' hb v, ContinuousLinearEquiv.coe_coe,
        Trivialization.coordChangeL_apply]

Premises used: Bundle.Trivialization.coordChangeL_apply, ContinuousLinearEquiv.coe_coe, 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
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := 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₁ :
  Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
h₂ :
  Trivialization.IsLinear R (E := E)
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he')
⊢ ((↑(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