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

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

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

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |({ re := x, im := y } - OneHom.toFun (↑↑inclusion) (nearestℤα { re := x, im := y })).re| ≤ |2⁻¹|
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 })).re| ≤
    |2⁻¹|

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 })).re| ≤
    |2⁻¹|
Tactic:
dsimp
State after:
case mk
a b c : ℤα
x y : ℝ
⊢ |x - (↑inclusion { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).re| ≤ |2⁻¹|

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |x - (↑inclusion { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).re| ≤ |2⁻¹|
Tactic:
rw [inclusion]
State after:
case mk
a b c : ℤα
x y : ℝ
⊢ |x -
        (↑{ 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) }).re| ≤
    |2⁻¹|

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |x -
        (↑{ 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) }).re| ≤
    |2⁻¹|
Tactic:
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
State after:
case mk
a b c : ℤα
x y : ℝ
⊢ |x - (toℂ { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).re| ≤ |2⁻¹|

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |x - (toℂ { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).re| ≤ |2⁻¹|
Tactic:
ring_nf
State after:
case mk
a b c : ℤα
x y : ℝ
⊢ |x -
        (toℂ
            { z := round (x + ↑(round (rt7⁻¹ * y * 2)) * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)),
              w := round (rt7⁻¹ * y * 2) }).re| ≤
    |↑(ofNat 1) / ↑2|

State before:
case mk
a b c : ℤα
x y : ℝ
⊢ |x -
        (toℂ
            { z := round (x + ↑(round (rt7⁻¹ * y * 2)) * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)),
              w := round (rt7⁻¹ * y * 2) }).re| ≤
    |↑(ofNat 1) / ↑2|
Tactic:
have : |(1 / 2 : ℝ)| = 1 / 2 := by norm_num
State after:
case mk
a b c : ℤα
x y : ℝ
this : |1 / 2| = 1 / 2
⊢ |x -
        (toℂ
            { z := round (x + ↑(round (rt7⁻¹ * y * 2)) * ↑(negOfNat 1) * (↑(ofNat 1) / ↑2)),
              w := round (rt7⁻¹ * y * 2) }).re| ≤
    |↑(ofNat 1) / ↑2|

State before:
a b c : ℤα
x y : ℝ
⊢ |1 / 2| = 1 / 2
Tactic:
norm_num
State after:
no goals