simp only [add_re, int_cast_re, mul_re, int_cast_im, MulZeroClass.zero_mul, tsub_zero]
a b c : ℤα
⊢ (↑a.z + ↑a.w * { re := 1 / 2, im := rt7 / 2 }).re = ↑a.z + ↑a.w / 2
a b c : ℤα
⊢ ↑a.z + ↑a.w * (1 / 2) = ↑a.z + ↑a.w / 2