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