no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.871859
𝕜₃ : Type ?u.871862
E : Type u_2
Eₗ : Type ?u.871868
F : Type ?u.871871
Fₗ : Type u_3
G : Type ?u.871877
Gₗ : Type u_4
𝓕 : Type ?u.871883
inst✝¹⁵ : SeminormedAddCommGroup E
inst✝¹⁴ : SeminormedAddCommGroup Eₗ
inst✝¹³ : SeminormedAddCommGroup F
inst✝¹² : SeminormedAddCommGroup Fₗ
inst✝¹¹ : SeminormedAddCommGroup G
inst✝¹⁰ : SeminormedAddCommGroup Gₗ
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
inst✝⁷ : NontriviallyNormedField 𝕜₃
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 Eₗ
inst✝⁴ : NormedSpace 𝕜₂ F
inst✝³ : NormedSpace 𝕜 Fₗ
inst✝² : NormedSpace 𝕜₃ G
inst✝¹ : NormedSpace 𝕜 Gₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₃ : 𝕜₂ →+* 𝕜₃
σ₁₃ : 𝕜 →+* 𝕜₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : E →L[𝕜] Fₗ
g : E →L[𝕜] Gₗ
x : E
⊢ ‖↑(ContinuousLinearMap.prod f g) x‖ ≤ ‖(f, g)‖ * ‖x‖
simpa only [prod_apply, Prod.norm_def, max_mul_of_nonneg, norm_nonneg] using
  max_le_max (le_op_norm f x) (le_op_norm g x)