simp only [complexα]
case a
a b c : ℤα
⊢ complexα.re * complexα.re - complexα.im * complexα.im = (complexα - 2).re
case a
a b c : ℤα
⊢ 1 / 2 * (1 / 2) - rt7 / 2 * (rt7 / 2) = ({ re := 1 / 2, im := rt7 / 2 } - 2).re