simp only [coe_of_mk]
case mk
b c : ℤω
x y : ℤ
⊢ ↑{ x := x, y := y }.x =
    (OneHom.toFun ↑↑inclusion { x := x, y := y }).re + rt3⁻¹ * (OneHom.toFun ↑↑inclusion { x := x, y := y }).im
case mk
b c : ℤω
x y : ℤ
⊢ ↑x = ↑x - ↑y / 2 + rt3⁻¹ * (↑y * rt3 / 2)