dsimp
a b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.x + ↑{ x := x, y := y }.y * complexω = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }
a b c : ℤω
x y : ℤ
⊢ ↑x + ↑y * complexω = { re := ↑x - ↑y / 2, im := ↑y * rt3 / 2 }