awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
rwa : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₁ : |ξ - HDiv.hDiv (α := ℝ) (↑(↑j : ℚ) : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₂ : |ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑k : ℝ) ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rwa₃ : |ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑k : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rwa [← abs_of_pos hk₀', Rat.cast_div, Rat.cast_intCast, Rat.cast_intCast, ← abs_mul, sub_mul,
    div_mul_cancel₀ _ hk₀'.ne', mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
rwa : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₁ : |ξ - HDiv.hDiv (α := ℝ) (↑(↑j : ℚ) : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₂ : |ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₃ : |ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑k : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑k : ℝ) ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rwa₄ : |(ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑k : ℝ)) * (↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rwa [← abs_of_pos hk₀', Rat.cast_div, Rat.cast_intCast, Rat.cast_intCast, ← abs_mul, sub_mul,
    div_mul_cancel₀ _ hk₀'.ne', mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
rwa : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₁ : |ξ - HDiv.hDiv (α := ℝ) (↑(↑j : ℚ) : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₂ : |ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₃ : |ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑k : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₄ : |(ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑k : ℝ)) * (↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑k : ℝ) ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rwa₅ : |ξ * (↑k : ℝ) - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑k : ℝ) * (↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rwa [← abs_of_pos hk₀', Rat.cast_div, Rat.cast_intCast, Rat.cast_intCast, ← abs_mul, sub_mul,
    div_mul_cancel₀ _ hk₀'.ne', mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ (↑n : ℤ)
h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk₀' : LT.lt (α := ℝ) 0 (↑k : ℝ)
hden : (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k
rwa : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₁ : |ξ - HDiv.hDiv (α := ℝ) (↑(↑j : ℚ) : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₂ : |ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑(↑k : ℚ) : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₃ : |ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑k : ℝ)| * |(↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₄ : |(ξ - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑k : ℝ)) * (↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₅ : |ξ * (↑k : ℝ) - HDiv.hDiv (α := ℝ) (↑j : ℝ) (↑k : ℝ) * (↑k : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑k : ℝ) ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have rwa₆ : |ξ * (↑k : ℝ) - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rwa [← abs_of_pos hk₀', Rat.cast_div, Rat.cast_intCast, Rat.cast_intCast, ← abs_mul, sub_mul,
    div_mul_cancel₀ _ hk₀'.ne', mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
⊢ ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
have h : 0 < |ξ - (↑q : ℝ)|
Tactic: have h := abs_pos.mpr (sub_ne_zero.mpr <| Irrational.ne_rat hξ q)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
⊢ ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
have obtain : ∀ (m : ℕ) (hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)),
  ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
Tactic: obtain ⟨m, hm⟩ := exists_nat_gt (1 / |ξ - q|)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
m : ℕ
hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)
⊢ ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
have m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
Tactic: have m_pos : (0 : ℝ) < m := (one_div_pos.mpr h).trans hm
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
m : ℕ
hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
⊢ ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
have obtain : ∀ (q' : ℚ) (hbd : |ξ - (↑q' : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ))) (hden : q'.den ≤ m),
  ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
Tactic: obtain ⟨q', hbd, hden⟩ := exists_rat_abs_sub_le_and_den_le ξ (Nat.cast_pos.mp m_pos)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
m : ℕ
hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
q' : ℚ
hbd : |ξ - (↑q' : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ))
hden : q'.den ≤ m
⊢ ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
have den_pos : LT.lt (α := ℝ) 0 (↑q'.den : ℝ)
Tactic: have den_pos : (0 : ℝ) < q'.den := Nat.cast_pos.mpr q'.pos
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
m : ℕ
hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
q' : ℚ
hbd : |ξ - (↑q' : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ))
hden : q'.den ≤ m
den_pos : LT.lt (α := ℝ) 0 (↑q'.den : ℝ)
⊢ ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
have md_pos : 0 < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ)
Tactic: have md_pos := mul_pos (add_pos m_pos zero_lt_one) den_pos
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
m : ℕ
hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
q' : ℚ
hbd : |ξ - (↑q' : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ))
hden : q'.den ≤ m
den_pos : LT.lt (α := ℝ) 0 (↑q'.den : ℝ)
md_pos : 0 < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ)
⊢ ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
have lt_of_le_of_lt : 1 / (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ)) < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2
Tactic: refine
    ⟨q', lt_of_le_of_lt hbd ?_,
      lt_of_le_of_lt hbd <|
        (one_div_lt md_pos h).mpr <|
          hm.trans <|
            lt_of_lt_of_le (lt_add_one _) <|
              (le_mul_iff_one_le_right <| add_pos m_pos zero_lt_one).mpr <|
                mod_cast (q'.pos : 1 ≤ q'.den)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
m : ℕ
hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
q' : ℚ
hbd : |ξ - (↑q' : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ))
hden : q'.den ≤ m
den_pos : LT.lt (α := ℝ) 0 (↑q'.den : ℝ)
md_pos : 0 < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ)
⊢ 1 / (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ)) < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2
have rw : (↑q'.den : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
Tactic: rw [sq, one_div_lt_one_div md_pos (mul_pos den_pos den_pos), mul_lt_mul_iff_left₀ den_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
hξ : Irrational ξ
⊢ Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
have refine : ∀ (h : Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}), False
Tactic: refine Or.resolve_left (Set.finite_or_infinite _) fun h => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
hξ : Irrational ξ
h : Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
⊢ False
have obtain : ∀ (q : ℚ),
  Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q →
    ∀
      (hq :
        ∀ (b : ℚ),
          Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} b →
            |ξ - (↑q : ℝ)| ≤ |ξ - (↑b : ℝ)|),
      False
Tactic: obtain ⟨q, _, hq⟩ :=
    exists_min_image {q : ℚ | |ξ - q| < 1 / (q.den : ℝ) ^ 2} (fun q => |ξ - q|) h
      ⟨⌊ξ⌋, by simp [abs_of_nonneg, Int.fract_lt_one]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
hξ : Irrational ξ
h : Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
q : ℚ
left : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
hq :
  ∀ (b : ℚ),
    Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} b →
      |ξ - (↑q : ℝ)| ≤ |ξ - (↑b : ℝ)|
⊢ False
have obtain : ∀ (q' : ℚ) (hmem : |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2)
  (hbetter : |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|), False
Tactic: obtain ⟨q', hmem, hbetter⟩ := exists_rat_abs_sub_lt_and_lt_of_irrational hξ q
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
h : |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
⊢ q.den ≤ ξ.den ∧ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
Tactic: have hq₀ : (0 : ℚ) < q.den := Nat.cast_pos.mpr q.pos
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
h : |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
⊢ |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
have h₁ : |ξ - q| * (↑q.den : ℚ) < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
Tactic: rw [← mul_lt_mul_iff_left₀ hq₀] at h
Cleared hypotheses: h, hq₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
h : |ξ - q| * (↑q.den : ℚ) < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
| |ξ - q| * (↑q.den : ℚ)
have rw : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)|
Tactic: rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
h : |ξ - q| * (↑q.den : ℚ) < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
⊢ |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
have h₁ : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
Tactic: conv_lhs at h => rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]
Cleared hypotheses: h, hq₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
⊢ |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
have rwa : ∀ (h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / HMul.hMul (α := ℚ) (↑q.den : ℚ) (↑q.den : ℚ) * (↑q.den : ℚ))
  (hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)), |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
Tactic: rwa [sq, div_mul, mul_div_cancel_left₀ _ hq₀.ne'] at h
Cleared hypotheses: h, hq₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
rwa :
  ∀ (h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / HMul.hMul (α := ℚ) (↑q.den : ℚ) (↑q.den : ℚ) * (↑q.den : ℚ))
    (hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)), |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
⊢ |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
have rwa₁ : ∀ (h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / (HMul.hMul (α := ℚ) (↑q.den : ℚ) (↑q.den : ℚ) / (↑q.den : ℚ)))
  (hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)), |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
Tactic: rwa [sq, div_mul, mul_div_cancel_left₀ _ hq₀.ne'] at h
Cleared hypotheses: h, hq₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
rwa :
  ∀ (h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / HMul.hMul (α := ℚ) (↑q.den : ℚ) (↑q.den : ℚ) * (↑q.den : ℚ))
    (hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)), |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
rwa₁ :
  ∀ (h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / (HMul.hMul (α := ℚ) (↑q.den : ℚ) (↑q.den : ℚ) / (↑q.den : ℚ)))
    (hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)), |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
⊢ |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
have rwa₂ : ∀ (h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)) (hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)),
  |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
Tactic: rwa [sq, div_mul, mul_div_cancel_left₀ _ hq₀.ne'] at h
Cleared hypotheses: h, hq₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
h : |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
⊢ q.den ≤ ξ.den ∧ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have h₁ : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
Tactic: replace h : |ξ * q.den - q.num| < 1 / q.den := by
    rw [← mul_lt_mul_iff_left₀ hq₀] at h
    conv_lhs at h => rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]
    rwa [sq, div_mul, mul_div_cancel_left₀ _ hq₀.ne'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
⊢ q.den ≤ ξ.den ∧ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have left : q.den ≤ ξ.den
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
left : q.den ≤ ξ.den
⊢ q.den ≤ ξ.den ∧ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have right : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
⊢ q.den ≤ ξ.den
have left : ∀ (hq₀ : LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)) (h : |ξ * (↑ξ.den : ℚ) - (↑ξ.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑ξ.den : ℚ)),
  ξ.den ≤ ξ.den
Tactic: rcases eq_or_ne ξ q with (rfl | H)
Cleared hypotheses: q, hq₀, h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
left :
  ∀ (hq₀ : LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)) (h : |ξ * (↑ξ.den : ℚ) - (↑ξ.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑ξ.den : ℚ)),
    ξ.den ≤ ξ.den
⊢ q.den ≤ ξ.den
have left₁ : ∀ (H : ξ ≠ q), q.den ≤ ξ.den
Tactic: rcases eq_or_ne ξ q with (rfl | H)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
H : ξ ≠ q
⊢ q.den ≤ ξ.den
have hξ₀ : LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)
Tactic: have hξ₀ : (0 : ℚ) < ξ.den := Nat.cast_pos.mpr ξ.pos
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
H : ξ ≠ q
hξ₀ : LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)
⊢ q.den ≤ ξ.den
have h₁ : |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)| <
  HDiv.hDiv (α := ℚ) (↑ξ.den : ℚ) (↑q.den : ℚ)
Tactic: rw [← Rat.num_div_den ξ, div_mul_eq_mul_div, div_sub' hξ₀.ne', abs_div, abs_of_pos hξ₀,
        div_lt_iff₀ hξ₀, div_mul_comm, mul_one] at h
Cleared hypotheses: h, H, hξ₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h :
  |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)| <
    HDiv.hDiv (α := ℚ) (↑ξ.den : ℚ) (↑q.den : ℚ)
H : ξ ≠ q
hξ₀ : LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)
⊢ q.den ≤ ξ.den
have left : 1 ≤ |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)|
Tactic: refine Nat.cast_le.mp ((one_lt_div hq₀).mp <| lt_of_le_of_lt ?_ h).le
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h :
  |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)| <
    HDiv.hDiv (α := ℚ) (↑ξ.den : ℚ) (↑q.den : ℚ)
H : ξ ≠ q
hξ₀ : LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)
⊢ 1 ≤ |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)|
have left : 1 ≤ |ξ.num * (↑q.den : ℤ) - (↑ξ.den : ℤ) * q.num|
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h :
  |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)| <
    HDiv.hDiv (α := ℚ) (↑ξ.den : ℚ) (↑q.den : ℚ)
H : ξ ≠ q
hξ₀ : LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)
⊢ 1 ≤ |ξ.num * (↑q.den : ℤ) - (↑ξ.den : ℤ) * q.num|
have left : 1 ≤ |ξ.num * (↑q.den : ℤ) - q.num * (↑ξ.den : ℤ)|
Tactic: rw [mul_comm _ q.num]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have h₁ : ξ * (↑q.den : ℚ) - (↑q.num : ℚ) < 1
Tactic: obtain ⟨h₁, h₂⟩ :=
      abs_sub_lt_iff.mp
        (h.trans_le <|
          (one_div_le zero_lt_one hq₀).mp <| (@one_div_one ℚ _).symm ▸ Nat.cast_le.mpr q.pos)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
h₁ : ξ * (↑q.den : ℚ) - (↑q.num : ℚ) < 1
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have h₂ : (↑q.num : ℚ) - ξ * (↑q.den : ℚ) < 1
Tactic: obtain ⟨h₁, h₂⟩ :=
      abs_sub_lt_iff.mp
        (h.trans_le <|
          (one_div_le zero_lt_one hq₀).mp <| (@one_div_one ℚ _).symm ▸ Nat.cast_le.mpr q.pos)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
h₁ : ξ * (↑q.den : ℚ) - (↑q.num : ℚ) < 1
h₂ : (↑q.num : ℚ) - ξ * (↑q.den : ℚ) < 1
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have h₃ : ξ * (↑q.den : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1
Tactic: rw [sub_lt_iff_lt_add, add_comm] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
h₁ : ξ * (↑q.den : ℚ) - (↑q.num : ℚ) < 1
h₂ : (↑q.num : ℚ) - ξ * (↑q.den : ℚ) < 1
h₃ : ξ * (↑q.den : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have h₄ : (↑q.num : ℚ) < ξ * (↑q.den : ℚ) + 1
Tactic: rw [sub_lt_iff_lt_add, add_comm] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
h₁ : ξ * (↑q.den : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1
h₂ : (↑q.num : ℚ) < ξ * (↑q.den : ℚ) + 1
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have h₃ : HSub.hSub (α := ℚ) (↑q.num : ℚ) 1 < ξ * (↑q.den : ℚ)
Tactic: rw [← sub_lt_iff_lt_add] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
h₁ : ξ * (↑q.den : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1
h₂ : HSub.hSub (α := ℚ) (↑q.num : ℚ) 1 < ξ * (↑q.den : ℚ)
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have h₃ : ξ * (↑q.den : ℚ) < (↑(q.num + 1) : ℚ)
Tactic: norm_cast at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
h₁ : ξ * (↑q.den : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1
h₂ : HSub.hSub (α := ℚ) (↑q.num : ℚ) 1 < ξ * (↑q.den : ℚ)
h₃ : ξ * (↑q.den : ℚ) < (↑(q.num + 1) : ℚ)
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
have h₄ : (↑(q.num - 1) : ℚ) < ξ * (↑q.den : ℚ)
Tactic: norm_cast at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
a b : ℚ
hab : f a = f b
⊢ a = b
have hab₁ : a.num = b.num ∧ a.den = b.den
Tactic: simp only [f, Prod.mk_inj] at hab
Cleared hypotheses: hab