Theorem: ℤω.im_sub_nearest (Mordell4/Eisenstein.lean)

State before:
a b c : ℤω
z : ℂ
⊢ (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
Tactic:
rw [sq_le_sq]
State after:
a b c : ℤω
z : ℂ
⊢ |(z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im| ≤ |4⁻¹ * rt3|

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

State before:
case mk
a b c : ℤω
x y : ℝ
⊢ |({ re := x, im := y } - OneHom.toFun (↑↑inclusion) (nearestℤω { re := x, im := y })).im| ≤ |4⁻¹ * rt3|
Tactic:
unfold nearestℤω
State after:
case mk
a b c : ℤω
x y : ℝ
⊢ |({ re := x, im := y } -
          OneHom.toFun (↑↑inclusion)
            (let y_1 := round (2 * rt3⁻¹ * { re := x, im := y }.im);
            { x := round ({ re := x, im := y }.re + 2⁻¹ * ↑y_1), y := y_1 })).im| ≤
    |4⁻¹ * rt3|

State before:
case mk
a b c : ℤω
x y : ℝ
⊢ |({ re := x, im := y } -
          OneHom.toFun (↑↑inclusion)
            (let y_1 := round (2 * rt3⁻¹ * { re := x, im := y }.im);
            { x := round ({ re := x, im := y }.re + 2⁻¹ * ↑y_1), y := y_1 })).im| ≤
    |4⁻¹ * rt3|
Tactic:
dsimp
State after:
case mk
a b c : ℤω
x y : ℝ
⊢ |y - (↑inclusion { x := round (x + 2⁻¹ * ↑(round (2 * rt3⁻¹ * y))), y := round (2 * rt3⁻¹ * y) }).im| ≤ |4⁻¹ * rt3|