no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.267674
E : Type u_3
Eₗ : Type ?u.267680
F : Type u_4
Fₗ : Type ?u.267686
G : Type ?u.267689
Gₗ : Type ?u.267692
𝓕 : Type ?u.267695
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 →SL[σ₁₂] F
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : E), ‖x‖ ≠ 0 → ‖↑f x‖ ≤ M * ‖x‖
x : E
h : ‖x‖ = 0
⊢ ‖↑f x‖ ≤ M * ‖x‖
simp only [h, MulZeroClass.mul_zero, norm_image_of_norm_zero f f.2 h, le_refl]