-- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean
theorem finite_rat_abs_sub_lt_one_div_den_sq (ξ : ℚ) :
    {q : ℚ | |ξ - q| < 1 / (q.den : ℚ) ^ 2}.Finite

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
⊢ s.Finite

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

Result:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
⊢ (⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}).Finite

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : f a = f b
⊢ a = b

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

Result:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
⊢ a = b

Proof state:
ξ : ℚ
⊢ {q | |ξ - q| < 1 / ↑q.den ^ 2}.Finite

Tactic:
let f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)

Result:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
⊢ {q | |ξ - q| < 1 / ↑q.den ^ 2}.Finite

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
⊢ s.Finite

Tactic:
have H : f '' s ⊆ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * y⌉ - 1) (⌊ξ * y⌋ + 1) ×ˢ {y} := by
  intro xy hxy
  simp only [mem_image, mem_setOf] 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, (congr_arg Prod.snd (Eq.symm hq₂)).trans rfl]
  exact ⟨q.num, hn, hq₂⟩

Result:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
⊢ s.Finite

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
⊢ s.Finite

Tactic:
have hinj : Function.Injective f := by
  intro a b hab
  simp only [f, Prod.mk.inj_iff] at hab
  rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]

Result:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
⊢ s.Finite

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
⊢ {q | |ξ - q| < 1 / ↑q.den ^ 2}.Finite

Tactic:
set s := {q : ℚ | |ξ - q| < 1 / (q.den : ℚ) ^ 2}

Result:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
⊢ s.Finite

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
⊢ Function.Injective f

Tactic:
intro a b hab

Result:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : f a = f b
⊢ a = b

Proof state:
case intro.intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑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₂⟩

Result:
no goals

Proof state:
case intro.intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑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
⊢ xy ∈ Icc (⌈ξ * ↑q.den⌉ - 1) (⌊ξ * ↑q.den⌋ + 1) ×ˢ {q.den}

Tactic:
simp only [prod_singleton, mem_image, mem_Icc, (congr_arg Prod.snd (Eq.symm hq₂)).trans rfl]

Result:
case intro.intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑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

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
⊢ (⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}).Finite

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

Result:
no goals

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
⊢ a = b

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

Result:
no goals

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : xy ∈ f '' s
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Tactic:
simp only [mem_image, mem_setOf] at hxy

Result:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : ∃ x ∈ s, f x = xy
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Proof state:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : ∃ x ∈ s, f x = xy
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Tactic:
obtain ⟨q, hq₁, hq₂⟩ := hxy

Result:
case intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Proof state:
case intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

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

Result:
case intro.intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑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
⊢ xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Proof state:
case intro.intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑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 ∈ Icc (⌈ξ * ↑i⌉ - 1) (⌊ξ * ↑i⌋ + 1) ×ˢ {i}

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

Result:
case intro.intro.intro
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑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
⊢ xy ∈ Icc (⌈ξ * ↑q.den⌉ - 1) (⌊ξ * ↑q.den⌋ + 1) ×ˢ {q.den}