-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_15
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_16
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_8, u_16} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
inst_19 : TopologicalSpace B
inst_20 : FiberBundle F₁ E₁
inst_21 : VectorBundle 𝕜 F₁ E₁
inst_22 : FiberBundle F₂ E₂
inst_23 : VectorBundle 𝕜 F₂ E₂
inst_24 : FiberBundle F₃ E₃
inst_25 : VectorBundle 𝕜 F₃ E₃
inst_26 : ∀ (x : B), IsTopologicalAddGroup.{u_16} (E₃ x)
inst_27 : ∀ (x : B), ContinuousSMul.{u_8, u_16} 𝕜 (E₃ x)
x₀ x : B
ϕ : E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)
v : F₁
w : F₂
h₁x : x ∈ Trivialization.baseSet (trivializationAt F₁ E₁ x₀)
h₂x : x ∈ Trivialization.baseSet (trivializationAt F₂ E₂ x₀)
h₃x : x ∈ Trivialization.baseSet (trivializationAt F₃ E₃ x₀)
⊢ Eq.{u_12 + 1} (α := F₃)
    ((((inCoordinates F₁ E₁ (F₂ →L[𝕜] F₃)
                  (fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) x₀ x x₀ x ϕ :
                (a : F₁) → F₂ →L[𝕜] F₃)
              v :
            F₂ →L[𝕜] F₃) :
          (a : F₂) → F₃)
        w :
      F₃)
    (((Trivialization.linearMapAt 𝕜 (E := E₃) (trivializationAt F₃ E₃ x₀) x :
            LinearMap.{u_8, u_8, u_16, u_12} (RingHom.id 𝕜) (E₃ x) F₃) :
          (a : E₃ x) → F₃)
        ((((ϕ : (a : E₁ x) → E₂ x →L[𝕜] E₃ x) (Trivialization.symm (E := E₁) (trivializationAt F₁ E₁ x₀) x v) :
                ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) :
              (a : E₂ x) → E₃ x)
            (Trivialization.symm (E := E₂) (trivializationAt F₂ E₂ x₀) x w) :
          E₃ x) :
      F₃)
have rw : Eq.{u_12 + 1} (α := F₃)
  ((((comp (σ₁₂ := RingHom.id 𝕜) (M₂ := ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x))
                ((↑(Trivialization.continuousLinearEquivAt 𝕜 (F := F₂ →L[𝕜] F₃) (E := fun (x : B) ↦
                        ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x))
                        (trivializationAt (F₂ →L[𝕜] F₃)
                          (fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) x₀)
                        x sorry) :
                    ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x) →L[𝕜] F₂ →L[𝕜] F₃) :
                  ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x) →L[𝕜] F₂ →L[𝕜] F₃)
                (ϕ.comp (σ₁₂ := RingHom.id 𝕜)
                    (↑(ContinuousLinearEquiv.symm
                          (Trivialization.continuousLinearEquivAt 𝕜 (E := E₁) (trivializationAt F₁ E₁ x₀) x h₁x)) :
                      F₁ →L[𝕜] E₁ x) :
                  F₁ →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) :
              (a : F₁) → F₂ →L[𝕜] F₃)
            v :
          F₂ →L[𝕜] F₃) :
        (a : F₂) → F₃)
      w :
    F₃)
  (((Trivialization.linearMapAt 𝕜 (E := E₃) (trivializationAt F₃ E₃ x₀) x :
          LinearMap.{u_8, u_8, u_16, u_12} (RingHom.id 𝕜) (E₃ x) F₃) :
        (a : E₃ x) → F₃)
      ((((ϕ : (a : E₁ x) → E₂ x →L[𝕜] E₃ x) (Trivialization.symm (E := E₁) (trivializationAt F₁ E₁ x₀) x v) :
              ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) :
            (a : E₂ x) → E₃ x)
          (Trivialization.symm (E := E₂) (trivializationAt F₂ E₂ x₀) x w) :
        E₃ x) :
    F₃)
Tactic: rw [inCoordinates_eq h₁x (by simp [h₂x, h₃x])]