no goals
𝕜 : Type u_1
𝕜₂ : Type u_2
𝕜₃ : Type ?u.274096
E : Type u_3
Eₗ : Type ?u.274102
F : Type u_4
Fₗ : Type ?u.274108
G : Type ?u.274111
Gₗ : Type ?u.274114
𝓕 : Type ?u.274117
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
K : ℝ≥0
hf : LipschitzWith K ↑f
x : E
⊢ ‖↑f x‖ ≤ ↑K * ‖x‖
simpa only [dist_zero_right, f.map_zero] using hf.dist_le_mul x 0