-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem exists_rat_abs_sub_le_and_den_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) :
    ∃ q : ℚ, |ξ - q| ≤ 1 / ((n + 1) * q.den) ∧ q.den ≤ n

Proof state:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑(↑j / ↑k)| * ↑(↑j / ↑k).den ≤ 1 / (↑n + 1)

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

Result:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑(↑j / ↑k)| * ↑k ≤ 1 / (↑n + 1)

Proof state:
case h.e'_3.h.e'_3.h.e'_1
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
⊢ ↑j / ↑k = Rat.divInt j k

Tactic:
exact Rat.intCast_div_eq_divInt _ _

Result:
no goals

Proof state:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

Tactic:
have hk₀' : (0 : ℝ) < k := Int.cast_pos.mpr hk₀

Result:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

Proof state:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

Tactic:
have hden : ((j / k : ℚ).den : ℤ) ≤ k := by
  convert le_of_dvd hk₀ (Rat.den_dvd j k)
  exact Rat.intCast_div_eq_divInt _ _

Result:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

Proof state:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

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

Result:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑(↑j / ↑k)| ≤ 1 / ((↑n + 1) * ↑(↑j / ↑k).den)

Proof state:
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
⊢ ↑(↑j / ↑k).den ≤ k

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

Result:
case h.e'_3.h.e'_3.h.e'_1
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
⊢ ↑j / ↑k = Rat.divInt j k

Proof state:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑(↑j / ↑k)| * ↑k ≤ 1 / (↑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]

Result:
no goals

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

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

Result:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

Proof state:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑(↑j / ↑k)| ≤ 1 / ((↑n + 1) * ↑(↑j / ↑k).den)

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

Result:
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
hk₀' : 0 < ↑k
hden : ↑(↑j / ↑k).den ≤ k
⊢ |ξ - ↑(↑j / ↑k)| * ↑(↑j / ↑k).den ≤ 1 / (↑n + 1)