simp [normSq, norm]
case mk
b c : ℤα
x y : ℤ
⊢ ↑normSq (OneHom.toFun ↑↑inclusion { z := x, w := y }) = ↑(norm { z := x, w := y })
case mk
b c : ℤα
x y : ℤ
⊢ (↑inclusion { z := x, w := y }).re * (↑inclusion { z := x, w := y }).re +
      (↑inclusion { z := x, w := y }).im * (↑inclusion { z := x, w := y }).im =
    ↑x ^ 2 + ↑x * ↑y + 2 * ↑y ^ 2