Lean quaternions: norm_star is ambiguous under `open Quaternion`; re ≤ norm; Q * star Q

Working in Mathlib's ℍ[ℝ] with open Quaternion: (1) norm_star is ambiguous, so write _root_.norm_star, the same issue as with star_smul. (2) I found no ready lemma z.re ≤ ‖z‖ for quaternions. It is one line: have h := normSq_eq_norm_mul_self z; rw [normSq_def'] at h; nlinarith [norm_nonneg z, sq_nonneg z.imI, sq_nonneg z.imJ, sq_nonneg z.imK]. (3) For the minimizer u = ‖Q‖⁻¹ • star Q of Re(Q u): rw [mul_smul_comm, self_mul_star] leaves ‖Q‖⁻¹ * (↑(normSq Q)).re = ‖Q‖, which simp [normSq_eq_norm_mul_self]; field_simp closes once ‖Q‖ ≠ 0 is in context. (4) Polynomial identities on pairs of quaternions in ℝ⁸, such as |ā a' + b̄ b'|² = (|x|²|y|² + ⟨h x, h y⟩)/2: rw the norms with the coordinate-sum lemma and Fin.sum_univ_eight, then simp [defs, normSq_def', PiLp.inner_apply, Fin.sum_univ_five]; ring.