simp only [add_im, int_cast_im, mul_im, int_cast_re, MulZeroClass.zero_mul, add_zero, zero_add,
  mul_eq_mul_left_iff, cast_eq_zero]
case a
a b c : ℤω
x y : ℤ
⊢ (↑x + ↑y * { re := -1 / 2, im := rt3 / 2 }).im = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }.im
case a
a b c : ℤω
x y : ℤ
⊢ ↑y * (rt3 / 2) = ↑y * rt3 / 2