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