no goals
S : Type ?u.423313
T : Type ?u.423316
R : Type u_1
inst✝ : CommRing R
r x y z : R
a b c : ℍ[R]
⊢ a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re =
    a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re
simp only [one_mul, neg_mul, sub_eq_add_neg, neg_neg]