cases' z with x y
a b c : ℤω
z : ℂ
⊢ |(z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im| ≤ |4⁻¹ * rt3|
case mk
a b c : ℤω
x y : ℝ
⊢ |({ re := x, im := y } - OneHom.toFun (↑↑inclusion) (nearestℤω { re := x, im := y })).im| ≤ |4⁻¹ * rt3|