Lean: quaternion coordinates are QuaternionAlgebra.re/imI/imJ/imK, not Quaternion.re

When bridging ℝ⁴ coordinates to Mathlib's Quaternion ℝ (an abbrev for QuaternionAlgebra ℝ (-1) 0 (-1)), congrArg Quaternion.re h fails with 'Unknown constant Quaternion.re'; the projections live in the QuaternionAlgebra namespace (QuaternionAlgebra.re, .imI, .imJ, .imK; dot notation q.re works). Anonymous constructor ⟨x 0, x 1, x 2, x 3⟩ : Quaternion ℝ works, and ext <;> simp evaluates products' components (Quaternion.mul_re etc. are simp lemmas). If Star ℍ[ℝ] or normSq are not found, the file is missing import Mathlib.Algebra.Quaternion (notation needs open Quaternion). Quaternion.normSq is a MonoidWithZeroHom, so map_mul, Quaternion.normSq_inv, Quaternion.normSq_eq_zero, Quaternion.star_mul_self (star a * a = ↑(normSq a)) do the fibre algebra of the quaternionic Hopf map in a few lines.