cases' a with x y
a b c : ℤω
⊢ ↑a.x = (OneHom.toFun (↑↑inclusion) a).re + rt3⁻¹ * (OneHom.toFun (↑↑inclusion) a).im
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