-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : (x : B) → AddCommMonoid (E x)
inst_1 : NormedAddCommGroup F
inst_2 : TopologicalSpace B
inst_3 : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst_4 : NontriviallyNormedField 𝕜₁
inst_5 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst_6 : TopologicalSpace B'
inst_7 : NormedSpace 𝕜₁ F
inst_8 : (x : B) → Module.{u_5, u_4} 𝕜₁ (E x)
inst_9 : TopologicalSpace (TotalSpace F E)
F' : Type u_8
inst_10 : NormedAddCommGroup F'
inst_11 : NormedSpace 𝕜₂ F'
E' : B' → Type u_9
inst_12 : (x : B') → AddCommMonoid (E' x)
inst_13 : (x : B') → Module.{u_6, u_9} 𝕜₂ (E' x)
inst_14 : TopologicalSpace (TotalSpace F' E')
inst_15 : FiberBundle F E
inst_16 : VectorBundle 𝕜₁ F E
inst_17 : (x : B') → TopologicalSpace (E' x)
inst_18 : FiberBundle F' E'
inst_19 : VectorBundle 𝕜₂ F' E'
x₀ x : B
y₀ y : B'
ϕ : ContinuousLinearMap.{u_5, u_6, u_4, u_9} σ (E x) (E' y)
hx : x ∈ Trivialization.baseSet (trivializationAt F E x₀)
hy : y ∈ Trivialization.baseSet (trivializationAt F' E' y₀)
x_1 : F
h :
  Eq.{u_8 + 1} (α := F')
    ((Trivialization.continuousLinearMapAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y ∘SL
            ϕ ∘SL Trivialization.symmL 𝕜₁ (E := E) (trivializationAt F E x₀) x :
          (a : F) → F')
        x_1 :
      F')
    (((↑(Trivialization.continuousLinearEquivAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y hy) : E' y →L[𝕜₂] F') ∘SL
            ϕ ∘SL
              (↑(ContinuousLinearEquiv.symm
                    (Trivialization.continuousLinearEquivAt 𝕜₁ (E := E) (trivializationAt F E x₀) x hx)) :
                F →L[𝕜₁] E x) :
          (a : F) → F')
        x_1 :
      F')
h₁ :
  Eq.{u_8 + 1} (α := F')
    (Function.comp.{u_3 + 1, u_9 + 1, u_8 + 1} (β := E' y)
      (⇑(Trivialization.continuousLinearMapAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y) : (a : E' y) → F')
      (Function.comp.{u_3 + 1, u_4 + 1, u_9 + 1} (β := E x) (⇑ϕ : (a : E x) → E' y)
        (⇑(Trivialization.symmL 𝕜₁ (E := E) (trivializationAt F E x₀) x) : (a : F) → E x))
      x_1)
    (Function.comp.{u_3 + 1, u_9 + 1, u_8 + 1} (β := E' y)
      (⇑(↑(Trivialization.continuousLinearEquivAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y hy) : E' y →L[𝕜₂] F') :
        (a : E' y) → F')
      (Function.comp.{u_3 + 1, u_4 + 1, u_9 + 1} (β := E x) (⇑ϕ : (a : E x) → E' y)
        (⇑(↑(ContinuousLinearEquiv.symm
                  (Trivialization.continuousLinearEquivAt 𝕜₁ (E := E) (trivializationAt F E x₀) x hx)) :
              F →L[𝕜₁] E x) :
          (a : F) → E x))
      x_1)
⊢ Eq.{u_8 + 1} (α := F') ((inCoordinates F E F' E' x₀ x y₀ y ϕ : (a : F) → F') x_1 : F')
    (((↑(Trivialization.continuousLinearEquivAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y hy) : E' y →L[𝕜₂] F') ∘SL
            ϕ ∘SL
              (↑(ContinuousLinearEquiv.symm
                    (Trivialization.continuousLinearEquivAt 𝕜₁ (E := E) (trivializationAt F E x₀) x hx)) :
                F →L[𝕜₁] E x) :
          (a : F) → F')
        x_1 :
      F')
have h₂ : Eq.{u_8 + 1} (α := F')
  (Function.comp.{u_3 + 1, u_9 + 1, u_8 + 1} (β := E' y)
    (⇑(Trivialization.continuousLinearMapAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y) : (a : E' y) → F')
    (Function.comp.{u_3 + 1, u_4 + 1, u_9 + 1} (β := E x) (⇑ϕ : (a : E x) → E' y)
      (⇑(Trivialization.symmL 𝕜₁ (E := E) (trivializationAt F E x₀) x) : (a : F) → E x))
    x_1)
  (Function.comp.{u_3 + 1, u_9 + 1, u_8 + 1} (β := E' y)
    (⇑(Trivialization.continuousLinearEquivAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y hy) : (a : E' y) → F')
    (Function.comp.{u_3 + 1, u_4 + 1, u_9 + 1} (β := E x) (⇑ϕ : (a : E x) → E' y)
      (⇑(ContinuousLinearEquiv.symm
            (Trivialization.continuousLinearEquivAt 𝕜₁ (E := E) (trivializationAt F E x₀) x hx)) :
        (a : F) → E x))
    x_1)
Tactic: simp_rw [inCoordinates, ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe,
    Trivialization.coe_continuousLinearEquivAt_eq, Trivialization.symm_continuousLinearEquivAt_eq]