simp [le_add_iff_nonneg_left]
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖e x‖ ≤ ‖e x‖
no goals