awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
obtain :
  ∀ (x : ℤ) (hx : x ∈ D) (y : ℤ) (hy : y ∈ D) (x_ne_y : x ≠ y) (hxy : f x = f y), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

Tactic:
obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd

Premises used: Finset.exists_ne_map_eq_of_card_lt_of_maps_to
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
inl : ∀ (h : x < y), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
inr : ∀ (h : x = y), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
inr₁ : ∀ (h : y < x), ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

Tactic:
rcases lt_trichotomy x y with (h | h | h)

Premises used: lt_trichotomy
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
h : x < y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

Tactic:
⟨x, hx, y, hy, h, hxy⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
h : x = y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

Tactic:
False.elim (x_ne_y h)

Premises used: False.elim
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
h : y < x
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

Tactic:
⟨y, hy, x, hx, h, hxy.symm⟩

Premises used: And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_ne_y : x ≠ y
hxy : f x = f y
h : x < y
⊢ ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y

Tactic:
exacts [⟨x, hx, y, hy, h, hxy⟩, False.elim (x_ne_y h), ⟨y, hy, x, hx, h, hxy.symm⟩]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
neg :
  ∀ (x : ℤ) (hx : x ∈ D) (y : ℤ) (hy : y ∈ D) (x_lt_y : x < y) (hxy : f x = f y),
    ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
obtain ⟨x, hx, y, hy, x_lt_y, hxy⟩ : ∃ x ∈ D, ∃ y ∈ D, x < y ∧ f x = f y := by
      obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd
      rcases lt_trichotomy x y with (h | h | h)
      exacts [⟨x, hx, y, hy, h, hxy⟩, False.elim (x_ne_y h), ⟨y, hy, x, hx, h, hxy.symm⟩]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
⟨⌊ξ * y⌋ - ⌊ξ * x⌋, y - x, sub_pos_of_lt x_lt_y,
        sub_le_iff_le_add.mpr <| le_add_of_le_of_nonneg (mem_Icc.mp hy).2 (mem_Icc.mp hx).1, ?_⟩

Premises used: Iff.mpr, Int.cast, HMul.hMul, Int.floor, HSub.hSub, sub_le_iff_le_add, Finset.mem_Icc, And.right, And.left, And.intro, Exists.intro, Iff.mp, le_add_of_le_of_nonneg, sub_pos_of_lt
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
neg : |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
⊢ ∃ (j : ℤ) (k : ℤ), 0 < k ∧ k ≤ (↑n : ℤ) ∧ |(ξ * (↑k : ℝ) - (↑j : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
refine
      ⟨⌊ξ * y⌋ - ⌊ξ * x⌋, y - x, sub_pos_of_lt x_lt_y,
        sub_le_iff_le_add.mpr <| le_add_of_le_of_nonneg (mem_Icc.mp hy).2 (mem_Icc.mp hx).1, ?_⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
h :
  |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| =
    |fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1|
neg : |fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1
⊢ |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
convert_to |fract (ξ * y) * (n + 1) - fract (ξ * x) * (n + 1)| ≤ 1

Premises used: Int.cast, HMul.hMul, Int.fract, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
h :
  (ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |(ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| =
    |fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1|

Tactic:
congr
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
h :
  (ξ * HSub.hSub (α := ℝ) (↑y : ℝ) (↑x : ℝ) - HSub.hSub (α := ℝ) (↑⌊ξ * (↑y : ℝ)⌋ : ℝ) (↑⌊ξ * (↑x : ℝ)⌋ : ℝ)) *
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (ξ * (↑(y - x) : ℝ) - (↑(⌊ξ * (↑y : ℝ)⌋ - ⌊ξ * (↑x : ℝ)⌋) : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ (ξ * HSub.hSub (α := ℝ) (↑y : ℝ) (↑x : ℝ) - HSub.hSub (α := ℝ) (↑⌊ξ * (↑y : ℝ)⌋ : ℝ) (↑⌊ξ * (↑x : ℝ)⌋ : ℝ)) *
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 =
    (ξ * (↑y : ℝ) - (↑⌊ξ * (↑y : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 -
      (ξ * (↑x : ℝ) - (↑⌊ξ * (↑x : ℝ)⌋ : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ |fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
(abs_sub_lt_one_of_floor_eq_floor hxy.symm).le

Premises used: LT.lt.le, Int.abs_sub_lt_one_of_floor_eq_floor, Eq.symm
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun (m : ℤ) ↦ ⌊fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1⌋
hn : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hfu : ∀ (m : ℤ), fract (ξ * (↑m : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
D : Finset ℤ := Icc 0 (↑n : ℤ)
H : ∀ (m : ℤ) (_ : m ∈ D), f m ≠ (↑n : ℤ)
hD : card (α := ℤ) (Ico 0 (↑n : ℤ)) < #D
hfu' : ∀ (m : ℤ), f m ≤ (↑n : ℤ)
hwd : ∀ m ∈ D, Membership.mem (γ := Finset ℤ) (Ico 0 (↑n : ℤ)) (f m)
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ |fract (ξ * (↑y : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - fract (ξ * (↑x : ℝ)) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ≤ 1

Tactic:
exact (abs_sub_lt_one_of_floor_eq_floor hxy.symm).le

Premises used: LT.lt.le, Int.abs_sub_lt_one_of_floor_eq_floor, Eq.symm
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
obtain :
  ∀ (j k : ℤ) (hk₀ : 0 < k) (hk₁ : k ≤ (↑n : ℤ)) (h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1),
    ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos

Premises used: Real.exists_int_int_abs_mul_sub_le
-- 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
⊢ (↑k.toNat : ℤ) = k

Tactic:
have hk := toNat_of_nonneg hk₀.le
-- 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 : (↑k.toNat : ℤ) = k
⊢ LT.lt (α := ℤ) 0 (↑k.toNat : ℤ)

Tactic:
rw [← hk] at hk₀ hk₁ h
-- 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 : (↑k.toNat : ℤ) = k
hk₂ : LT.lt (α := ℤ) 0 (↑k.toNat : ℤ)
⊢ LE.le (α := ℤ) (↑k.toNat : ℤ) (↑n : ℤ)

Tactic:
rw [← hk] at hk₀ hk₁ h
-- 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 : (↑k.toNat : ℤ) = k
hk₂ : LT.lt (α := ℤ) 0 (↑k.toNat : ℤ)
hk₃ : LE.le (α := ℤ) (↑k.toNat : ℤ) (↑n : ℤ)
⊢ |(↑(↑k.toNat : ℤ) : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
rw [← hk] at hk₀ hk₁ h
-- 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 : (↑k.toNat : ℤ) = k
hk₂ : LT.lt (α := ℤ) 0 (↑k.toNat : ℤ)
hk₃ : LE.le (α := ℤ) (↑k.toNat : ℤ) (↑n : ℤ)
h₁ : |(↑(↑k.toNat : ℤ) : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ (↑k.toNat : ℤ) = k

Tactic:
rw [← hk] at hk₀ hk₁ h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : LT.lt (α := ℤ) 0 (↑k.toNat : ℤ)
hk₁ : LE.le (α := ℤ) (↑k.toNat : ℤ) (↑n : ℤ)
h : |(↑(↑k.toNat : ℤ) : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk : (↑k.toNat : ℤ) = k
⊢ ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
⟨k.toNat, natCast_pos.mp hk₀, Nat.cast_le.mp hk₁, (round_le (↑k.toNat * ξ) j).trans h⟩

Premises used: And.intro, Exists.intro, Iff.mp, Int.toNat, Nat.cast_le, Int.natCast_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : LT.lt (α := ℤ) 0 (↑k.toNat : ℤ)
hk₁ : LE.le (α := ℤ) (↑k.toNat : ℤ) (↑n : ℤ)
h : |(↑(↑k.toNat : ℤ) : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
hk : (↑k.toNat : ℤ) = k
⊢ ∃ (k : ℕ), 0 < k ∧ k ≤ n ∧ |(↑k : ℝ) * ξ - (↑(round ((↑k : ℝ) * ξ)) : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
exact ⟨k.toNat, natCast_pos.mp hk₀, Nat.cast_le.mp hk₁, (round_le (↑k.toNat * ξ) j).trans h⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
n : ℕ
n_pos : 0 < n
obtain :
  ∀ (j k : ℤ) (hk₀ : 0 < k) (hk₁ : k ≤ (↑n : ℤ)) (h : |(↑k : ℝ) * ξ - (↑j : ℝ)| ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1),
    ∃ (q : ℚ), |ξ - (↑q : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑q.den : ℝ)) ∧ q.den ≤ n
⊢ ∃ (q : ℚ), |ξ - (↑q : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑q.den : ℝ)) ∧ q.den ≤ n

Tactic:
obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos

Premises used: Real.exists_int_int_abs_mul_sub_le
-- 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
⊢ LT.lt (α := ℝ) 0 (↑k : ℝ)

Tactic:
have hk₀' : (0 : ℝ) < k := Int.cast_pos.mpr hk₀
-- 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 : ℝ)
⊢ (↑(Rat.divInt j k).den : ℤ) ≤ k

Tactic:
le_of_dvd hk₀ (Rat.den_dvd j k)

Premises used: Int.le_of_dvd, Rat.den_dvd
-- 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 : ℝ)
h₁ : HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ) = Rat.divInt j k
⊢ (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k

Tactic:
convert! le_of_dvd hk₀ (Rat.den_dvd j k)

Premises used: Int.le_of_dvd, Rat.den_dvd
-- 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 : ℝ)
⊢ HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ) = Rat.divInt j k

Tactic:
Rat.intCast_div_eq_divInt _ _

Premises used: Rat.intCast_div_eq_divInt
-- 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 : ℝ)
⊢ HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ) = Rat.divInt j k

Tactic:
exact Rat.intCast_div_eq_divInt _ _

Premises used: Rat.intCast_div_eq_divInt
-- 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 : ℝ)
⊢ (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℤ) ≤ k

Tactic:
have hden : ((j / k : ℚ).den : ℤ) ≤ k := by
    convert! le_of_dvd hk₀ (Rat.den_dvd j k)
    exact Rat.intCast_div_eq_divInt _ _
-- 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
⊢ ∃ (q : ℚ), |ξ - (↑q : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑q.den : ℝ)) ∧ q.den ≤ n

Tactic:
⟨j / k, ?_, Nat.cast_le.mp (hden.trans hk₁)⟩

Premises used: Int.cast, HDiv.hDiv, And.intro, Exists.intro, Iff.mp, Nat.cast_le, LE.le.trans
-- 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
refine :
  |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| ≤
    1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℝ))
⊢ ∃ (q : ℚ), |ξ - (↑q : ℝ)| ≤ 1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑q.den : ℝ)) ∧ q.den ≤ n

Tactic:
refine ⟨j / k, ?_, Nat.cast_le.mp (hden.trans hk₁)⟩
-- 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
rw :
  |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℝ) ≤
    1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| ≤
    1 / (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℝ))

Tactic:
rw [← div_div, le_div_iff₀ (Nat.cast_pos.mpr <| Rat.pos _ : (0 : ℝ) < _)]

Premises used: Iff.mpr, Nat.cast_pos, Rat.pos, div_div, le_div_iff₀
-- 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
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℝ) ≤
    1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
(mul_le_mul_of_nonneg_left (Int.cast_le.mpr hden : _ ≤ (k : ℝ)) (abs_nonneg _)).trans ?_

Premises used: Iff.mpr, Int.cast_le, LE.le.trans, mul_le_mul_of_nonneg_left, abs_nonneg
-- 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
refine : |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑k : ℝ) ≤ 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ |ξ - (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)) : ℝ)| * (↑(HDiv.hDiv (α := ℚ) (↑j : ℚ) (↑k : ℚ)).den : ℝ) ≤
    1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
refine (mul_le_mul_of_nonneg_left (Int.cast_le.mpr hden : _ ≤ (k : ℝ)) (abs_nonneg _)).trans ?_

Premises used: Iff.mpr, Int.cast_le, LE.le.trans, mul_le_mul_of_nonneg_left, abs_nonneg