-- 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₂'
x_1 : TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
x : B
L : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
h :
  Membership.mem (γ :=
    Set (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)) ⁻¹'
      (e₁.baseSet ∩ e₂.baseSet))
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)
h₁ :
  TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L) ∈
    e₁.baseSet
h₂ :
  TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L) ∈
    e₂.baseSet
⊢ Eq (α := TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
            (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L),
          comp (M₂ :=
            E₂
              (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)))
            (Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂
              (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)))
            (comp (σ₂₃ := σ) (M₂ :=
              E₁
                (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                  ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                  (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)))
              (TotalSpace.snd (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L))
              (Trivialization.symmL 𝕜₁ (E := E₁) e₁
                (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                  ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                  (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x
                    L))))).1
      (comp.{u_1, u_2, u_2, u_5, u_6, u_7} (R₂ := 𝕜₂) (σ₁₂ := σ) (σ₂₃ := RingHom.id 𝕜₂) (M₂ := F₂)
        (Trivialization.symmL 𝕜₂ (E := E₂) e₂
          (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L),
              comp (M₂ :=
                E₂
                  (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                    ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)))
                (Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂
                  (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                    ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)))
                (comp (σ₂₃ := σ) (M₂ :=
                  E₁
                    (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                      ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x
                        L)))
                  (TotalSpace.snd (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                    ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L))
                  (Trivialization.symmL 𝕜₁ (E := E₁) e₁
                    (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                      ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x
                        L))))).1)
        (comp (σ₁₂ := RingHom.id 𝕜₁)
          (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L),
              comp (M₂ :=
                E₂
                  (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                    ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)))
                (Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂
                  (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                    ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)))
                (comp (σ₂₃ := σ) (M₂ :=
                  E₁
                    (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                      ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x
                        L)))
                  (TotalSpace.snd (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                    ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L))
                  (Trivialization.symmL 𝕜₁ (E := E₁) e₁
                    (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                      ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x
                        L))))).2
          (Trivialization.continuousLinearMapAt 𝕜₁ (E := E₁) e₁
            (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                  ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                  (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L),
                comp (M₂ :=
                  E₂
                    (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                      ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x
                        L)))
                  (Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂
                    (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                      ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x
                        L)))
                  (comp (σ₂₃ := σ) (M₂ :=
                    E₁
                      (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                        ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                        (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x
                          L)))
                    (TotalSpace.snd (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                      ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L))
                    (Trivialization.symmL 𝕜₁ (E := E₁) e₁
                      (TotalSpace.proj (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                        ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
                        (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x
                          L))))).1))))
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x L)
have simp : comp.{u_1, u_2, u_2, u_5, u_6, u_7} (R₂ := 𝕜₂) (σ₁₂ := σ) (σ₂₃ := RingHom.id 𝕜₂) (M₂ := F₂)
    (Trivialization.symmL 𝕜₂ (E := E₂) e₂ x)
    (comp.{u_1, u_1, u_2, u_5, u_4, u_6} (σ₁₂ := RingHom.id 𝕜₁) (M₂ := F₁)
      (comp (σ₁₂ := σ) (Trivialization.continuousLinearMapAt 𝕜₂ (E := E₂) e₂ x)
        (L.comp (σ₁₂ := RingHom.id 𝕜₁) (Trivialization.symmL 𝕜₁ (E := E₁) e₁ x)))
      (Trivialization.continuousLinearMapAt 𝕜₁ (E := E₁) e₁ x)) =
  L
Tactic: simp only [TotalSpace.mk_inj]