ext <;> dsimp <;> norm_num <;> ring
case mk.mk
c : ℤω
x✝¹ y✝¹ x✝ y✝ : ℤ
⊢ ↑(x✝¹ + x✝) + ↑(y✝¹ + y✝) * { re := -1 / 2, im := rt3 / 2 } =
    ↑x✝¹ + ↑y✝¹ * { re := -1 / 2, im := rt3 / 2 } + (↑x✝ + ↑y✝ * { re := -1 / 2, im := rt3 / 2 })
no goals