Mathlib quaternion lemma names: re_add not add_re; congrArg QuaternionAlgebra.re

When computing with ℍ[ℝ] componentwise: (1) the simp lemmas are Quaternion.re_add, Quaternion.re_coe, Quaternion.re_smul, Quaternion.imI_add, Quaternion.imI_coe, Quaternion.imI_smul (component first). Quaternion.add_re and Quaternion.zero_re do not exist. (2) The projections are QuaternionAlgebra.re etc., so write congrArg QuaternionAlgebra.imK h, not Quaternion.imK. (3) A real cast ((‖u‖^2 - 1 : ℝ) : ℍ[ℝ]) under plain simp gets push_cast-ed to (↑‖u‖ ^ 2).re, which simp then cannot finish. Use simp only [Quaternion.re_add, Quaternion.re_coe, ...] first. Likewise 2 * ξ leaves QuaternionAlgebra.re 2, so write (2 : ℝ) • ξ. (4) There is no Quaternion.normSq_pos. Use lt_of_le_of_ne Quaternion.normSq_nonneg (Ne.symm (mt Quaternion.normSq_eq_zero.1 ha)). (5) Degree of left multiplication by a unit c on S³: split on c = -1 (antipodal map, degree (-1)^4) versus no antipodal points, so 'f x ≠ -x ⇒ degree 1' applies.