rw [normSq_eq_zero] at this
case mp
a b c : ℤω
h : natNorm a = 0
this : ↑normSq (OneHom.toFun (↑↑inclusion) a) = 0
⊢ a = 0
case mp
a b c : ℤω
h : natNorm a = 0
this : OneHom.toFun (↑↑inclusion) a = 0
⊢ a = 0