-- 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
M : Type u_13
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 : TopologicalSpace M
inst_21 : FiberBundle F₁ E₁
inst_22 : VectorBundle 𝕜 F₁ E₁
inst_23 : FiberBundle F₂ E₂
inst_24 : VectorBundle 𝕜 F₂ E₂
inst_25 : FiberBundle F₃ E₃
inst_26 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_16} (E₃ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_8, u_16} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ :
  Continuous[inst_20,
      ContinuousLinearMap.topologicalSpaceTotalSpace (RingHom.id 𝕜) F₁ E₁ (F₂ →L[𝕜] F₃) fun (x : B) ↦ E₂ x →L[𝕜] E₃ x]
    fun (m : M) ↦
    TotalSpace.mk' (E := fun (x : B) ↦
      E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m)
      (ψ m)
hv : Continuous[inst_20, inst_5] fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)
hw : Continuous[inst_20, inst_11] fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) (w m)
⊢ Continuous[inst_20, inst_17] fun (m : M) ↦
    TotalSpace.mk' (E := E₃) F₃ (b m)
      ((((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
            ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
          (a : E₂ (b m)) → E₃ (b m))
        (w m))
have simp : ∀
  (hψ :
    ContinuousOn (Y :=
      TotalSpace (F₁ →L[𝕜] F₂ →L[𝕜] F₃) fun (x : B) ↦
        E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x))
      (fun (m : M) ↦
        TotalSpace.mk' (E := fun (x : B) ↦
          E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) (F₁ →L[𝕜] F₂ →L[𝕜] F₃)
          (b m) (ψ m))
      univ)
  (hv : ContinuousOn (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ)
  (hw : ContinuousOn (Y := TotalSpace F₂ E₂) (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) (w m)) univ),
  ContinuousOn (Y := TotalSpace F₃ E₃)
    (fun (m : M) ↦
      TotalSpace.mk' (E := E₃) F₃ (b m)
        ((((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)))
    univ
Tactic: simp only [← continuousOn_univ] at hψ hv hw ⊢
Cleared hypotheses: hψ, hv, hw