norm_num
case this
a b c z : ℤα
h : OneHom.toFun (↑↑inclusion) z = 0
⊢ 2 * rt7⁻¹ * 0.im = 0

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