no goals
S : Type ?u.539505
T : Type ?u.539508
R : Type u_1
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ ↑normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
simp only [normSq_def, sq, mul_neg, sub_neg_eq_add, mul_re, star_re, star_imI, star_imJ,
  star_imK]