-- Module: Mathlib.Geometry.Manifold.VectorBundle.Hom
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B) → TopologicalSpace (E₁ x)
inst_7 : (x : B) → AddCommGroup (E₂ x)
inst_8 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst_13 : NormedAddCommGroup EB
inst_14 : NormedSpace 𝕜 EB
HB : Type u_9
inst_15 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_16 : TopologicalSpace B
inst_17 : ChartedSpace HB B
EM : Type u_10
inst_18 : NormedAddCommGroup EM
inst_19 : NormedSpace 𝕜 EM
HM : Type u_11
inst_20 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_21 : TopologicalSpace M
inst_22 : ChartedSpace HM M
inst_23 : FiberBundle F₁ E₁
inst_24 : VectorBundle 𝕜 F₁ E₁
inst_25 : FiberBundle F₂ E₂
inst_26 : VectorBundle 𝕜 F₂ E₂
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_27 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
inst_29 : ContMDiffVectorBundle n F₁ E₁ IB
inst_30 : ContMDiffVectorBundle n F₂ E₂ IB
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₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂),
    ContMDiffOn IB (E' := (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n f
        (baseSet (F := F₁ →L[𝕜] F₂) (Z :=
            TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦
              ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
            (continuousLinearMap (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₂) ∩
          baseSet (F := F₁ →L[𝕜] F₂) (Z :=
            TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦
              ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
            (continuousLinearMap (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁' e₂')) ∧
      ∀
        b ∈
          baseSet (F := F₁ →L[𝕜] F₂) (Z :=
              TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
              (continuousLinearMap (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₂) ∩
            baseSet (F := F₁ →L[𝕜] F₂) (Z :=
              TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
              (continuousLinearMap (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁' e₂'),
        ∀ (v : F₁ →L[𝕜] F₂),
          Eq (α := F₁ →L[𝕜] F₂) ((f b : (a : F₁ →L[𝕜] F₂) → F₁ →L[𝕜] F₂) v : F₁ →L[𝕜] F₂)
            (((↑(continuousLinearMap (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁' e₂') :
                    (TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ E₁ x →L[𝕜] E₂ x) → B × (F₁ →L[𝕜] F₂))
                  ⟨b,
                    Pretrivialization.symm (E := fun (x : B) ↦
                      ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
                      (continuousLinearMap (RingHom.id 𝕜) (E₁ := E₁) (E₂ := E₂) e₁ e₂ :
                        Pretrivialization (B := B) (F₁ →L[𝕜] F₂) (Z :=
                          TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦
                            ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
                          (TotalSpace.proj (E := fun (x : B) ↦
                            ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))))
                      b v⟩).2 :
              F₁ →L[𝕜] F₂)

Tactic:
exact ⟨continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂',
      contMDiffOn_continuousLinearMapCoordChange,
      continuousLinearMapCoordChange_apply (RingHom.id 𝕜) e₁ e₁' e₂ e₂'⟩