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

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