-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁
inst_18 : Trivialization.IsLinear 𝕜₁ (E := E₁) e₁'
inst_19 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂
inst_20 : Trivialization.IsLinear 𝕜₂ (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ →SL[σ] F₂
v : F₁
⊢ Eq.{u_6 + 1} (α := F₂)
    ((((continuousLinearMapCoordChange σ (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂' b : (a : F₁ →SL[σ] F₂) → F₁ →SL[σ] F₂) L :
            F₁ →SL[σ] F₂) :
          (a : F₁) → F₂)
        v :
      F₂)
    ((((↑(continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁' e₂') :
                (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
              (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) b
                (Pretrivialization.symm (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                  (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂ :
                    Pretrivialization (B := B) (F₁ →SL[σ] F₂) (Z :=
                      TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                      (TotalSpace.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))
                  b L))).2 :
          (a : F₁) → F₂)
        v :
      F₂)
have h : Eq (α := F₂)
  ((Trivialization.coordChangeL 𝕜₂ (E := E₂) e₂ e₂' b : (a : F₂) → F₂)
      ((L : (a : F₁) → F₂) ((Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b : (a : F₁) → F₁) v : F₁) : F₂) :
    F₂)
  (((Trivialization.linearMapAt 𝕜₂ (E := E₂) e₂' b : LinearMap.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂) :
        (a : E₂ b) → F₂)
      (e₂.symm (E := E₂) b
        ((L : (a : F₁) → F₂)
          (((Trivialization.linearMapAt 𝕜₁ (E := E₁) e₁ b : LinearMap.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁) :
                (a : E₁ b) → F₁)
              (e₁'.symm (E := E₁) b v) :
            F₁))) :
    F₂)
Tactic: simp_rw [continuousLinearMapCoordChange, ContinuousLinearEquiv.coe_coe,
    ContinuousLinearEquiv.arrowCongrSL_apply, continuousLinearMap_apply,
    continuousLinearMap_symm_apply' σ e₁ e₂ hb.1, comp_apply, ContinuousLinearEquiv.coe_coe,
    ContinuousLinearEquiv.symm_symm, Trivialization.continuousLinearMapAt_apply,
    Trivialization.symmL_apply]