awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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
rwa₆ : |ξ * (↑k : ℝ) - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rwa₇ rwa₈ rwa₉ rwa₁₀ : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |ξ - (↑(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]

Premises used: Rat.cast_intCast, div_mul_cancel₀, abs_mul, Rat.cast_div, LT.lt.ne', sub_mul, mul_comm, abs_of_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
⊢ 0 < |ξ - (↑q : ℝ)|

Tactic:
have h := abs_pos.mpr (sub_ne_zero.mpr <| Irrational.ne_rat hξ q)
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
obtain :
  ∀ (m : ℕ) (hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)),
    ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
⊢ ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|

Tactic:
obtain ⟨m, hm⟩ := exists_nat_gt (1 / |ξ - q|)

Premises used: abs, HSub.hSub, HDiv.hDiv, Rat.cast, exists_nat_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
m : ℕ
hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑m : ℝ)

Tactic:
have m_pos : (0 : ℝ) < m := (one_div_pos.mpr h).trans hm
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - (↑q : ℝ)|
m : ℕ
hm : 1 / |ξ - (↑q : ℝ)| < (↑m : ℝ)
m_pos : LT.lt (α := ℝ) 0 (↑m : ℝ)
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 : ℝ)|
⊢ ∃ (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)

Premises used: Nat.cast_pos, Real.exists_rat_abs_sub_le_and_den_le, Iff.mp
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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
⊢ LT.lt (α := ℝ) 0 (↑q'.den : ℝ)

Tactic:
have den_pos : (0 : ℝ) < q'.den := Nat.cast_pos.mpr q'.pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
⊢ 0 < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ)

Tactic:
have md_pos := mul_pos (add_pos m_pos zero_lt_one) den_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)|

Tactic:
⟨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)⟩

Premises used: Iff.mpr, lt_of_le_of_lt, Rat.pos, le_mul_iff_one_le_right, congrArg, lt_add_one, add_pos, cast, Rat.den, one_div_lt, Nat.cast_le._simp_1, LE.le, Nat.cast, zero_lt_one, And.intro, Exists.intro, LT.lt.trans, congrFun', Eq.symm, Nat.cast_one, Eq.trans, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
lt_of_le_of_lt : 1 / (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ)) < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2
⊢ ∃ (q' : ℚ), |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2 ∧ |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|

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)⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
rw : (↑q'.den : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1
⊢ 1 / (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (↑q'.den : ℝ)) < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2

Tactic:
rw [sq, one_div_lt_one_div md_pos (mul_pos den_pos den_pos), mul_lt_mul_iff_left₀ den_pos]

Premises used: sq, mul_pos, one_div_lt_one_div, mul_lt_mul_iff_left₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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'.den : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
lt_add_of_le_of_pos (Nat.cast_le.mpr hden) zero_lt_one

Premises used: Iff.mpr, zero_lt_one, lt_add_of_le_of_pos, Nat.cast_le
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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'.den : ℝ) < HAdd.hAdd (α := ℝ) (↑m : ℝ) 1

Tactic:
exact lt_add_of_le_of_pos (Nat.cast_le.mpr hden) zero_lt_one

Premises used: Iff.mpr, zero_lt_one, lt_add_of_le_of_pos, Nat.cast_le
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
hξ : Irrational ξ
⊢ Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}

Tactic:
Or.resolve_left (Set.finite_or_infinite _) fun h => ?_

Premises used: Set.finite_or_infinite, Or.resolve_left
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
hξ : Irrational ξ
refine : ∀ (h : Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}), False
⊢ Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}

Tactic:
refine Or.resolve_left (Set.finite_or_infinite _) fun h => ?_

Premises used: Set.finite_or_infinite, Or.resolve_left
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
hξ : Irrational ξ
h : Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
⊢ Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} (↑⌊ξ⌋ : ℚ)

Tactic:
simp [abs_of_nonneg, Int.fract_lt_one]

Premises used: Int.fract_lt_one, abs_of_nonneg
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
hξ : Irrational ξ
h : Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
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
⊢ 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]⟩

Premises used: Int.cast, Int.floor, abs, setOf, HSub.hSub, Rat.den, Set.exists_min_image, HDiv.hDiv, Rat.cast, Nat.cast, HPow.hPow, LT.lt, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)|
obtain :
  ∀ (q' : ℚ) (hmem : |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2)
    (hbetter : |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|), False
⊢ False

Tactic:
obtain ⟨q', hmem, hbetter⟩ := exists_rat_abs_sub_lt_and_lt_of_irrational hξ q

Premises used: Real.exists_rat_abs_sub_lt_and_lt_of_irrational
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)|
q' : ℚ
hmem : |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2
hbetter : |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
⊢ False

Tactic:
lt_irrefl _ (lt_of_le_of_lt (hq q' hmem) hbetter)

Premises used: lt_of_le_of_lt, lt_irrefl
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)|
q' : ℚ
hmem : |ξ - (↑q' : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q'.den : ℝ) 2
hbetter : |ξ - (↑q' : ℝ)| < |ξ - (↑q : ℝ)|
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_le_of_lt (hq q' hmem) hbetter)

Premises used: lt_of_le_of_lt, lt_irrefl
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ q : ℚ
h : |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
⊢ LT.lt (α := ℚ) 0 (↑q.den : ℚ)

Tactic:
have hq₀ : (0 : ℚ) < q.den := Nat.cast_pos.mpr q.pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ q : ℚ
h : |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
⊢ |ξ - q| * (↑q.den : ℚ) < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)

Tactic:
rw [← mul_lt_mul_iff_left₀ hq₀] at h

Premises used: mul_lt_mul_iff_left₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ q : ℚ
h : |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h₁ : |ξ - q| * (↑q.den : ℚ) < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
⊢ LT.lt (α := ℚ) 0 (↑q.den : ℚ)

Tactic:
rw [← mul_lt_mul_iff_left₀ hq₀] at h

Premises used: mul_lt_mul_iff_left₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ q : ℚ
h : |ξ - q| * (↑q.den : ℚ) < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
rw : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)|
| |ξ - q| * (↑q.den : ℚ)

Tactic:
rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]

Premises used: abs_mul, sub_mul, Rat.mul_den_eq_num, abs_of_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ q : ℚ
h : |ξ - q| * (↑q.den : ℚ) < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
⊢ |ξ * (↑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]

Premises used: abs_mul, sub_mul, Rat.mul_den_eq_num, abs_of_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ q : ℚ
h : |ξ - q| * (↑q.den : ℚ) < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h₁ : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2 * (↑q.den : ℚ)
⊢ LT.lt (α := ℚ) 0 (↑q.den : ℚ)

Tactic:
conv_lhs at h => rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]

Premises used: abs_mul, sub_mul, Rat.mul_den_eq_num, abs_of_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℚ)
rwa₂ rwa₃ rwa₄ 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 : ℚ)
⊢ |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)

Tactic:
rwa [sq, div_mul, mul_div_cancel_left₀ _ hq₀.ne'] at h

Premises used: mul_div_cancel_left₀, div_mul, sq, LT.lt.ne'
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℚ)

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
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
left : q.den ≤ ξ.den
right : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
⊢ q.den ≤ ξ.den ∧ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1

Tactic:
constructor
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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
left₁ : ∀ (H : ξ ≠ q), q.den ≤ ξ.den
⊢ q.den ≤ ξ.den

Tactic:
rcases eq_or_ne ξ q with (rfl | H)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)
h : |ξ * (↑ξ.den : ℚ) - (↑ξ.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑ξ.den : ℚ)
⊢ ξ.den ≤ ξ.den

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)
h : |ξ * (↑ξ.den : ℚ) - (↑ξ.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑ξ.den : ℚ)
⊢ ξ.den ≤ ξ.den

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
H : ξ ≠ q
⊢ LT.lt (α := ℚ) 0 (↑ξ.den : ℚ)

Tactic:
have hξ₀ : (0 : ℚ) < ξ.den := Nat.cast_pos.mpr ξ.pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℚ)
⊢ |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

Premises used: Rat.num_div_den, abs_div, div_mul_eq_mul_div, div_lt_iff₀, LT.lt.ne', div_mul_comm, div_sub', abs_of_pos, mul_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℚ)
h₁ :
  |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)| <
    HDiv.hDiv (α := ℚ) (↑ξ.den : ℚ) (↑q.den : ℚ)
⊢ ξ ≠ q

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

Premises used: Rat.num_div_den, abs_div, div_mul_eq_mul_div, div_lt_iff₀, LT.lt.ne', div_mul_comm, div_sub', abs_of_pos, mul_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℚ)
h₁ :
  |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)| <
    HDiv.hDiv (α := ℚ) (↑ξ.den : ℚ) (↑q.den : ℚ)
H₁ : ξ ≠ q
⊢ LT.lt (α := ℚ) 0 (↑ξ.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

Premises used: Rat.num_div_den, abs_div, div_mul_eq_mul_div, div_lt_iff₀, LT.lt.ne', div_mul_comm, div_sub', abs_of_pos, mul_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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

Tactic:
Nat.cast_le.mp ((one_lt_div hq₀).mp <| lt_of_le_of_lt ?_ h).le

Premises used: lt_of_le_of_lt, one_lt_div, LT.lt.le, Iff.mp, Nat.cast_le
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℚ)
left : 1 ≤ |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)|
⊢ q.den ≤ ξ.den

Tactic:
refine Nat.cast_le.mp ((one_lt_div hq₀).mp <| lt_of_le_of_lt ?_ h).le

Premises used: lt_of_le_of_lt, one_lt_div, LT.lt.le, Iff.mp, Nat.cast_le
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℚ)
left : 1 ≤ |ξ.num * (↑q.den : ℤ) - (↑ξ.den : ℤ) * q.num|
⊢ 1 ≤ |HMul.hMul (α := ℚ) (↑ξ.num : ℚ) (↑q.den : ℚ) - HMul.hMul (α := ℚ) (↑ξ.den : ℚ) (↑q.num : ℚ)|

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℚ)
left : 1 ≤ |ξ.num * (↑q.den : ℤ) - q.num * (↑ξ.den : ℤ)|
⊢ 1 ≤ |ξ.num * (↑q.den : ℤ) - (↑ξ.den : ℤ) * q.num|

Tactic:
rw [mul_comm _ q.num]

Premises used: Rat.num, mul_comm
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℤ) - q.num * (↑ξ.den : ℤ)|

Tactic:
Int.one_le_abs (sub_ne_zero_of_ne <| mt Rat.eq_iff_mul_eq_mul.mpr H)

Premises used: Iff.mpr, Int.one_le_abs, mt, sub_ne_zero_of_ne, Rat.eq_iff_mul_eq_mul
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℤ) - q.num * (↑ξ.den : ℤ)|

Tactic:
exact Int.one_le_abs (sub_ne_zero_of_ne <| mt Rat.eq_iff_mul_eq_mul.mpr H)

Premises used: Iff.mpr, Int.one_le_abs, mt, sub_ne_zero_of_ne, Rat.eq_iff_mul_eq_mul
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ q : ℚ
hq₀ : LT.lt (α := ℚ) 0 (↑q.den : ℚ)
h : |ξ * (↑q.den : ℚ) - (↑q.num : ℚ)| < HDiv.hDiv (α := ℚ) 1 (↑q.den : ℚ)
⊢ ξ * (↑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)

Premises used: abs_sub_lt_iff, zero_lt_one, one_div_le, LT.lt.trans_le, Iff.mp
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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.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)

Premises used: abs_sub_lt_iff, zero_lt_one, one_div_le, LT.lt.trans_le, Iff.mp
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1

Tactic:
rw [sub_lt_iff_lt_add, add_comm] at h₁ h₂

Premises used: add_comm, sub_lt_iff_lt_add