Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: 𝕜 : 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✝²⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁵ : NormedAddCommGroup F₁
inst✝²⁴ : NormedSpace 𝕜 F₁
inst✝²³ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²² : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_15
inst✝²¹ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁰ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁹ : NormedAddCommGroup F₂
inst✝¹⁸ : NormedSpace 𝕜 F₂
inst✝¹⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁶ : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_16
inst✝¹⁵ : (x : B) → AddCommGroup (E₃ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₃ x)
inst✝¹³ : NormedAddCommGroup F₃
inst✝¹² : NormedSpace 𝕜 F₃
inst✝¹¹ : TopologicalSpace (TotalSpace F₃ E₃)
inst✝¹⁰ : (x : B) → TopologicalSpace (E₃ x)
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace M
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜 F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : FiberBundle F₃ E₃
inst✝² : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₃ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)
w : (x : M) → E₂ (b x)
hψ :
  Continuous[inst✝⁸,
      ContinuousLinearMap.topologicalSpaceTotalSpace (RingHom.id 𝕜) F₁ E₁ (F₂ →L[𝕜] F₃) fun x ↦ E₂ x →L[𝕜] E₃ x]
    fun m ↦ TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)
hv : Continuous[inst✝⁸, inst✝²³] fun m ↦ TotalSpace.mk' F₁ (b m) (v m)
hw : Continuous[inst✝⁸, inst✝¹⁷] fun m ↦ TotalSpace.mk' F₂ (b m) (w m)
⊢ Continuous[inst✝⁸, inst✝¹¹] fun m ↦ TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))

Tactic:
simp only [← continuousOn_univ] at hψ hv hw ⊢

Goal state after:
𝕜 : 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✝²⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁵ : NormedAddCommGroup F₁
inst✝²⁴ : NormedSpace 𝕜 F₁
inst✝²³ : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²² : (x : B) → TopologicalSpace (E₁ x)
E₂ : B → Type u_15
inst✝²¹ : (x : B) → AddCommGroup (E₂ x)
inst✝²⁰ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁹ : NormedAddCommGroup F₂
inst✝¹⁸ : NormedSpace 𝕜 F₂
inst✝¹⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁶ : (x : B) → TopologicalSpace (E₂ x)
E₃ : B → Type u_16
inst✝¹⁵ : (x : B) → AddCommGroup (E₃ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₃ x)
inst✝¹³ : NormedAddCommGroup F₃
inst✝¹² : NormedSpace 𝕜 F₃
inst✝¹¹ : TopologicalSpace (TotalSpace F₃ E₃)
inst✝¹⁰ : (x : B) → TopologicalSpace (E₃ x)
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace M
inst✝⁷ : FiberBundle F₁ E₁
inst✝⁶ : VectorBundle 𝕜 F₁ E₁
inst✝⁵ : FiberBundle F₂ E₂
inst✝⁴ : VectorBundle 𝕜 F₂ E₂
inst✝³ : FiberBundle F₃ E₃
inst✝² : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₃ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] E₂ (b x) →L[𝕜] E₃ (b x)
w : (x : M) → E₂ (b x)
hψ : ContinuousOn (fun m ↦ TotalSpace.mk' (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m) (ψ m)) univ
hv : ContinuousOn (fun m ↦ TotalSpace.mk' F₁ (b m) (v m)) univ
hw : ContinuousOn (fun m ↦ TotalSpace.mk' F₂ (b m) (w m)) univ
⊢ ContinuousOn (fun m ↦ TotalSpace.mk' F₃ (b m) (((ψ m) (v m)) (w m))) univ