unfold normSq
a b c : ℤα
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤα z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤα z)).im ^ 2 ≤ (4⁻¹ * rt7) ^ 2
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤα z)) < 1
a b c : ℤα
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤα z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤα z)).im ^ 2 ≤ (4⁻¹ * rt7) ^ 2
⊢ ↑{ toZeroHom := { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1 },
          map_one' := normSq.proof_2, map_mul' := normSq.proof_3 }
      (z - OneHom.toFun (↑↑inclusion) (nearestℤα z)) <
    1