z w : ℂ
⊢ (z * ↑(starRingEnd ℂ) w).re ≤ Real.sqrt (↑normSq (z * ↑(starRingEnd ℂ) w))
z w : ℂ
⊢ Real.sqrt (↑normSq (z + w)) * Real.sqrt (↑normSq (z + w)) ≤
    (Real.sqrt (↑normSq z) + Real.sqrt (↑normSq w)) * (Real.sqrt (↑normSq z) + Real.sqrt (↑normSq w))
rw [mul_self_abs, add_mul_self_eq, mul_self_abs, mul_self_abs, add_right_comm, normSq_add,
  add_le_add_iff_left, mul_assoc, mul_le_mul_left (zero_lt_two' ℝ), ←
  Real.sqrt_mul <| normSq_nonneg z, ← normSq_conj w, ← map_mul]
no goals
z w : ℂ
⊢ (z * ↑(starRingEnd ℂ) w).re ≤ Real.sqrt (↑normSq (z * ↑(starRingEnd ℂ) w))
exact re_le_abs (z * conj w)