simp only [← pow_two]
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⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) * (z.re - (↑inclusion (nearestℤω z)).re) +
      (z.im - (↑inclusion (nearestℤω z)).im) * (z.im - (↑inclusion (nearestℤω z)).im) <
    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⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1