no goals
S : Type ?u.911149
T : Type ?u.911152
R : Type u_1
inst✝ : CommRing R
r x y z : R
a✝ b✝ c a b : ℍ[R]
⊢ ↑normSq (a + b) = ↑normSq a + (a * star b).re + ((b * star a).re + ↑normSq b)
simp_rw [normSq_def, star_add, add_mul, mul_add, add_re]
no goals
S : Type ?u.911149
T : Type ?u.911152
R : Type u_1
inst✝ : CommRing R
r x y z : R
a✝ b✝ c a b : ℍ[R]
⊢ ↑normSq a + (a * star b).re + ((b * star a).re + ↑normSq b) =
    ↑normSq a + ↑normSq b + ((a * star b).re + (b * star a).re)
abel
no goals
S : Type ?u.911149
T : Type ?u.911152
R : Type u_1
inst✝ : CommRing R
r x y z : R
a✝ b✝ c a b : ℍ[R]
⊢ ↑normSq a + ↑normSq b + ((a * star b).re + (b * star a).re) = ↑normSq a + ↑normSq b + 2 * (a * star b).re
rw [← add_re, ← star_mul_star a b, self_add_star', coe_re]