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