z : ℂ
⊢ z.re * z.re ≤ ↑normSq z
z : ℂ
⊢ abs z.re ≤ Real.sqrt (↑normSq z)
rw [mul_self_le_mul_self_iff (abs_nonneg z.re) (abs_nonneg' _), abs_mul_abs_self, mul_self_abs]
no goals
z : ℂ
⊢ z.re * z.re ≤ ↑normSq z
apply re_sq_le_normSq