-- 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₁_1 e₁'_1 : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂_1 e₂'_1 : 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 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
⊢ ∃ (f : B → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂),
    ContinuousOn f
        (baseSet (F := F₁ →SL[σ] F₂) (Z :=
            TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
            (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) ∩
          baseSet (F := F₁ →SL[σ] F₂) (Z :=
            TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
            (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁' e₂')) ∧
      ∀
        b ∈
          baseSet (F := F₁ →SL[σ] F₂) (Z :=
              TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
              (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) ∩
            baseSet (F := F₁ →SL[σ] F₂) (Z :=
              TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
              (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁' e₂'),
        ∀ (v : F₁ →SL[σ] F₂),
          Eq (α := F₁ →SL[σ] F₂) ((f b : (a : F₁ →SL[σ] F₂) → F₁ →SL[σ] F₂) v : F₁ →SL[σ] 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 v))).2 :
              F₁ →SL[σ] F₂)

Tactic:
exact ⟨continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂',
      continuousOn_continuousLinearMapCoordChange,
      continuousLinearMapCoordChange_apply σ e₁ e₁' e₂ e₂'⟩