internlm/Lean-Github huggingface dataset:
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
case mp
a b c : ℤω
h : natNorm a = 0
this : ↑(natNorm a) = 0
⊢ a = 0
Tactic:
rw [← natNorm_coe] at this
Proof state after:
case mp
a b c : ℤω
h : natNorm a = 0
this : ↑normSq (OneHom.toFun (↑↑inclusion) a) = 0
⊢ a = 0
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
case mp
a b c : ℤω
h : natNorm a = 0
this : ↑normSq (OneHom.toFun (↑↑inclusion) a) = 0
⊢ a = 0
Tactic:
rw [normSq_eq_zero] at this
Proof state after:
case mp
a b c : ℤω
h : natNorm a = 0
this : OneHom.toFun (↑↑inclusion) a = 0
⊢ a = 0
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
case mp
a b c : ℤω
h : natNorm a = 0
this : OneHom.toFun (↑↑inclusion) a = 0
⊢ a = 0
Tactic:
rwa [coe_eq_zero] at this
Proof state after:
no goals
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
a b c : ℤω
h : natNorm a = 0
⊢ ↑(natNorm a) = 0
Tactic:
exact_mod_cast h
Proof state after:
no goals
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
case mpr
a b c : ℤω
⊢ a = 0 → natNorm a = 0
Tactic:
intro h
Proof state after:
case mpr
a b c : ℤω
h : a = 0
⊢ natNorm a = 0
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
case mpr
a b c : ℤω
h : a = 0
⊢ natNorm a = 0
Tactic:
rw [h]
Proof state after:
case mpr
a b c : ℤω
h : a = 0
⊢ natNorm 0 = 0
Theorem: ℤω.natNorm_eq_zero_iff
Proof state before:
case mpr
a b c : ℤω
h : a = 0
⊢ natNorm 0 = 0
Tactic:
decide
Proof state after:
no goals
Theorem: ℤω.self_sub_round_sq
Proof state before:
a b c : ℤω
x : ℝ
⊢ (x - ↑(round x)) ^ 2 ≤ 2⁻¹ ^ 2
Tactic:
rw [sq_le_sq]
Proof state after:
a b c : ℤω
x : ℝ
⊢ |x - ↑(round x)| ≤ |2⁻¹|
Theorem: ℤω.self_sub_round_sq
Proof state before:
a b c : ℤω
x : ℝ
⊢ |x - ↑(round x)| ≤ |2⁻¹|
Tactic:
have bound := abs_sub_round x
Proof state after:
a b c : ℤω
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|
Theorem: ℤω.self_sub_round_sq
Proof state before:
a b c : ℤω
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|
Tactic:
have : |(2⁻¹ : ℝ)| = 1 / 2 := by
  simp only [one_div, abs_eq_self, inv_nonneg, zero_le_bit0, zero_le_one]
Proof state after:
a b c : ℤω
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
this : |2⁻¹| = 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|
Theorem: ℤω.self_sub_round_sq
Proof state before:
a b c : ℤω
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
this : |2⁻¹| = 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|
Tactic:
rwa [this]
Proof state after:
no goals
Theorem: ℤω.self_sub_round_sq
Proof state before:
a b c : ℤω
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ |2⁻¹| = 1 / 2
Tactic:
simp only [one_div, abs_eq_self, inv_nonneg, zero_le_bit0, zero_le_one]
Proof state after:
a b c : ℤω
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ 0 ≤ 2
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
have hc : c * c⁻¹ = 1 := by
  apply mul_inv_cancel
  exact ne_of_gt c_pos
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
have h_abs_c : |c| = c := abs_of_pos c_pos
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
have := abs_mul (c⁻¹ * x - round (c⁻¹ * x)) c
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |(c⁻¹ * x - ↑(round (c⁻¹ * x))) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |(c⁻¹ * x - ↑(round (c⁻¹ * x))) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [sub_mul] at this
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x * c - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x * c - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [mul_comm] at this
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c * (c⁻¹ * x) - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c * (c⁻¹ * x) - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [← mul_assoc] at this
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c * c⁻¹ * x - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c * c⁻¹ * x - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [hc, one_mul, mul_comm] at this
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |x - c * ↑(round (c⁻¹ * x))| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |x - c * ↑(round (c⁻¹ * x))| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [this]
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |x - c * ↑(round (c⁻¹ * x))| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |x - c * ↑(round (c⁻¹ * x))| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c
Tactic:
clear this
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c
Tactic:
have := abs_sub_round (c⁻¹ * x)
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c
Tactic:
rw [h_abs_c]
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * c ≤ 2⁻¹ * c
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * c ≤ 2⁻¹ * c
Tactic:
rw [mul_le_mul_right c_pos]
Proof state after:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 2⁻¹
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 2⁻¹
Tactic:
rwa [one_div] at this
Proof state after:
no goals
Theorem: ℤω.sub_hMul_round
Proof state before:
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
⊢ c * c⁻¹ = 1
Tactic:
apply mul_inv_cancel
Proof state after:
case h
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
⊢ c ≠ 0
Theorem: ℤω.sub_hMul_round
Proof state before:
case h
a b c✝ : ℤω
c x : ℝ
c_pos : c > 0
⊢ c ≠ 0
Tactic:
exact ne_of_gt c_pos
Proof state after:
no goals
Theorem: ℤω.im_sub_nearest
Proof state before:
a b c : ℤω
z : ℂ
⊢ (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
Tactic:
rw [sq_le_sq]
Proof state after:
a b c : ℤω
z : ℂ
⊢ |(z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im| ≤ |4⁻¹ * rt3|
Theorem: ℤω.im_sub_nearest
Proof state before:
a b c : ℤω
z : ℂ
⊢ |(z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im| ≤ |4⁻¹ * rt3|
Tactic:
cases' z with x y
Proof state after:
case mk
a b c : ℤω
x y : ℝ
⊢ |({ re := x, im := y } - OneHom.toFun (↑↑inclusion) (nearestℤω { re := x, im := y })).im| ≤ |4⁻¹ * rt3|
Theorem: ℤω.im_sub_nearest
Proof 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ℤω
Proof 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|
Theorem: ℤω.im_sub_nearest
Proof 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
Proof 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|
Theorem: ℤω.re_sub_nearest
Proof state before:
a b c : ℤω
z : ℂ
⊢ (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
Tactic:
rw [sq_le_sq]
Proof state after:
a b c : ℤω
z : ℂ
⊢ |(z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re| ≤ |2⁻¹|
Theorem: ℤω.re_sub_nearest
Proof state before:
a b c : ℤω
z : ℂ
⊢ |(z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re| ≤ |2⁻¹|
Tactic:
cases' z with x y
Proof state after:
case mk
a b c : ℤω
x y : ℝ
⊢ |({ re := x, im := y } - OneHom.toFun (↑↑inclusion) (nearestℤω { re := x, im := y })).re| ≤ |2⁻¹|
Theorem: ℤω.re_sub_nearest
Proof 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ℤω
Proof 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 })).re| ≤
    |2⁻¹|
Theorem: ℤω.re_sub_nearest
Proof 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 })).re| ≤
    |2⁻¹|
Tactic:
dsimp
Proof state after:
case mk
a b c : ℤω
x y : ℝ
⊢ |x - (↑inclusion { x := round (x + 2⁻¹ * ↑(round (2 * rt3⁻¹ * y))), y := round (2 * rt3⁻¹ * y) }).re| ≤ |2⁻¹|
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
a b c : ℤω
z : ℂ
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1
Tactic:
have hre := re_sub_nearest z
Proof state after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1
Tactic:
have him := im_sub_nearest z
Proof state after:
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
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1
Tactic:
unfold normSq
Proof state after:
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
⊢ ↑{ toZeroHom := { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1 },
          map_one' := normSq.proof_2, map_mul' := normSq.proof_3 }
      (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) <
    1
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
⊢ ↑{ toZeroHom := { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1 },
          map_one' := normSq.proof_2, map_mul' := normSq.proof_3 }
      (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) <
    1
Tactic:
dsimp
Proof state after:
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
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
Tactic:
simp only [← pow_two]
Proof state after:
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
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
Tactic:
have arith : (2 : ℝ)⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1 :=
  by
  ring_nf
  simp only [one_div, rt3_sq]
  norm_num
Proof state after:
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
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Tactic:
have near := add_le_add hre him
Proof state after:
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
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
near :
  (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤
    2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
near :
  (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤
    2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Tactic:
have := lt_of_le_of_lt near arith
Proof state after:
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
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
near :
  (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤
    2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2
this : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
near :
  (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤
    2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2
this : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Tactic:
clear near arith hre him
Proof state after:
a b c : ℤω
z : ℂ
this : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
a b c : ℤω
z : ℂ
this : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Tactic:
rwa [sub_re, sub_im] at this
Proof state after:
no goals
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
⊢ 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
Tactic:
ring_nf
Proof state after:
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
⊢ ↑(ofNat 1) / ↑4 + rt3 ^ 2 * (↑(ofNat 1) / ↑16) < 1
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
⊢ ↑(ofNat 1) / ↑4 + rt3 ^ 2 * (↑(ofNat 1) / ↑16) < 1
Tactic:
simp only [one_div, rt3_sq]
Proof state after:
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
⊢ ↑(ofNat 1) / ↑4 + 3 * (↑(ofNat 1) / ↑16) < 1
Theorem: ℤω.norm_sub_nearestℤω_self_lt
Proof state before:
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
⊢ ↑(ofNat 1) / ↑4 + 3 * (↑(ofNat 1) / ↑16) < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤω.div_add_mod
Proof state before:
a b c : ℤω
⊢ b * (a / b) + a % b = a
Tactic:
change b * div a b + mod a b = a
Proof state after:
a b c : ℤω
⊢ b * div a b + mod a b = a
Theorem: ℤω.div_add_mod
Proof state before:
a b c : ℤω
⊢ b * div a b + mod a b = a
Tactic:
simp [mod]
Proof state after:
no goals
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
⊢ natNorm (mod a b) < natNorm b
Tactic:
suffices Complex.normSq (mod a b) < normSq b
  by
  simp only [natNorm_coe] at this
  exact_mod_cast this
Proof state after:
a b c : ℤω
h : b ≠ 0
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) (mod a b)) < ↑normSq (OneHom.toFun (↑↑inclusion) b)
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) (mod a b)) < ↑normSq (OneHom.toFun (↑↑inclusion) b)
Tactic:
simp [mod, div]
Proof state after:
a b c : ℤω
h : b ≠ 0
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
have bound : Complex.normSq (a / b - nearestℤω (a / b)) < 1 :=
  norm_sub_nearestℤω_self_lt (a / b : ℂ)
Proof state after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Theorem: ℤω.normSq_mod_lt
Proof state before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
have : (a / b : ℂ) - nearestℤω (a / b) = (a - nearestℤω (a / b) * b) * b⁻¹ :=
  by
  ring_nf
  have : (b : ℂ) * (b : ℂ)⁻¹ = 1 := by
    apply mul_inv_cancel
    simpa [coe_eq_zero] using h
  congr
  rw [mul_comm (b : ℂ)]
  rw [_root_.mul_assoc]
  rw [this]
  rw [_root_.mul_one]
Proof state after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this :
  OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)