-- Module: Mathlib.Topology.VectorBundle.Hom
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 : RingHomIsometric σ
inst_18 : VectorBundle 𝕜₁ F₁ E₁
inst_19 : VectorBundle 𝕜₂ F₂ E₂
inst_20 : MemTrivializationAtlas (E := E₁) e₁
inst_21 : MemTrivializationAtlas (E := E₁) e₁'
inst_22 : MemTrivializationAtlas (E := E₂) e₂
inst_23 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  Continuous (X := F₂ →L[𝕜₂] F₂) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₂ :
  Continuous (X := F₁ →L[𝕜₁] F₁) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)) :
      (a : F₁ →L[𝕜₁] F₁) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₃ :
  ContinuousOn.{u_3, u_4} (Y := F₁ →L[𝕜₁] F₁)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b) : F₁ →L[𝕜₁] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
h₄ :
  ContinuousOn.{u_3, u_6} (Y := F₂ →L[𝕜₂] F₂)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₂ (E := E₂) e₂ e₂' b) : F₂ →L[𝕜₂] F₂)) (e₂.baseSet ∩ e₂'.baseSet)
b : B
refine_3 :
  b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) →
    Eq (α := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
      (continuousLinearMapCoordChange σ (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂' b)
      ((fun (x : B) ↦
          (comp (R₂ := 𝕜₂) (σ₁₂ := RingHom.id 𝕜₂) (σ₂₃ := RingHom.id 𝕜₂) (M₂ := F₁ →SL[σ] F₂)
              (Function.comp (β := F₂ →L[𝕜₂] F₂)
                (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
                (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₂ (E := E₂) e₂ e₂' b) : F₂ →L[𝕜₂] F₂)) x)
              (Function.comp (β := F₁ →L[𝕜₁] F₁)
                (⇑(ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)) :
                  (a : F₁ →L[𝕜₁] F₁) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
                (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b) : F₁ →L[𝕜₁] F₁)) x) :
            (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂))
        b)
⊢ b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) →
    Eq (α := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
      (continuousLinearMapCoordChange σ (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂' b)
      ((fun (x : B) ↦
          (comp (R₂ := 𝕜₂) (σ₁₂ := RingHom.id 𝕜₂) (σ₂₃ := RingHom.id 𝕜₂) (M₂ := F₁ →SL[σ] F₂)
              (Function.comp (β := F₂ →L[𝕜₂] F₂)
                (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
                (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₂ (E := E₂) e₂ e₂' b) : F₂ →L[𝕜₂] F₂)) x)
              (Function.comp (β := F₁ →L[𝕜₁] F₁)
                (⇑(ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)) :
                  (a : F₁ →L[𝕜₁] F₁) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
                (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b) : F₁ →L[𝕜₁] F₁)) x) :
            (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂))
        b)

Tactic:
_