no goals
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type ?u.45640
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → F
hf : IsBoundedLinearMap 𝕜 f
hg : IsBoundedLinearMap 𝕜 g
hlf : IsLinearMap 𝕜 f
Mf : ℝ
left✝¹ : 0 < Mf
hMf : ∀ (x : E), ‖f x‖ ≤ Mf * ‖x‖
hlg : IsLinearMap 𝕜 g
Mg : ℝ
left✝ : 0 < Mg
hMg : ∀ (x : E), ‖g x‖ ≤ Mg * ‖x‖
x : E
⊢ Mf * ‖x‖ + Mg * ‖x‖ ≤ (Mf + Mg) * ‖x‖
rw [add_mul]