-- Mathlib/Topology/VectorBundle/Basic.lean
theorem toVectorBundle : @VectorBundle R _ F E _ _ _ _ _ _ a.totalSpaceTopology _ a.toFiberBundle :=
  letI := a.totalSpaceTopology; letI := a.toFiberBundle
  { trivialization_linear'

Proof state:
case mk.intro.intro.mk.intro.intro.h
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module R (E x)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace R F
inst✝¹ : TopologicalSpace B
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
h₂ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he')
⊢ (↑(a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he')
        { proj := b, snd := (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he).symm b v }).2 =
    (↑e' { proj := b, snd := e.symm b v }).2

case mk.intro.intro.mk.intro.intro.h.hb
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module R (E x)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace R F
inst✝¹ : TopologicalSpace B
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
h₂ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he')
⊢ b ∈
    (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he).baseSet ∩
      (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he').baseSet

Tactic:
exacts [rfl, hb]

Result:
no goals

Proof state:
case mk.intro.intro.mk.intro.intro.h
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module R (E x)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace R F
inst✝¹ : TopologicalSpace B
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ : Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he)
⊢ ↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
          (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b)
      v =
    (a.coordChange he he' b) v

Tactic:
haveI h₂ := a.linear_trivializationOfMemPretrivializationAtlas he'

Result:
case mk.intro.intro.mk.intro.intro.h
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module R (E x)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace R F
inst✝¹ : TopologicalSpace B
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ : Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he)
h₂ : Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he')
⊢ ↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
          (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b)
      v =
    (a.coordChange he he' b) v

Proof state:
case mk.intro.intro.mk.intro.intro.h
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module R (E x)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace R F
inst✝¹ : TopologicalSpace B
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ : Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he)
h₂ : Trivialization.IsLinear R (a.trivializationOfMemPretrivializationAtlas he')
⊢ ↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
          (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b)
      v =
    (a.coordChange he he' b) v

Tactic:
rw [trivializationOfMemPretrivializationAtlas] at h₁ h₂

Result:
case mk.intro.intro.mk.intro.intro.h
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁶ : NontriviallyNormedField R
inst✝⁵ : (x : B) → AddCommMonoid (E x)
inst✝⁴ : (x : B) → Module R (E x)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace R F
inst✝¹ : TopologicalSpace B
inst✝ : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
this : FiberBundle F E := a.toFiberBundle
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.toFiberPrebundle.pretrivializationAtlas
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.toFiberPrebundle.pretrivializationAtlas
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
h₂ : Trivialization.IsLinear R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he')
⊢ ↑(Trivialization.coordChangeL R (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he)
          (a.toFiberPrebundle.trivializationOfMemPretrivializationAtlas he') b)
      v =
    (a.coordChange he he' b) v