Theorem: ℤα.im_sub_nearest (Mordell4/Rt7Ring.lean)

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

State before:
a b c : ℤα
z : ℂ
⊢ |(z - OneHom.toFun (↑↑inclusion) (nearestℤα z)).im| ≤ |4⁻¹ * rt7|
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⁻¹ * rt7|

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

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

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - (↑inclusion { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).im| ≤ |4⁻¹ * rt7|
Tactic:
rw [inclusion]
State after:
case mk
a b c : ℤα
x y : ℝ
⊢ |y -
        (↑{ toMonoidHom := { toOneHom := { toFun := toℂ, map_one' := my_map_one }, map_mul' := my_map_mul },
                map_zero' := my_map_zero, map_add' := my_map_add }
            { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).im| ≤
    |4⁻¹ * rt7|

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |y -
        (↑{ toMonoidHom := { toOneHom := { toFun := toℂ, map_one' := my_map_one }, map_mul' := my_map_mul },
                map_zero' := my_map_zero, map_add' := my_map_add }
            { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).im| ≤
    |4⁻¹ * rt7|
Tactic:
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,toℂ,complexα]
State after:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - (↑(round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y)))) + ↑(round (2 * rt7⁻¹ * y)) * { re := 1 / 2, im := rt7 / 2 }).im| ≤
    |4⁻¹ * rt7|

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - (↑(round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y)))) + ↑(round (2 * rt7⁻¹ * y)) * { re := 1 / 2, im := rt7 / 2 }).im| ≤
    |4⁻¹ * rt7|
Tactic:
norm_num
State after:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |1 / 4 * rt7|

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |1 / 4 * rt7|
Tactic:
simp only [one_div]
State after:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|
Tactic:
have := sub_hMul_round y (by norm_num : 2⁻¹ * rt7 > 0)
State after:
case mk
a b c : ℤα
x y : ℝ
this : |y - 2⁻¹ * rt7 * ↑(round ((2⁻¹ * rt7)⁻¹ * y))| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|

State before:
case mk
a b c : ℤα
x y : ℝ
this : |y - 2⁻¹ * rt7 * ↑(round ((2⁻¹ * rt7)⁻¹ * y))| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|
Tactic:
rw [mul_comm] at this
State after:
case mk
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|

State before:
case mk
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|
Tactic:
have arith : 2⁻¹ * (2⁻¹ * rt7) = |4⁻¹ * rt7| :=
  by
  ring_nf
  symm
  apply abs_of_pos
  norm_num
State after:
case mk
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
arith : 2⁻¹ * (2⁻¹ * rt7) = |4⁻¹ * rt7|
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|

State before:
case mk
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
arith : 2⁻¹ * (2⁻¹ * rt7) = |4⁻¹ * rt7|
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|
Tactic:
rwa [arith] at this
State after:
case mk
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ |4⁻¹ * rt7|
arith : 2⁻¹ * (2⁻¹ * rt7) = |4⁻¹ * rt7|
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|

State before:
a b c : ℤα
x y : ℝ
⊢ 2⁻¹ * rt7 > 0
Tactic:
norm_num
State after:
no goals

State before:
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ 2⁻¹ * (2⁻¹ * rt7) = |4⁻¹ * rt7|
Tactic:
ring_nf
State after:
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ rt7 * (↑(ofNat 1) / ↑4) = |rt7 * (↑(ofNat 1) / ↑4)|

State before:
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ rt7 * (↑(ofNat 1) / ↑4) = |rt7 * (↑(ofNat 1) / ↑4)|
Tactic:
symm
State after:
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ |rt7 * (↑(ofNat 1) / ↑4)| = rt7 * (↑(ofNat 1) / ↑4)

State before:
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ |rt7 * (↑(ofNat 1) / ↑4)| = rt7 * (↑(ofNat 1) / ↑4)
Tactic:
apply abs_of_pos
State after:
case h
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ 0 < rt7 * (↑(ofNat 1) / ↑4)

State before:
case h
a b c : ℤα
x y : ℝ
this : |y - ↑(round ((2⁻¹ * rt7)⁻¹ * y)) * (2⁻¹ * rt7)| ≤ 2⁻¹ * (2⁻¹ * rt7)
⊢ 0 < rt7 * (↑(ofNat 1) / ↑4)
Tactic:
norm_num
State after:
no goals