internlm/Lean-Github huggingface dataset:
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x 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 := x, w := y }).re ^
        2 +
      (↑{ 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 := x, w := y }).im ^
        2 =
    ↑(x * y + x ^ 2 + y ^ 2 * 2)
Tactic:
simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, cast_add, cast_mul,
cast_pow, int_cast_ofNat,toℂ]
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * complexα).re ^ 2 + (↑x + ↑y * complexα).im ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * complexα).re ^ 2 + (↑x + ↑y * complexα).im ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
simp only [complexα,re_of_coe, im_of_coe]
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).re ^ 2 + (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).im ^ 2 =
    ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).re ^ 2 + (↑x + ↑y * { re := 1 / 2, im := rt7 / 2 }).im ^ 2 =
    ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
ring_nf
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).re ^ 2 +
      (↑x + ↑y * { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).im ^ 2 =
    ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).re ^ 2 +
      (↑x + ↑y * { re := ↑(ofNat 1) / ↑2, im := rt7 * (↑(ofNat 1) / ↑2) }).im ^ 2 =
    ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
norm_num
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * (1 / 2)) ^ 2 + (↑y * (rt7 * (1 / 2))) ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * (1 / 2)) ^ 2 + (↑y * (rt7 * (1 / 2))) ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
rw [pow_two]
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * (1 / 2)) * (↑x + ↑y * (1 / 2)) + (↑y * (rt7 * (1 / 2))) ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ (↑x + ↑y * (1 / 2)) * (↑x + ↑y * (1 / 2)) + (↑y * (rt7 * (1 / 2))) ^ 2 = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
ring
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * rt7 ^ 2 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * rt7 ^ 2 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
rw [rt7_sq]
Proof state after:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * 7 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Theorem: ℤα.normSq_coe
Proof state before:
case mk
b c : ℤα
x y : ℤ
⊢ ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * (↑(ofNat 1) / ↑4) + ↑y ^ 2 * 7 * (↑(ofNat 1) / ↑4) = ↑x * ↑y + ↑x ^ 2 + ↑y ^ 2 * 2
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ℤα.natNorm_coe
Proof state before:
a b c : ℤα
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(natNorm a)
Tactic:
unfold natNorm
Proof state after:
a b c : ℤα
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(natAbs (norm a))
Theorem: ℤα.natNorm_coe
Proof state before:
a b c : ℤα
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) a) = ↑(natAbs (norm a))
Tactic:
rw [normSq_coe]
Proof state after:
a b c : ℤα
⊢ ↑(norm a) = ↑(natAbs (norm a))
Theorem: ℤα.natNorm_coe
Proof state before:
a b c : ℤα
⊢ ↑(norm a) = ↑(natAbs (norm a))
Tactic:
suffices h : a.norm = a.norm.natAbs
Proof state after:
a b c : ℤα
h : norm a = ↑(natAbs (norm a))
⊢ ↑(norm a) = ↑(natAbs (norm a))

case h
a b c : ℤα
⊢ norm a = ↑(natAbs (norm a))
Theorem: ℤα.natNorm_coe
Proof state before:
a b c : ℤα
h : norm a = ↑(natAbs (norm a))
⊢ ↑(norm a) = ↑(natAbs (norm a))

case h
a b c : ℤα
⊢ norm a = ↑(natAbs (norm a))
Tactic:
congr
Proof state after:
case h
a b c : ℤα
⊢ norm a = ↑(natAbs (norm a))
Theorem: ℤα.natNorm_coe
Proof state before:
case h
a b c : ℤα
⊢ norm a = ↑(natAbs (norm a))
Tactic:
norm_cast
Proof state after:
case h
a b c : ℤα
⊢ norm a = |norm a|
Theorem: ℤα.natNorm_coe
Proof state before:
case h
a b c : ℤα
⊢ norm a = |norm a|
Tactic:
exact this
Proof state after:
no goals
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
⊢ norm v = ↑(natNorm v)
Tactic:
unfold natNorm
Proof state after:
a b c v : ℤα
⊢ norm v = ↑(natAbs (norm v))
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
⊢ norm v = ↑(natAbs (norm v))
Tactic:
have p : 0 ≤ (norm v : ℝ) := by
  rw [← normSq_coe]
  exact normSq_nonneg _
Proof state after:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
⊢ norm v = ↑(natAbs (norm v))
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
⊢ norm v = ↑(natAbs (norm v))
Tactic:
have h : 0 ≤ norm v := by exact_mod_cast p
Proof state after:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : 0 ≤ norm v
⊢ norm v = ↑(natAbs (norm v))
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : 0 ≤ norm v
⊢ norm v = ↑(natAbs (norm v))
Tactic:
rw [← abs_eq_self] at h
Proof state after:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ norm v = ↑(natAbs (norm v))
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ norm v = ↑(natAbs (norm v))
Tactic:
norm_cast
Proof state after:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ norm v = |norm v|
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ norm v = |norm v|
Tactic:
symm
Proof state after:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ |norm v| = norm v
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
h : |norm v| = norm v
⊢ |norm v| = norm v
Tactic:
exact h
Proof state after:
no goals
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
⊢ 0 ≤ ↑(norm v)
Tactic:
rw [← normSq_coe]
Proof state after:
a b c v : ℤα
⊢ 0 ≤ ↑normSq (OneHom.toFun (↑↑inclusion) v)
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
⊢ 0 ≤ ↑normSq (OneHom.toFun (↑↑inclusion) v)
Tactic:
exact normSq_nonneg _
Proof state after:
no goals
Theorem: ℤα.equiv_norms
Proof state before:
a b c v : ℤα
p : 0 ≤ ↑(norm v)
⊢ 0 ≤ norm v
Tactic:
exact_mod_cast p
Proof state after:
no goals
Theorem: ℤα.norm_hMul
Proof state before:
a b c : ℤα
⊢ norm (a * b) = norm a * norm b
Tactic:
have := normSq_mul a b
Proof state after:
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ norm (a * b) = norm a * norm b
Theorem: ℤα.norm_hMul
Proof state before:
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ norm (a * b) = norm a * norm b
Tactic:
rw [← coe_hMul] at this
Proof state after:
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ norm (a * b) = norm a * norm b
Theorem: ℤα.norm_hMul
Proof state before:
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ norm (a * b) = norm a * norm b
Tactic:
simp only [normSq_coe] at this
Proof state after:
a b c : ℤα
this : ↑(norm (a * b)) = ↑(norm a) * ↑(norm b)
⊢ norm (a * b) = norm a * norm b
Theorem: ℤα.norm_hMul
Proof state before:
a b c : ℤα
this : ↑(norm (a * b)) = ↑(norm a) * ↑(norm b)
⊢ norm (a * b) = norm a * norm b
Tactic:
exact_mod_cast this
Proof state after:
no goals
Theorem: ℤα.natNorm_hMul
Proof state before:
a b c : ℤα
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
have := normSq_mul a b
Proof state after:
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Theorem: ℤα.natNorm_hMul
Proof state before:
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) a * OneHom.toFun (↑↑inclusion) b) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
rw [← coe_hMul] at this
Proof state after:
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Theorem: ℤα.natNorm_hMul
Proof state before:
a b c : ℤα
this :
  ↑normSq (OneHom.toFun (↑↑inclusion) (a * b)) =
    ↑normSq (OneHom.toFun (↑↑inclusion) a) * ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
simp only [natNorm_coe] at this
Proof state after:
a b c : ℤα
this : ↑(natNorm (a * b)) = ↑(natNorm a) * ↑(natNorm b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Theorem: ℤα.natNorm_hMul
Proof state before:
a b c : ℤα
this : ↑(natNorm (a * b)) = ↑(natNorm a) * ↑(natNorm b)
⊢ natNorm (a * b) = natNorm a * natNorm b
Tactic:
exact_mod_cast this
Proof state after:
no goals
Theorem: ℤα.natNorm_eq_zero_iff
Proof state before:
a b c : ℤα
⊢ natNorm a = 0 ↔ a = 0
Tactic:
constructor
Proof state after:
case mp
a b c : ℤα
⊢ natNorm a = 0 → a = 0

case mpr
a b c : ℤα
⊢ a = 0 → natNorm a = 0
Theorem: ℤα.natNorm_eq_zero_iff
Proof state before:
case mp
a b c : ℤα
⊢ natNorm a = 0 → a = 0
Tactic:
intro h
Proof state after:
case mp
a b c : ℤα
h : natNorm a = 0
⊢ a = 0
Theorem: ℤα.natNorm_eq_zero_iff
Proof state before:
case mp
a b c : ℤα
h : natNorm a = 0
⊢ a = 0
Tactic:
have : (a.natNorm : ℝ) = 0 := by exact_mod_cast h
Proof state after:
case mp
a b c : ℤα
h : natNorm a = 0
this : ↑(natNorm a) = 0
⊢ a = 0
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]
  norm_num
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: ℤα.self_sub_round_sq
Proof state before:
a b c : ℤα
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
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⁻¹ * rt7) ^ 2
Tactic:
rw [sq_le_sq]
Proof state after:
a b c : ℤα
z : ℂ
⊢ |(z - OneHom.toFun (↑↑inclusion) (nearestℤα z)).im| ≤ |4⁻¹ * rt7|
Theorem: ℤα.im_sub_nearest
Proof state before:
a b c : ℤα
z : ℂ
⊢ |(z - OneHom.toFun (↑↑inclusion) (nearestℤα z)).im| ≤ |4⁻¹ * rt7|
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⁻¹ * rt7|
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⁻¹ * rt7|
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 * rt7⁻¹ * { re := x, im := y }.im);
            { z := round ({ re := x, im := y }.re - 2⁻¹ * ↑y_1), w := y_1 })).im| ≤
    |4⁻¹ * rt7|
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 * rt7⁻¹ * { re := x, im := y }.im);
            { z := round ({ re := x, im := y }.re - 2⁻¹ * ↑y_1), w := y_1 })).im| ≤
    |4⁻¹ * rt7|
Tactic:
dsimp
Proof 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|
Theorem: ℤα.im_sub_nearest
Proof 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]
Proof 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|
Theorem: ℤα.im_sub_nearest
Proof 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α]
Proof 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|
Theorem: ℤα.im_sub_nearest
Proof 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
Proof state after:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |1 / 4 * rt7|
Theorem: ℤα.im_sub_nearest
Proof state before:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |1 / 4 * rt7|
Tactic:
simp only [one_div]
Proof state after:
case mk
a b c : ℤα
x y : ℝ
⊢ |y - ↑(round (2 * rt7⁻¹ * y)) * (rt7 / 2)| ≤ |4⁻¹ * rt7|
Theorem: ℤα.im_sub_nearest
Proof 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)
Proof 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|
Theorem: ℤα.im_sub_nearest
Proof 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
Proof 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|
Theorem: ℤα.im_sub_nearest
Proof 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
Proof 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|
Theorem: ℤα.im_sub_nearest
Proof 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
Proof 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|
Theorem: ℤα.im_sub_nearest
Proof state before:
a b c : ℤα
x y : ℝ
⊢ 2⁻¹ * rt7 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤα.im_sub_nearest
Proof 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
Proof 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)|