rw [← coe_hMul] at this
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b