rw [y_from_coe, h]
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ ↑z.y = 0

case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y
case this
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 2 * rt3⁻¹ * 0.im = 0

case mp.y
a b c z : ℤω
h : OneHom.toFun (↑↑inclusion) z = 0
this : ↑z.y = 0
⊢ z.y = 0.y