K : Type u_1
E : Type ?u.6631852
inst✝ : IsROrC K
z : K
⊢ ↑im z * ↑im z ≤ ↑normSq z
K : Type u_1
E : Type ?u.6631852
inst✝ : IsROrC K
z : K
⊢ abs (↑im z) ≤ ‖z‖
rw [mul_self_le_mul_self_iff (abs_nonneg _) (norm_nonneg _), abs_mul_abs_self, mul_self_norm]
no goals
K : Type u_1
E : Type ?u.6631852
inst✝ : IsROrC K
z : K
⊢ ↑im z * ↑im z ≤ ↑normSq z
apply im_sq_le_normSq