awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₃ : ξ * (↑q.den : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1
⊢ (↑q.num : ℚ) < ξ * (↑q.den : ℚ) + 1

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

Premises used: add_comm, sub_lt_iff_lt_add
-- 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 : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1
h₂ : (↑q.num : ℚ) < ξ * (↑q.den : ℚ) + 1
⊢ HSub.hSub (α := ℚ) (↑q.num : ℚ) 1 < ξ * (↑q.den : ℚ)

Tactic:
rw [← sub_lt_iff_lt_add] at h₂

Premises used: sub_lt_iff_lt_add
-- 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 : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1
h₂ : HSub.hSub (α := ℚ) (↑q.num : ℚ) 1 < ξ * (↑q.den : ℚ)
⊢ ξ * (↑q.den : ℚ) < (↑(q.num + 1) : ℚ)

Tactic:
norm_cast at h₁ h₂
-- 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 : ℚ) < HAdd.hAdd (α := ℚ) (↑q.num : ℚ) 1
h₂ : HSub.hSub (α := ℚ) (↑q.num : ℚ) 1 < ξ * (↑q.den : ℚ)
h₃ : ξ * (↑q.den : ℚ) < (↑(q.num + 1) : ℚ)
⊢ (↑(q.num - 1) : ℚ) < ξ * (↑q.den : ℚ)

Tactic:
norm_cast at h₁ h₂
-- 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 - 1) : ℚ) < ξ * (↑q.den : ℚ)
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1

Tactic:
⟨sub_le_iff_le_add.mpr (Int.ceil_le.mpr h₁.le), sub_le_iff_le_add.mp (Int.le_floor.mpr h₂.le)⟩

Premises used: Iff.mpr, sub_le_iff_le_add, LT.lt.le, Int.ceil_le, And.intro, Int.le_floor, 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 - 1) : ℚ) < ξ * (↑q.den : ℚ)
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1

Tactic:
exact
      ⟨sub_le_iff_le_add.mpr (Int.ceil_le.mpr h₁.le), sub_le_iff_le_add.mp (Int.le_floor.mpr h₂.le)⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
set :
  let s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2};
  s.Finite
⊢ Set.Finite (α := ℚ) {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}

Tactic:
set s := {q : ℚ | |ξ - q| < 1 / (q.den : ℚ) ^ 2}
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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.num = b.num ∧ a.den = b.den

Tactic:
simp only [f, Prod.mk_inj] at hab

Premises used: Prod.mk_inj
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
rw : HDiv.hDiv (α := ℚ) (↑a.num : ℚ) (↑a.den : ℚ) = b
rw₁ : HDiv.hDiv (α := ℚ) (↑a.num : ℚ) (↑a.den : ℚ) = HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ)
rw₂ : HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑a.den : ℚ) = HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ)
rw₃ rw₄ : HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ) = HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ)
⊢ a = b

Tactic:
rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]

Premises used: Rat.num_div_den, And.right, And.left
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
⊢ Function.Injective f

Tactic:
have hinj : Function.Injective f := by
    intro a b hab
    simp only [f, Prod.mk_inj] at hab
    rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : xy ∈ f '' s
⊢ ∃ x ∈ s, f x = xy

Tactic:
simp only [mem_image] at hxy

Premises used: Set.mem_image
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : ∃ x ∈ s, f x = xy
obtain :
  ∀ (q : ℚ) (hq₁ : q ∈ s) (hq₂ : f q = xy),
    Membership.mem (γ := Set (ℤ × ℕ))
      (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}) xy
⊢ Membership.mem (γ := Set (ℤ × ℕ))
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}) xy

Tactic:
obtain ⟨q, hq₁, hq₂⟩ := hxy
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
⊢ q.den ≤ ξ.den

Tactic:
obtain ⟨hd, hn⟩ := den_le_and_le_num_le_of_sub_lt_one_div_den_sq hq₁

Premises used: Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
⊢ ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1

Tactic:
obtain ⟨hd, hn⟩ := den_le_and_le_num_le_of_sub_lt_one_div_den_sq hq₁

Premises used: Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
simp_rw :
  ∃ (i : ℕ) (_ : i ∈ Ioc 0 ξ.den), xy ∈ SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑i : ℚ)⌉ - 1) (⌊ξ * (↑i : ℚ)⌋ + 1)) {i}
⊢ Membership.mem (γ := Set (ℤ × ℕ))
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}) xy

Tactic:
simp_rw [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
⊢ ∃ (i : ℕ) (_ : i ∈ Ioc 0 ξ.den), xy ∈ SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑i : ℚ)⌉ - 1) (⌊ξ * (↑i : ℚ)⌋ + 1)) {i}

Tactic:
⟨q.den, Set.mem_Ioc.mpr ⟨q.pos, hd⟩, ?_⟩

Premises used: Iff.mpr, Rat.pos, Rat.den, And.intro, Exists.intro, Set.mem_Ioc
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
refine : xy ∈ SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑q.den : ℚ)⌉ - 1) (⌊ξ * (↑q.den : ℚ)⌋ + 1)) {q.den}
⊢ ∃ (i : ℕ) (_ : i ∈ Ioc 0 ξ.den), xy ∈ SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑i : ℚ)⌉ - 1) (⌊ξ * (↑i : ℚ)⌋ + 1)) {i}

Tactic:
refine ⟨q.den, Set.mem_Ioc.mpr ⟨q.pos, hd⟩, ?_⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
simp : ∃ (x : ℤ), (⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ x ∧ x ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1) ∧ (x, q.den) = xy
⊢ xy ∈ SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑q.den : ℚ)⌉ - 1) (⌊ξ * (↑q.den : ℚ)⌋ + 1)) {q.den}

Tactic:
simp only [prod_singleton, mem_image, mem_Icc]

Premises used: Set.mem_image, Set.prod_singleton, Set.mem_Icc
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
⊢ ∃ (x : ℤ), (⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ x ∧ x ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1) ∧ (x, q.den) = xy

Tactic:
⟨q.num, hn, hq₂⟩

Premises used: Rat.num, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
⊢ ∃ (x : ℤ), (⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ x ∧ x ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1) ∧ (x, q.den) = xy

Tactic:
exact ⟨q.num, hn, hq₂⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
⊢ f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}

Tactic:
have H : f '' s ⊆ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * y⌉ - 1) (⌊ξ * y⌋ + 1) ×ˢ {y} := by
    intro xy hxy
    simp only [mem_image] at hxy
    obtain ⟨q, hq₁, hq₂⟩ := hxy
    obtain ⟨hd, hn⟩ := den_le_and_le_num_le_of_sub_lt_one_div_den_sq hq₁
    simp_rw [mem_iUnion]
    refine ⟨q.den, Set.mem_Ioc.mpr ⟨q.pos, hd⟩, ?_⟩
    simp only [prod_singleton, mem_image, mem_Icc]
    exact ⟨q.num, hn, hq₂⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}
⊢ s.Finite

Tactic:
(Finite.subset ?_ H).of_finite_image hinj.injOn

Premises used: Function.Injective.injOn, Set.Finite.subset, Set.Finite.of_finite_image
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}
refine :
  Set.Finite (α := ℤ × ℕ)
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y})
⊢ s.Finite

Tactic:
refine (Finite.subset ?_ H).of_finite_image hinj.injOn

Premises used: Function.Injective.injOn, Set.Finite.subset, Set.Finite.of_finite_image
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}
⊢ Set.Finite (α := ℤ × ℕ)
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y})

Tactic:
Finite.biUnion (finite_Ioc _ _) fun x _ => Finite.prod (finite_Icc _ _) (finite_singleton _)

Premises used: HMul.hMul, Int.floor, HSub.hSub, Set.finite_Icc, Nat.cast, Set.Finite.prod, HAdd.hAdd, Set.Finite.biUnion, Set.finite_Ioc, Int.ceil, OfNat.ofNat, Set.finite_singleton
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}
⊢ Set.Finite (α := ℤ × ℕ)
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y})

Tactic:
exact Finite.biUnion (finite_Ioc _ _) fun x _ => Finite.prod (finite_Icc _ _) (finite_singleton _)

Premises used: Set.finite_Icc, Set.Finite.prod, Set.Finite.biUnion, Set.finite_Ioc, Set.finite_singleton
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
⊢ Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} ↔ Irrational ξ

Tactic:
⟨fun h => (irrational_iff_ne_rational ξ).mpr fun a b _ => ?_,
      Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational⟩

Premises used: Iff.mpr, Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational, irrational_iff_ne_rational, Iff.intro
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
h :
  ∀ (h : Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}) (a b : ℤ),
    b ≠ 0 → ξ ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} ↔ Irrational ξ

Tactic:
refine
    ⟨fun h => (irrational_iff_ne_rational ξ).mpr fun a b _ => ?_,
      Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
h : Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
a b : ℤ
h_1 : b ≠ 0
contrapose! :
  ∀ (h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
    Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
⊢ ξ ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
contrapose! h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ Set.Finite (α := ℚ)
    {q : ℚ | |HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}

Tactic:
Rat.finite_rat_abs_sub_lt_one_div_den_sq ((a : ℚ) / b)

Premises used: Int.cast, Rat.finite_rat_abs_sub_lt_one_div_den_sq, HDiv.hDiv
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
h₁ :
  ∀ (q : ℚ),
    |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 ↔
      |HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
⊢ Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}

Tactic:
convert! Rat.finite_rat_abs_sub_lt_one_div_den_sq ((a : ℚ) / b) with q

Premises used: Int.cast, Rat.finite_rat_abs_sub_lt_one_div_den_sq, HDiv.hDiv
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
q : ℚ
push_cast : 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 = 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 = (↑(1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
q : ℚ
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 = 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2

Tactic:
rfl
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
q : ℚ
h₁ :
  |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - (↑q : ℝ)| < (↑(1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2) : ℝ) ↔
    |HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
⊢ |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 ↔
    |HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2

Tactic:
rw [h, (by (push_cast; rfl) : (1 : ℝ) / (q.den : ℝ) ^ 2 = (1 / (q.den : ℚ) ^ 2 : ℚ))]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
q : ℚ
h₁ h₂ h₃ h₄ :
  |Rat.divInt a b - q| < HDiv.hDiv (α := ℚ) 1 (↑(HPow.hPow (β := ℕ) q.den 2) : ℚ) ↔
    |Rat.divInt a b - q| < HDiv.hDiv (α := ℚ) 1 (↑(HPow.hPow (β := ℕ) q.den 2) : ℚ)
⊢ |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - (↑q : ℝ)| < (↑(1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2) : ℝ) ↔
    |HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
⊢ ξ.convergent 0 = (↑⌊ξ⌋ : ℚ)

Tactic:
rfl

Premises used: Real.convergent, rfl
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
⊢ ξ.convergent (n + 1) = (↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹

Tactic:
rfl

Premises used: Real.convergent, rfl
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
⊢ convergent 0 0 = 0

Tactic:
simp only [convergent_zero, floor_zero, cast_zero]

Premises used: Int.cast_zero, Real.convergent_zero, Int.floor_zero
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
n : ℕ
ih : convergent 0 n = 0
⊢ convergent 0 (n + 1) = 0

Tactic:
simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]

Premises used: Int.cast_zero, inv_zero, Real.convergent_succ, Int.floor_zero, add_zero, Int.fract_zero
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
n : ℕ
zero : convergent 0 0 = 0
succ : ∀ (n : ℕ) (ih : convergent 0 n = 0), convergent 0 (n + 1) = 0
⊢ convergent 0 n = 0

Tactic:
induction n with
  | zero => simp only [convergent_zero, floor_zero, cast_zero]
  | succ n ih =>
    simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]

Premises used: Int.cast_zero, inv_zero, Real.convergent_succ, Real.convergent_zero, Int.floor_zero, Int.succ, add_zero, Int.fract_zero
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℤ
n : ℕ
zero : convergent (↑ξ : ℝ) 0 = (↑ξ : ℚ)
succ : ∀ (n : ℕ), convergent (↑ξ : ℝ) (n + 1) = (↑ξ : ℚ)
⊢ convergent (↑ξ : ℝ) n = (↑ξ : ℚ)

Tactic:
cases n
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℤ
⊢ convergent (↑ξ : ℝ) 0 = (↑ξ : ℚ)

Tactic:
simp only [convergent_zero, floor_intCast]

Premises used: Int.floor_intCast, Real.convergent_zero
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℤ
n : ℕ
⊢ convergent (↑ξ : ℝ) (n + 1) = (↑ξ : ℚ)

Tactic:
simp only [convergent_succ, floor_intCast, fract_intCast, convergent_of_zero, add_zero,
      inv_zero]

Premises used: Int.floor_intCast, inv_zero, Int.fract_intCast, Real.convergent_succ, Real.convergent_of_zero, add_zero
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℤ
hv : 0 < v
norm_cast : 0 < 2 * v - 1
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℤ
hv : 0 < v
⊢ 0 < 2 * v - 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ LT.lt (α := ℝ) 0 (↑v : ℝ)

Tactic:
have hv₀ : (0 : ℝ) < v := cast_pos.mpr (zero_lt_two.trans_le hv)
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑v : ℝ)

Tactic:
obtain ⟨hv₁, hv₂⟩ := aux₀ (zero_lt_two.trans_le hv)

Premises used: _private.0.Real.aux₀, LT.lt.trans_le, zero_lt_two
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1

Tactic:
obtain ⟨hv₁, hv₂⟩ := aux₀ (zero_lt_two.trans_le hv)

Premises used: _private.0.Real.aux₀, LT.lt.trans_le, zero_lt_two
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
⊢ IsCoprime u v

Tactic:
obtain ⟨hcop, _, h⟩ := h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
⊢ v = 1 → -(1 / 2) < ξ - (↑u : ℝ)

Tactic:
obtain ⟨hcop, _, h⟩ := h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹

Tactic:
obtain ⟨hcop, _, h⟩ := h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ 0 < fract ξ

Tactic:
fract_pos.mpr fun hf => ?_

Premises used: Iff.mpr, Int.fract_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
refine : ∀ (hf : ξ = (↑⌊ξ⌋ : ℝ)), False
⊢ 0 < fract ξ

Tactic:
refine fract_pos.mpr fun hf => ?_

Premises used: Iff.mpr, Int.fract_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
⊢ |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹

Tactic:
rw [hf] at h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
h₁ : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ ξ = (↑⌊ξ⌋ : ℝ)

Tactic:
rw [hf] at h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1 < 1

Tactic:
(mul_lt_iff_lt_one_right hv₀).1 ((inv_lt_inv₀ hv₀ (mul_pos hv₁ hv₂)).1 (h.trans_le' ?_))

Premises used: LT.lt.trans_le', mul_pos, Iff.mp, mul_lt_iff_lt_one_right, inv_lt_inv₀