-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem exists_int_int_abs_mul_sub_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
    ∃ j k : ℤ, 0 < k ∧ k ≤ n ∧ |↑k * ξ - j| ≤ 1 / (n + 1)

Proof state:
case neg.intro.intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ |fract (ξ * ↑y) * (↑n + 1) - fract (ξ * ↑x) * (↑n + 1)| ≤ 1

Tactic:
exact (abs_sub_lt_one_of_floor_eq_floor hxy.symm).le

Result:
no goals

Proof state:
case pos.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ |(ξ * ↑m - ↑(⌊ξ * ↑m⌋ + 1)) * (↑n + 1)| ≤ 1

Tactic:
rw [cast_add, ← sub_sub, sub_mul, cast_one, one_mul, abs_le]

Result:
case pos.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
m : ℤ
hm : m ∈ D
hf : f m = ↑n
hf' : ↑↑n ≤ fract (ξ * ↑m) * (↑n + 1)
hm₀ : 0 < m
⊢ -1 ≤ (ξ * ↑m - ↑⌊ξ * ↑m⌋) * (↑n + 1) - (↑n + 1) ∧ (ξ * ↑m - ↑⌊ξ * ↑m⌋) * (↑n + 1) - (↑n + 1) ≤ 1

Proof state:
case intro.intro.intro.intro.intro.inl
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
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

case intro.intro.intro.intro.intro.inr.inl
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
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

case intro.intro.intro.intro.intro.inr.inr
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
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:
exacts [⟨x, hx, y, hy, h, hxy⟩, False.elim (x_ne_y h), ⟨y, hy, x, hx, h, hxy.symm⟩]

Result:
no goals

Proof state:
case neg.intro.intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
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) * (↑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, ?_⟩

Result:
case neg.intro.intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ |(ξ * ↑(y - x) - ↑(⌊ξ * ↑y⌋ - ⌊ξ * ↑x⌋)) * (↑n + 1)| ≤ 1

Proof state:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
⊢ ∃ 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

Result:
case intro.intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
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

Proof state:
case h.e'_3.e_a
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ (ξ * ↑(y - x) - ↑(⌊ξ * ↑y⌋ - ⌊ξ * ↑x⌋)) * (↑n + 1) = fract (ξ * ↑y) * (↑n + 1) - fract (ξ * ↑x) * (↑n + 1)

Tactic:
push_cast

Result:
case h.e'_3.e_a
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ (ξ * (↑y - ↑x) - (↑⌊ξ * ↑y⌋ - ↑⌊ξ * ↑x⌋)) * (↑n + 1) = fract (ξ * ↑y) * (↑n + 1) - fract (ξ * ↑x) * (↑n + 1)

Proof state:
case h.e'_3.e_a
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ m ∈ D, f m ∈ Ico 0 ↑n
x : ℤ
hx : x ∈ D
y : ℤ
hy : y ∈ D
x_lt_y : x < y
hxy : f x = f y
⊢ (ξ * (↑y - ↑x) - (↑⌊ξ * ↑y⌋ - ↑⌊ξ * ↑x⌋)) * (↑n + 1) =
    (ξ * ↑y - ↑⌊ξ * ↑y⌋) * (↑n + 1) - (ξ * ↑x - ↑⌊ξ * ↑x⌋) * (↑n + 1)

Tactic:
ring

Result:
no goals

Proof state:
ξ : ℝ
n : ℕ
n_pos : 0 < n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)

Tactic:
let f : ℤ → ℤ := fun m => ⌊fract (ξ * m) * (n + 1)⌋

Result:
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)

Proof state:
case neg
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ¬∃ m ∈ D, f m = ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1

Tactic:
simp_rw [not_exists, not_and] at H

Result:
case neg
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1

Proof state:
case neg
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1

Tactic:
have hfu' : ∀ m, f m ≤ n := fun m => lt_add_one_iff.mp (floor_lt.mpr (mod_cast hfu m))

Result:
case neg
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
D : Finset ℤ := Icc 0 ↑n
H : ∀ x ∈ D, ¬f x = ↑n
hD : #(Ico 0 ↑n) < #D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1