[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
[PROOFSTEP]
let f : ℤ → ℤ := fun m => ⌊fract (ξ * m) * (n + 1)⌋
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
[PROOFSTEP]
have hn : 0 < (n : ℝ) + 1 := by exact_mod_cast Nat.succ_pos _
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
⊢ 0 < ↑n + 1
[PROOFSTEP]
exact_mod_cast Nat.succ_pos _
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
[PROOFSTEP]
have hfu := fun m : ℤ => mul_lt_of_lt_one_left hn <| fract_lt_one (ξ * ↑m)
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
[PROOFSTEP]
conv in |_| ≤ _ => rw [mul_comm, le_div_iff hn, ← abs_of_pos hn, ← abs_mul]
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
j k : ℤ
| |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
[PROOFSTEP]
rw [mul_comm, le_div_iff hn, ← abs_of_pos hn, ← abs_mul]
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
j k : ℤ
| |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
[PROOFSTEP]
rw [mul_comm, le_div_iff hn, ← abs_of_pos hn, ← abs_mul]
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
j k : ℤ
| |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
[PROOFSTEP]
rw [mul_comm, le_div_iff hn, ← abs_of_pos hn, ← abs_mul]
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
f : ℤ → ℤ := fun m => ⌊fract (ξ * ↑m) * (↑n + 1)⌋
hn : 0 < ↑n + 1
hfu : ∀ (m : ℤ), fract (ξ * ↑m) * (↑n + 1) < ↑n + 1
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
let D := Icc (0 : ℤ) n
[GOAL]
ξ : ℝ
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
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
by_cases H : ∃ m ∈ D, f m = n
[GOAL]
case pos
ξ : ℝ
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, m ∈ D ∧ f m = ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
obtain ⟨m, hm, hf⟩ := H
[GOAL]
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
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
have hf' : ((n : ℤ) : ℝ) ≤ fract (ξ * m) * (n + 1) := hf ▸ floor_le (fract (ξ * m) * (n + 1))
[GOAL]
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)
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
have hm₀ : 0 < m :=
  by
  have hf₀ : f 0 = 0 := by
    -- Porting note: was
            -- simp only [floor_eq_zero_iff, algebraMap.coe_zero, mul_zero, fract_zero,
            --   zero_mul, Set.left_mem_Ico, zero_lt_one]simp only [cast_zero, mul_zero, fract_zero, zero_mul,
      floor_zero]
  refine' Ne.lt_of_le (fun h => n_pos.ne _) (mem_Icc.mp hm).1
  exact_mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n)
[GOAL]
ξ : ℝ
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)
⊢ 0 < m
[PROOFSTEP]
have hf₀ : f 0 = 0 := by
  -- Porting note: was
          -- simp only [floor_eq_zero_iff, algebraMap.coe_zero, mul_zero, fract_zero,
          --   zero_mul, Set.left_mem_Ico, zero_lt_one]simp only [cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]
[GOAL]
ξ : ℝ
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)
⊢ f 0 = 0
[PROOFSTEP]
simp only [cast_zero, mul_zero, fract_zero, zero_mul, floor_zero]
[GOAL]
ξ : ℝ
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)
hf₀ : f 0 = 0
⊢ 0 < m
[PROOFSTEP]
refine' Ne.lt_of_le (fun h => n_pos.ne _) (mem_Icc.mp hm).1
[GOAL]
ξ : ℝ
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)
hf₀ : f 0 = 0
h : 0 = m
⊢ 0 = n
[PROOFSTEP]
exact_mod_cast hf₀.symm.trans (h.symm ▸ hf : f 0 = n)
[GOAL]
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
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
refine' ⟨⌊ξ * m⌋ + 1, m, hm₀, (mem_Icc.mp hm).2, _⟩
[GOAL]
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
[PROOFSTEP]
rw [cast_add, ← sub_sub, sub_mul, cast_one, one_mul, abs_le]
[GOAL]
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
[PROOFSTEP]
refine' ⟨le_sub_iff_add_le.mpr _, sub_le_iff_le_add.mpr <| le_of_lt <| (hfu m).trans <| lt_one_add _⟩
[GOAL]
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 + (↑n + 1) ≤ (ξ * ↑m - ↑⌊ξ * ↑m⌋) * (↑n + 1)
[PROOFSTEP]
simpa only [neg_add_cancel_comm_assoc] using hf'
[GOAL]
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, m ∈ D ∧ f m = ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
simp_rw [not_exists, not_and] at H
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
have hD : (Ico (0 : ℤ) n).card < D.card := by rw [card_Icc, card_Ico]; exact lt_add_one n
[GOAL]
ξ : ℝ
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
⊢ card (Ico 0 ↑n) < card D
[PROOFSTEP]
rw [card_Icc, card_Ico]
[GOAL]
ξ : ℝ
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
⊢ toNat (↑n - 0) < toNat (↑n + 1 - 0)
[PROOFSTEP]
exact lt_add_one n
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
have hfu' : ∀ m, f m ≤ n := fun m => lt_add_one_iff.mp (floor_lt.mpr (by exact_mod_cast hfu m))
[GOAL]
ξ : ℝ
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
m : ℤ
⊢ fract (ξ * ↑m) * (↑n + 1) < ↑(↑n + 1)
[PROOFSTEP]
exact_mod_cast hfu m
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
have hwd : ∀ m : ℤ, m ∈ D → f m ∈ Ico (0 : ℤ) n := fun x hx =>
  mem_Ico.mpr ⟨floor_nonneg.mpr (mul_nonneg (fract_nonneg (ξ * x)) hn.le), Ne.lt_of_le (H x hx) (hfu' x)⟩
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), m ∈ D → f m ∈ Ico 0 ↑n
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
have : ∃ (x : ℤ) (_ : x ∈ D) (y : ℤ) (_ : 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⟩]
[GOAL]
ξ : ℝ
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), m ∈ D → f m ∈ Ico 0 ↑n
⊢ ∃ x x_1 y x_2, x < y ∧ f x = f y
[PROOFSTEP]
obtain ⟨x, hx, y, hy, x_ne_y, hxy⟩ := exists_ne_map_eq_of_card_lt_of_maps_to hD hwd
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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 x_1 y x_2, x < y ∧ f x = f y
[PROOFSTEP]
rcases lt_trichotomy x y with (h | h | h)
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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 x_1 y x_2, 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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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 x_1 y x_2, 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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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 x_1 y x_2, x < y ∧ f x = f y
[PROOFSTEP]
exacts [⟨x, hx, y, hy, h, hxy⟩, False.elim (x_ne_y h), ⟨y, hy, x, hx, h, hxy.symm⟩]
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), m ∈ D → f m ∈ Ico 0 ↑n
this : ∃ x x_1 y x_2, x < y ∧ f x = f y
⊢ ∃ j k, 0 < k ∧ k ≤ ↑n ∧ |(ξ * ↑k - ↑j) * (↑n + 1)| ≤ 1
[PROOFSTEP]
obtain ⟨x, hx, y, hy, x_lt_y, hxy⟩ := this
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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
[PROOFSTEP]
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, _⟩
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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
[PROOFSTEP]
convert_to |fract (ξ * y) * (n + 1) - fract (ξ * x) * (n + 1)| ≤ 1
[GOAL]
case h.e'_3
ξ : ℝ
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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)|
[PROOFSTEP]
congr
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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)
[PROOFSTEP]
push_cast
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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)
[PROOFSTEP]
simp only [fract]
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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)
[PROOFSTEP]
ring
[GOAL]
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 : ℤ), x ∈ Icc 0 ↑n → ¬⌊fract (ξ * ↑x) * (↑n + 1)⌋ = ↑n
hD : card (Ico 0 ↑n) < card D
hfu' : ∀ (m : ℤ), f m ≤ ↑n
hwd : ∀ (m : ℤ), 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
[PROOFSTEP]
exact (abs_sub_lt_one_of_floor_eq_floor hxy.symm).le
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
[PROOFSTEP]
obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos
[GOAL]
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < k
hk₁ : k ≤ ↑n
h : |↑k * ξ - ↑j| ≤ 1 / (↑n + 1)
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
[PROOFSTEP]
have hk := toNat_of_nonneg hk₀.le
[GOAL]
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 : ↑(toNat k) = k
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
[PROOFSTEP]
rw [← hk] at hk₀ hk₁ h
[GOAL]
case intro.intro.intro.intro
ξ : ℝ
n : ℕ
n_pos : 0 < n
j k : ℤ
hk₀ : 0 < ↑(toNat k)
hk₁ : ↑(toNat k) ≤ ↑n
h : |↑↑(toNat k) * ξ - ↑j| ≤ 1 / (↑n + 1)
hk : ↑(toNat k) = k
⊢ ∃ k, 0 < k ∧ k ≤ n ∧ |↑k * ξ - ↑(round (↑k * ξ))| ≤ 1 / (↑n + 1)
[PROOFSTEP]
exact ⟨k.toNat, coe_nat_pos.mp hk₀, Nat.cast_le.mp hk₁, (round_le (↑k.toNat * ξ) j).trans h⟩
[GOAL]
ξ : ℝ
n : ℕ
n_pos : 0 < n
⊢ ∃ q, |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n
[PROOFSTEP]
obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos
[GOAL]
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
[PROOFSTEP]
have hk₀' : (0 : ℝ) < k := Int.cast_pos.mpr hk₀
[GOAL]
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
[PROOFSTEP]
have hden : ((j / k : ℚ).den : ℤ) ≤ k :=
  by
  convert le_of_dvd hk₀ (Rat.den_dvd j k)
  exact Rat.coe_int_div_eq_divInt
[GOAL]
ξ : ℝ
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
[PROOFSTEP]
convert le_of_dvd hk₀ (Rat.den_dvd j k)
[GOAL]
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
[PROOFSTEP]
exact Rat.coe_int_div_eq_divInt
[GOAL]
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
[PROOFSTEP]
refine' ⟨j / k, _, Nat.cast_le.mp (hden.trans hk₁)⟩
[GOAL]
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)
[PROOFSTEP]
rw [← div_div, le_div_iff (Nat.cast_pos.mpr <| Rat.pos _ : (0 : ℝ) < _)]
[GOAL]
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)
[PROOFSTEP]
refine' (mul_le_mul_of_nonneg_left (Int.cast_le.mpr hden : _ ≤ (k : ℝ)) (abs_nonneg _)).trans _
[GOAL]
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)
[PROOFSTEP]
rwa [← abs_of_pos hk₀', Rat.cast_div, Rat.cast_coe_int, Rat.cast_coe_int, ← abs_mul, sub_mul, div_mul_cancel _ hk₀'.ne',
  mul_comm]
[GOAL]
ξ : ℝ
hξ : Irrational ξ
q : ℚ
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
[PROOFSTEP]
have h := abs_pos.mpr (sub_ne_zero.mpr <| Irrational.ne_rat hξ q)
[GOAL]
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
[PROOFSTEP]
obtain ⟨m, hm⟩ := exists_nat_gt (1 / |ξ - q|)
[GOAL]
case intro
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
[PROOFSTEP]
have m_pos : (0 : ℝ) < m := (one_div_pos.mpr h).trans hm
[GOAL]
case intro
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
[PROOFSTEP]
obtain ⟨q', hbd, hden⟩ := exists_rat_abs_sub_le_and_den_le ξ (Nat.cast_pos.mp m_pos)
[GOAL]
case intro.intro.intro
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
[PROOFSTEP]
have den_pos : (0 : ℝ) < q'.den := Nat.cast_pos.mpr q'.pos
[GOAL]
case intro.intro.intro
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
den_pos : 0 < ↑q'.den
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
[PROOFSTEP]
have md_pos := mul_pos (add_pos m_pos zero_lt_one) den_pos
[GOAL]
case intro.intro.intro
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
den_pos : 0 < ↑q'.den
md_pos : 0 < (↑m + 1) * ↑q'.den
⊢ ∃ q', |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|
[PROOFSTEP]
refine'
  ⟨q', lt_of_le_of_lt hbd _,
    lt_of_le_of_lt hbd <|
      (one_div_lt md_pos h).mpr <|
        hm.trans <|
          lt_of_lt_of_le (lt_add_one _) <|
            (le_mul_iff_one_le_right <| add_pos m_pos zero_lt_one).mpr <| by exact_mod_cast (q'.pos : 1 ≤ q'.den)⟩
[GOAL]
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
den_pos : 0 < ↑q'.den
md_pos : 0 < (↑m + 1) * ↑q'.den
⊢ 1 ≤ ↑q'.den
[PROOFSTEP]
exact_mod_cast (q'.pos : 1 ≤ q'.den)
[GOAL]
case intro.intro.intro
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
den_pos : 0 < ↑q'.den
md_pos : 0 < (↑m + 1) * ↑q'.den
⊢ 1 / ((↑m + 1) * ↑q'.den) < 1 / ↑q'.den ^ 2
[PROOFSTEP]
rw [sq, one_div_lt_one_div md_pos (mul_pos den_pos den_pos), mul_lt_mul_right den_pos]
[GOAL]
case intro.intro.intro
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
den_pos : 0 < ↑q'.den
md_pos : 0 < (↑m + 1) * ↑q'.den
⊢ ↑q'.den < ↑m + 1
[PROOFSTEP]
exact lt_add_of_le_of_pos (Nat.cast_le.mpr hden) zero_lt_one
[GOAL]
ξ : ℝ
hξ : Irrational ξ
⊢ Set.Infinite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
[PROOFSTEP]
refine' Or.resolve_left (Set.finite_or_infinite _) fun h => _
[GOAL]
ξ : ℝ
hξ : Irrational ξ
h : Set.Finite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
⊢ False
[PROOFSTEP]
obtain ⟨q, _, hq⟩ :=
  exists_min_image {q : ℚ | |ξ - q| < 1 / (q.den : ℝ) ^ 2} (fun q => |ξ - q|) h
    ⟨⌊ξ⌋, by simp [abs_of_nonneg, Int.fract_lt_one]⟩
[GOAL]
ξ : ℝ
hξ : Irrational ξ
h : Set.Finite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
⊢ ↑⌊ξ⌋ ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
[PROOFSTEP]
simp [abs_of_nonneg, Int.fract_lt_one]
[GOAL]
case intro.intro
ξ : ℝ
hξ : Irrational ξ
h : Set.Finite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
q : ℚ
left✝ : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
hq : ∀ (b : ℚ), b ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2} → |ξ - ↑q| ≤ |ξ - ↑b|
⊢ False
[PROOFSTEP]
obtain ⟨q', hmem, hbetter⟩ := exists_rat_abs_sub_lt_and_lt_of_irrational hξ q
[GOAL]
case intro.intro.intro.intro
ξ : ℝ
hξ : Irrational ξ
h : Set.Finite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
q : ℚ
left✝ : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
hq : ∀ (b : ℚ), b ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2} → |ξ - ↑q| ≤ |ξ - ↑b|
q' : ℚ
hmem : |ξ - ↑q'| < 1 / ↑q'.den ^ 2
hbetter : |ξ - ↑q'| < |ξ - ↑q|
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (lt_of_le_of_lt (hq q' hmem) hbetter)
[GOAL]
ξ q : ℚ
h : |ξ - q| < 1 / ↑q.den ^ 2
⊢ q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
[PROOFSTEP]
have hq₀ : (0 : ℚ) < q.den := Nat.cast_pos.mpr q.pos
[GOAL]
ξ q : ℚ
h : |ξ - q| < 1 / ↑q.den ^ 2
hq₀ : 0 < ↑q.den
⊢ q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
[PROOFSTEP]
replace h : |ξ * q.den - q.num| < 1 / q.den
[GOAL]
case h
ξ q : ℚ
h : |ξ - q| < 1 / ↑q.den ^ 2
hq₀ : 0 < ↑q.den
⊢ |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
[PROOFSTEP]
rw [← mul_lt_mul_right hq₀] at h
[GOAL]
case h
ξ q : ℚ
h : |ξ - q| * ↑q.den < 1 / ↑q.den ^ 2 * ↑q.den
hq₀ : 0 < ↑q.den
⊢ |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
[PROOFSTEP]
conv_lhs at h => rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]
[GOAL]
ξ q : ℚ
h : |ξ - q| * ↑q.den < 1 / ↑q.den ^ 2 * ↑q.den
hq₀ : 0 < ↑q.den
| |ξ - q| * ↑q.den
[PROOFSTEP]
rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]
[GOAL]
ξ q : ℚ
h : |ξ - q| * ↑q.den < 1 / ↑q.den ^ 2 * ↑q.den
hq₀ : 0 < ↑q.den
| |ξ - q| * ↑q.den
[PROOFSTEP]
rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]
[GOAL]
ξ q : ℚ
h : |ξ - q| * ↑q.den < 1 / ↑q.den ^ 2 * ↑q.den
hq₀ : 0 < ↑q.den
| |ξ - q| * ↑q.den
[PROOFSTEP]
rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]
[GOAL]
case h
ξ q : ℚ
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den ^ 2 * ↑q.den
hq₀ : 0 < ↑q.den
⊢ |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
[PROOFSTEP]
rwa [sq, div_mul, mul_div_cancel_left _ hq₀.ne'] at h
[GOAL]
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
⊢ q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
[PROOFSTEP]
constructor
[GOAL]
case left
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
⊢ q.den ≤ ξ.den
[PROOFSTEP]
rcases eq_or_ne ξ q with (rfl | H)
[GOAL]
case left.inl
ξ : ℚ
hq₀ : 0 < ↑ξ.den
h : |ξ * ↑ξ.den - ↑ξ.num| < 1 / ↑ξ.den
⊢ ξ.den ≤ ξ.den
[PROOFSTEP]
exact le_rfl
[GOAL]
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
H : ξ ≠ q
⊢ q.den ≤ ξ.den
[PROOFSTEP]
have hξ₀ : (0 : ℚ) < ξ.den := Nat.cast_pos.mpr ξ.pos
[GOAL]
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den
[PROOFSTEP]
rw [← Rat.num_div_den ξ, div_mul_eq_mul_div, div_sub' _ _ _ hξ₀.ne', abs_div, abs_of_pos hξ₀, div_lt_iff hξ₀,
  div_mul_comm, mul_one] at h
[GOAL]
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den
[PROOFSTEP]
refine' Nat.cast_le.mp ((one_lt_div hq₀).mp <| lt_of_le_of_lt _ h).le
[GOAL]
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ 1 ≤ |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num|
[PROOFSTEP]
norm_cast
[GOAL]
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ 1 ≤ |ξ.num * ↑q.den - ↑ξ.den * q.num|
[PROOFSTEP]
rw [mul_comm _ q.num]
[GOAL]
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ 1 ≤ |ξ.num * ↑q.den - q.num * ↑ξ.den|
[PROOFSTEP]
exact Int.one_le_abs (sub_ne_zero_of_ne <| mt Rat.eq_iff_mul_eq_mul.mpr H)
[GOAL]
case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
[PROOFSTEP]
obtain ⟨h₁, h₂⟩ :=
  abs_sub_lt_iff.mp (h.trans_le <| (one_div_le zero_lt_one hq₀).mp <| (@one_div_one ℚ _).symm ▸ Nat.cast_le.mpr q.pos)
[GOAL]
case right.intro
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den - ↑q.num < 1
h₂ : ↑q.num - ξ * ↑q.den < 1
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
[PROOFSTEP]
rw [sub_lt_iff_lt_add, add_comm] at h₁ h₂
[GOAL]
case right.intro
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den < ↑q.num + 1
h₂ : ↑q.num < ξ * ↑q.den + 1
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
[PROOFSTEP]
rw [← sub_lt_iff_lt_add] at h₂
[GOAL]
case right.intro
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 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
[PROOFSTEP]
norm_cast at h₁ h₂
[GOAL]
case right.intro
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 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
[PROOFSTEP]
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)⟩
[GOAL]
ξ : ℚ
⊢ Set.Finite {q | |ξ - q| < 1 / ↑q.den ^ 2}
[PROOFSTEP]
let f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
[GOAL]
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
⊢ Set.Finite {q | |ξ - q| < 1 / ↑q.den ^ 2}
[PROOFSTEP]
set s := {q : ℚ | |ξ - q| < 1 / (q.den : ℚ) ^ 2}
[GOAL]
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
⊢ Set.Finite s
[PROOFSTEP]
have hinj : Function.Injective f := by
  intro a b hab
  simp only [Prod.mk.inj_iff] at hab
  rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
[GOAL]
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
⊢ Function.Injective f
[PROOFSTEP]
intro a b hab
[GOAL]
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : f a = f b
⊢ a = b
[PROOFSTEP]
simp only [Prod.mk.inj_iff] at hab
[GOAL]
ξ : ℚ
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
[PROOFSTEP]
rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
[GOAL]
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
⊢ Set.Finite s
[PROOFSTEP]
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₂⟩
[GOAL]
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
⊢ f '' s ⊆ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
[PROOFSTEP]
intro xy hxy
[GOAL]
ξ : ℚ
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 : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
[PROOFSTEP]
simp only [mem_image, mem_setOf] at hxy
[GOAL]
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : ∃ x, |ξ - x| < 1 / ↑x.den ^ 2 ∧ (x.num, x.den) = xy
⊢ xy ∈ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
[PROOFSTEP]
obtain ⟨q, hq₁, hq₂⟩ := hxy
[GOAL]
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| < 1 / ↑q.den ^ 2
hq₂ : (q.num, q.den) = xy
⊢ xy ∈ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
[PROOFSTEP]
obtain ⟨hd, hn⟩ := den_le_and_le_num_le_of_sub_lt_one_div_den_sq hq₁
[GOAL]
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| < 1 / ↑q.den ^ 2
hq₂ : (q.num, q.den) = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
⊢ xy ∈ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
[PROOFSTEP]
simp_rw [mem_iUnion]
[GOAL]
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| < 1 / ↑q.den ^ 2
hq₂ : (q.num, q.den) = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
⊢ ∃ i i_1, xy ∈ Icc (⌈ξ * ↑i⌉ - 1) (⌊ξ * ↑i⌋ + 1) ×ˢ {i}
[PROOFSTEP]
refine' ⟨q.den, Set.mem_Ioc.mpr ⟨q.pos, hd⟩, _⟩
[GOAL]
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| < 1 / ↑q.den ^ 2
hq₂ : (q.num, q.den) = 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}
[PROOFSTEP]
simp only [prod_singleton, mem_image, mem_Icc, (congr_arg Prod.snd (Eq.symm hq₂)).trans rfl]
[GOAL]
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| < 1 / ↑q.den ^ 2
hq₂ : (q.num, q.den) = 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
[PROOFSTEP]
exact ⟨q.num, hn, hq₂⟩
[GOAL]
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
⊢ Set.Finite s
[PROOFSTEP]
refine' Finite.of_finite_image (Finite.subset _ H) (injOn_of_injective hinj s)
[GOAL]
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
⊢ Set.Finite (⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y})
[PROOFSTEP]
exact Finite.biUnion (finite_Ioc _ _) fun x _ => Finite.prod (finite_Icc _ _) (finite_singleton _)
[GOAL]
ξ : ℝ
⊢ Set.Infinite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2} ↔ Irrational ξ
[PROOFSTEP]
refine'
  ⟨fun h => (irrational_iff_ne_rational ξ).mpr fun a b H => Set.not_infinite.mpr _ h,
    Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational⟩
[GOAL]
ξ : ℝ
h : Set.Infinite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
a b : ℤ
H : ξ = ↑a / ↑b
⊢ Set.Finite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
[PROOFSTEP]
convert Rat.finite_rat_abs_sub_lt_one_div_den_sq ((a : ℚ) / b) with q
[GOAL]
case h.e'_2.h.e'_2.h.a
ξ : ℝ
h : Set.Infinite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ |ξ - ↑q| < 1 / ↑q.den ^ 2 ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2
[PROOFSTEP]
rw [H, (by (push_cast ; rfl) : (1 : ℝ) / (q.den : ℝ) ^ 2 = (1 / (q.den : ℚ) ^ 2 : ℚ))]
[GOAL]
ξ : ℝ
h : Set.Infinite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ 1 / ↑q.den ^ 2 = ↑(1 / ↑q.den ^ 2)
[PROOFSTEP]
push_cast
[GOAL]
ξ : ℝ
h : Set.Infinite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ 1 / ↑q.den ^ 2 = 1 / ↑q.den ^ 2
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2.h.e'_2.h.a
ξ : ℝ
h : Set.Infinite {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
a b : ℤ
H : ξ = ↑a / ↑b
q : ℚ
⊢ |↑a / ↑b - ↑q| < ↑(1 / ↑q.den ^ 2) ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
⊢ convergent 0 n = 0
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ convergent 0 Nat.zero = 0
[PROOFSTEP]
simp only [Nat.zero_eq, convergent_zero, floor_zero, cast_zero]
[GOAL]
case succ
n : ℕ
ih : convergent 0 n = 0
⊢ convergent 0 (Nat.succ n) = 0
[PROOFSTEP]
simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]
[GOAL]
ξ : ℤ
n : ℕ
⊢ convergent (↑ξ) n = ↑ξ
[PROOFSTEP]
cases n
[GOAL]
case zero
ξ : ℤ
⊢ convergent (↑ξ) Nat.zero = ↑ξ
[PROOFSTEP]
simp only [Nat.zero_eq, convergent_zero, floor_intCast]
[GOAL]
case succ
ξ : ℤ
n✝ : ℕ
⊢ convergent (↑ξ) (Nat.succ n✝) = ↑ξ
[PROOFSTEP]
simp only [convergent_succ, floor_intCast, fract_intCast, convergent_of_zero, add_zero, inv_zero]
[GOAL]
ξ : ℝ
n : ℕ
⊢ convergents (GeneralizedContinuedFraction.of ξ) n = ↑(convergent ξ n)
[PROOFSTEP]
induction' n with n ih generalizing ξ
[GOAL]
case zero
ξ✝ ξ : ℝ
⊢ convergents (GeneralizedContinuedFraction.of ξ) Nat.zero = ↑(convergent ξ Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, zeroth_convergent_eq_h, of_h_eq_floor, convergent_zero, Rat.cast_coe_int]
[GOAL]
case succ
ξ✝ : ℝ
n : ℕ
ih : ∀ (ξ : ℝ), convergents (GeneralizedContinuedFraction.of ξ) n = ↑(convergent ξ n)
ξ : ℝ
⊢ convergents (GeneralizedContinuedFraction.of ξ) (Nat.succ n) = ↑(convergent ξ (Nat.succ n))
[PROOFSTEP]
rw [convergents_succ, ih (fract ξ)⁻¹, convergent_succ, one_div]
[GOAL]
case succ
ξ✝ : ℝ
n : ℕ
ih : ∀ (ξ : ℝ), convergents (GeneralizedContinuedFraction.of ξ) n = ↑(convergent ξ n)
ξ : ℝ
⊢ ↑⌊ξ⌋ + (↑(convergent (fract ξ)⁻¹ n))⁻¹ = ↑(↑⌊ξ⌋ + (convergent (fract ξ)⁻¹ n)⁻¹)
[PROOFSTEP]
norm_cast
[GOAL]
v : ℤ
hv : 0 < v
⊢ 0 < 2 * ↑v - 1
[PROOFSTEP]
norm_cast
[GOAL]
v : ℤ
hv : 0 < v
⊢ 0 < 2 * v - 1
[PROOFSTEP]
linarith
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ 0 < fract ξ
[PROOFSTEP]
have hv₀ : (0 : ℝ) < v := cast_pos.mpr (zero_lt_two.trans_le hv)
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ : 0 < ↑v
⊢ 0 < fract ξ
[PROOFSTEP]
obtain ⟨hv₁, hv₂⟩ := aux₀ (zero_lt_two.trans_le hv)
[GOAL]
case intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
⊢ 0 < fract ξ
[PROOFSTEP]
obtain ⟨hcop, _, h⟩ := h
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
⊢ 0 < fract ξ
[PROOFSTEP]
refine' fract_pos.mpr fun hf => _
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ False
[PROOFSTEP]
rw [hf] at h
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ False
[PROOFSTEP]
have H : (2 * v - 1 : ℝ) < 1 :=
  by
  refine' (mul_lt_iff_lt_one_right hv₀).mp ((inv_lt_inv hv₀ (mul_pos hv₁ hv₂)).mp (lt_of_le_of_lt _ h))
  have h' : (⌊ξ⌋ : ℝ) - u / v = (⌊ξ⌋ * v - u) / v := by field_simp [hv₀.ne']
  rw [h', abs_div, abs_of_pos hv₀, ← one_div, div_le_div_right hv₀]
  norm_cast
  rw [← zero_add (1 : ℤ), add_one_le_iff, abs_pos, sub_ne_zero]
  rintro rfl
  cases isUnit_iff.mp (isCoprime_self.mp (IsCoprime.mul_left_iff.mp hcop).2) <;> linarith
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ 2 * ↑v - 1 < 1
[PROOFSTEP]
refine' (mul_lt_iff_lt_one_right hv₀).mp ((inv_lt_inv hv₀ (mul_pos hv₁ hv₂)).mp (lt_of_le_of_lt _ h))
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ (↑v)⁻¹ ≤ |↑⌊ξ⌋ - ↑u / ↑v|
[PROOFSTEP]
have h' : (⌊ξ⌋ : ℝ) - u / v = (⌊ξ⌋ * v - u) / v := by field_simp [hv₀.ne']
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
[PROOFSTEP]
field_simp [hv₀.ne']
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ (↑v)⁻¹ ≤ |↑⌊ξ⌋ - ↑u / ↑v|
[PROOFSTEP]
rw [h', abs_div, abs_of_pos hv₀, ← one_div, div_le_div_right hv₀]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ 1 ≤ |↑⌊ξ⌋ * ↑v - ↑u|
[PROOFSTEP]
norm_cast
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ 1 ≤ |⌊ξ⌋ * v - u|
[PROOFSTEP]
rw [← zero_add (1 : ℤ), add_one_le_iff, abs_pos, sub_ne_zero]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ ⌊ξ⌋ * v ≠ u
[PROOFSTEP]
rintro rfl
[GOAL]
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hf : ξ = ↑⌊ξ⌋
hcop : IsCoprime (⌊ξ⌋ * v) v
left✝ : v = 1 → -(1 / 2) < ξ - ↑(⌊ξ⌋ * v)
h : |↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : ↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v = (↑⌊ξ⌋ * ↑v - ↑(⌊ξ⌋ * v)) / ↑v
⊢ False
[PROOFSTEP]
cases isUnit_iff.mp (isCoprime_self.mp (IsCoprime.mul_left_iff.mp hcop).2)
[GOAL]
case inl
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hf : ξ = ↑⌊ξ⌋
hcop : IsCoprime (⌊ξ⌋ * v) v
left✝ : v = 1 → -(1 / 2) < ξ - ↑(⌊ξ⌋ * v)
h : |↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : ↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v = (↑⌊ξ⌋ * ↑v - ↑(⌊ξ⌋ * v)) / ↑v
h✝ : v = 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case inr
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hf : ξ = ↑⌊ξ⌋
hcop : IsCoprime (⌊ξ⌋ * v) v
left✝ : v = 1 → -(1 / 2) < ξ - ↑(⌊ξ⌋ * v)
h : |↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : ↑⌊ξ⌋ - ↑(⌊ξ⌋ * v) / ↑v = (↑⌊ξ⌋ * ↑v - ↑(⌊ξ⌋ * v)) / ↑v
h✝ : v = -1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
H : 2 * ↑v - 1 < 1
⊢ False
[PROOFSTEP]
norm_cast at H
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
H : 2 * v - 1 < 1
⊢ False
[PROOFSTEP]
linarith only [hv, H]
  -- An auxiliary lemma for the inductive step.
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
[PROOFSTEP]
obtain ⟨hcop, _, h⟩ := h
[GOAL]
case intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
[PROOFSTEP]
obtain ⟨hv₀, hv₀'⟩ := aux₀ (zero_lt_two.trans_le hv)
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
[PROOFSTEP]
have hv₁ : 0 < 2 * v - 1 := by linarith only [hv]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
⊢ 0 < 2 * v - 1
[PROOFSTEP]
linarith only [hv]
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
[PROOFSTEP]
rw [← one_div, lt_div_iff (mul_pos hv₀ hv₀'), ← abs_of_pos (mul_pos hv₀ hv₀'), ← abs_mul, sub_mul, ← mul_assoc, ←
  mul_assoc, div_mul_cancel _ hv₀.ne', abs_sub_comm, abs_lt, lt_sub_iff_add_lt, sub_lt_iff_lt_add, mul_assoc] at h
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
[PROOFSTEP]
have hu₀ : 0 ≤ u - ⌊ξ⌋ * v := by
  -- Porting note: this abused the definitional equality `-1 + 1 = 0`
      -- refine' (zero_le_mul_right hv₁).mp ((lt_iff_add_one_le (-1 : ℤ) _).mp _)
  refine' (zero_le_mul_right hv₁).mp ?_
  rw [← sub_one_lt_iff, zero_sub]
  replace h := h.1
  rw [← lt_sub_iff_add_lt, ← mul_assoc, ← sub_mul] at h
  exact_mod_cast
    h.trans_le
      ((mul_le_mul_right <| hv₀').mpr <| (sub_le_sub_iff_left (u : ℝ)).mpr ((mul_le_mul_right hv₀).mpr (floor_le ξ)))
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 ≤ u - ⌊ξ⌋ * v
[PROOFSTEP]
refine' (zero_le_mul_right hv₁).mp ?_
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 ≤ (u - ⌊ξ⌋ * v) * (2 * v - 1)
[PROOFSTEP]
rw [← sub_one_lt_iff, zero_sub]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)
[PROOFSTEP]
replace h := h.1
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1)
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)
[PROOFSTEP]
rw [← lt_sub_iff_add_lt, ← mul_assoc, ← sub_mul] at h
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
h : -1 < (↑u - ξ * ↑v) * (2 * ↑v - 1)
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)
[PROOFSTEP]
exact_mod_cast
  h.trans_le
    ((mul_le_mul_right <| hv₀').mpr <| (sub_le_sub_iff_left (u : ℝ)).mpr ((mul_le_mul_right hv₀).mpr (floor_le ξ)))
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
[PROOFSTEP]
have hu₁ : u - ⌊ξ⌋ * v ≤ v := by
  refine' le_of_mul_le_mul_right (le_of_lt_add_one _) hv₁
  replace h := h.2
  rw [← sub_lt_iff_lt_add, ← mul_assoc, ← sub_mul, ← add_lt_add_iff_right (v * (2 * v - 1) : ℝ), add_comm (1 : ℝ)] at h
  have :=
    (mul_lt_mul_right <| hv₀').mpr
      ((sub_lt_sub_iff_left (u : ℝ)).mpr <| (mul_lt_mul_right hv₀).mpr <| sub_right_lt_of_lt_add <| lt_floor_add_one ξ)
  rw [sub_mul ξ, one_mul, ← sub_add, add_mul] at this
  exact_mod_cast this.trans h
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
⊢ u - ⌊ξ⌋ * v ≤ v
[PROOFSTEP]
refine' le_of_mul_le_mul_right (le_of_lt_add_one _) hv₁
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
[PROOFSTEP]
replace h := h.2
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
[PROOFSTEP]
rw [← sub_lt_iff_lt_add, ← mul_assoc, ← sub_mul, ← add_lt_add_iff_right (v * (2 * v - 1) : ℝ), add_comm (1 : ℝ)] at h
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
[PROOFSTEP]
have :=
  (mul_lt_mul_right <| hv₀').mpr
    ((sub_lt_sub_iff_left (u : ℝ)).mpr <| (mul_lt_mul_right hv₀).mpr <| sub_right_lt_of_lt_add <| lt_floor_add_one ξ)
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
this : (↑u - ↑⌊ξ⌋ * ↑v) * (2 * ↑v - 1) < (↑u - (ξ - 1) * ↑v) * (2 * ↑v - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
[PROOFSTEP]
rw [sub_mul ξ, one_mul, ← sub_add, add_mul] at this
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
this : (↑u - ↑⌊ξ⌋ * ↑v) * (2 * ↑v - 1) < (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
[PROOFSTEP]
exact_mod_cast this.trans h
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
[PROOFSTEP]
have huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v := by rwa [sub_eq_add_neg, ← neg_mul, IsCoprime.add_mul_right_left_iff]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
⊢ IsCoprime (u - ⌊ξ⌋ * v) v
[PROOFSTEP]
rwa [sub_eq_add_neg, ← neg_mul, IsCoprime.add_mul_right_left_iff]
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
[PROOFSTEP]
refine' ⟨lt_of_le_of_ne' hu₀ fun hf => _, lt_of_le_of_ne hu₁ fun hf => _⟩
[GOAL]
case intro.intro.intro.refine'_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
hf : u - ⌊ξ⌋ * v = 0
⊢ False
[PROOFSTEP]
rw [hf] at huv_cop
[GOAL]
case intro.intro.intro.refine'_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime 0 v
hf : u - ⌊ξ⌋ * v = 0
⊢ False
[PROOFSTEP]
simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop
[GOAL]
case intro.intro.intro.refine'_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = 0
huv_cop : v = 1 ∨ v = -1
⊢ False
[PROOFSTEP]
cases' huv_cop with huv_cop huv_cop
[GOAL]
case intro.intro.intro.refine'_1.inl
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = 0
huv_cop : v = 1
⊢ False
[PROOFSTEP]
linarith only [hv, huv_cop]
  -- The key step: the relevant inequality persists in the inductive step.
[GOAL]
case intro.intro.intro.refine'_1.inr
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = 0
huv_cop : v = -1
⊢ False
[PROOFSTEP]
linarith only [hv, huv_cop]
  -- The key step: the relevant inequality persists in the inductive step.
[GOAL]
case intro.intro.intro.refine'_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
hf : u - ⌊ξ⌋ * v = v
⊢ False
[PROOFSTEP]
rw [hf] at huv_cop
[GOAL]
case intro.intro.intro.refine'_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime v v
hf : u - ⌊ξ⌋ * v = v
⊢ False
[PROOFSTEP]
simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop
[GOAL]
case intro.intro.intro.refine'_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = v
huv_cop : v = 1 ∨ v = -1
⊢ False
[PROOFSTEP]
cases' huv_cop with huv_cop huv_cop
[GOAL]
case intro.intro.intro.refine'_2.inl
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = v
huv_cop : v = 1
⊢ False
[PROOFSTEP]
linarith only [hv, huv_cop]
  -- The key step: the relevant inequality persists in the inductive step.
[GOAL]
case intro.intro.intro.refine'_2.inr
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = v
huv_cop : v = -1
⊢ False
[PROOFSTEP]
linarith only [hv, huv_cop]
  -- The key step: the relevant inequality persists in the inductive step.
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ |(fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹
[PROOFSTEP]
obtain ⟨hu₀, huv⟩ := aux₂ hv h
[GOAL]
case intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hu₀ : 0 < u - ⌊ξ⌋ * v
huv : u - ⌊ξ⌋ * v < v
⊢ |(fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹
[PROOFSTEP]
have hξ₀ := aux₁ hv h
[GOAL]
case intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hu₀ : 0 < u - ⌊ξ⌋ * v
huv : u - ⌊ξ⌋ * v < v
hξ₀ : 0 < fract ξ
⊢ |(fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹
[PROOFSTEP]
set u' := u - ⌊ξ⌋ * v with hu'
[GOAL]
case intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
⊢ |(fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹
[PROOFSTEP]
have hu'ℝ : (u' : ℝ) = u - ⌊ξ⌋ * v := by exact_mod_cast hu'
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
⊢ ↑u' = ↑u - ↑⌊ξ⌋ * ↑v
[PROOFSTEP]
exact_mod_cast hu'
[GOAL]
case intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u' = ↑u - ↑⌊ξ⌋ * ↑v
⊢ |(fract ξ)⁻¹ - ↑v / (↑u - ↑⌊ξ⌋ * ↑v)| < ((↑u - ↑⌊ξ⌋ * ↑v) * (2 * (↑u - ↑⌊ξ⌋ * ↑v) - 1))⁻¹
[PROOFSTEP]
rw [← hu'ℝ]
[GOAL]
case intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u' = ↑u - ↑⌊ξ⌋ * ↑v
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
replace hu'ℝ := (eq_sub_iff_add_eq.mp hu'ℝ).symm
[GOAL]
case intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
obtain ⟨Hu, Hu'⟩ := aux₀ hu₀
[GOAL]
case intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
obtain ⟨Hv, Hv'⟩ := aux₀ (zero_lt_two.trans_le hv)
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
have H₁ := div_pos (div_pos Hv Hu) hξ₀
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
replace h := h.2.2
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
have h' : |fract ξ - u' / v| < ((v : ℝ) * (2 * v - 1))⁻¹ := by
  rwa [hu'ℝ, add_div, mul_div_cancel _ Hv.ne', ← sub_sub, sub_right_comm] at h
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
⊢ |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
[PROOFSTEP]
rwa [hu'ℝ, add_div, mul_div_cancel _ Hv.ne', ← sub_sub, sub_right_comm] at h
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
have H : (2 * u' - 1 : ℝ) ≤ (2 * v - 1) * fract ξ :=
  by
  replace h := (abs_lt.mp h).1
  have : (2 * (v : ℝ) - 1) * (-((v : ℝ) * (2 * v - 1))⁻¹ + u' / v) = 2 * u' - (1 + u') / v := by
    field_simp [Hv.ne', Hv'.ne']; ring
  rw [hu'ℝ, add_div, mul_div_cancel _ Hv.ne', ← sub_sub, sub_right_comm, self_sub_floor, lt_sub_iff_add_lt, ←
    mul_lt_mul_left Hv', this] at h
  refine' LE.le.trans _ h.le
  rw [sub_le_sub_iff_left, div_le_one Hv, add_comm]
  exact_mod_cast huv
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
[PROOFSTEP]
replace h := (abs_lt.mp h).1
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑u / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
[PROOFSTEP]
have : (2 * (v : ℝ) - 1) * (-((v : ℝ) * (2 * v - 1))⁻¹ + u' / v) = 2 * u' - (1 + u') / v := by
  field_simp [Hv.ne', Hv'.ne']; ring
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑u / ↑v
⊢ (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
[PROOFSTEP]
field_simp [Hv.ne', Hv'.ne']
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑u / ↑v
⊢ (2 * ↑v - 1) * (-↑v + (↑u - ↑⌊ξ⌋ * ↑v) * (↑v * (2 * ↑v - 1))) * ↑v =
    (2 * (↑u - ↑⌊ξ⌋ * ↑v) * ↑v - (1 + (↑u - ↑⌊ξ⌋ * ↑v))) * (↑v * (2 * ↑v - 1) * ↑v)
[PROOFSTEP]
ring
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : -(↑v * (2 * ↑v - 1))⁻¹ < ξ - ↑u / ↑v
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
[PROOFSTEP]
rw [hu'ℝ, add_div, mul_div_cancel _ Hv.ne', ← sub_sub, sub_right_comm, self_sub_floor, lt_sub_iff_add_lt, ←
  mul_lt_mul_left Hv', this] at h
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : 2 * ↑u' - (1 + ↑u') / ↑v < (2 * ↑v - 1) * fract ξ
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
[PROOFSTEP]
refine' LE.le.trans _ h.le
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : 2 * ↑u' - (1 + ↑u') / ↑v < (2 * ↑v - 1) * fract ξ
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ 2 * ↑u' - 1 ≤ 2 * ↑u' - (1 + ↑u') / ↑v
[PROOFSTEP]
rw [sub_le_sub_iff_left, div_le_one Hv, add_comm]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h : 2 * ↑u' - (1 + ↑u') / ↑v < (2 * ↑v - 1) * fract ξ
this : (2 * ↑v - 1) * (-(↑v * (2 * ↑v - 1))⁻¹ + ↑u' / ↑v) = 2 * ↑u' - (1 + ↑u') / ↑v
⊢ ↑u' + 1 ≤ ↑v
[PROOFSTEP]
exact_mod_cast huv
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
have help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)| := by intros;
  rw [abs_sub_comm]; congr 1; field_simp; ring
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
⊢ ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|
[PROOFSTEP]
intros
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
a✝³ b✝ c✝ : ℝ
a✝² : a✝³ ≠ 0
a✝¹ : b✝ ≠ 0
a✝ : c✝ ≠ 0
⊢ |a✝³⁻¹ - b✝ / c✝| = |(a✝³ - c✝ / b✝) * (b✝ / c✝ / a✝³)|
[PROOFSTEP]
rw [abs_sub_comm]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
a✝³ b✝ c✝ : ℝ
a✝² : a✝³ ≠ 0
a✝¹ : b✝ ≠ 0
a✝ : c✝ ≠ 0
⊢ |b✝ / c✝ - a✝³⁻¹| = |(a✝³ - c✝ / b✝) * (b✝ / c✝ / a✝³)|
[PROOFSTEP]
congr 1
[GOAL]
case e_a
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
a✝³ b✝ c✝ : ℝ
a✝² : a✝³ ≠ 0
a✝¹ : b✝ ≠ 0
a✝ : c✝ ≠ 0
⊢ b✝ / c✝ - a✝³⁻¹ = (a✝³ - c✝ / b✝) * (b✝ / c✝ / a✝³)
[PROOFSTEP]
field_simp
[GOAL]
case e_a
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
a✝³ b✝ c✝ : ℝ
a✝² : a✝³ ≠ 0
a✝¹ : b✝ ≠ 0
a✝ : c✝ ≠ 0
⊢ b✝ * a✝³ = a✝³ * b✝
[PROOFSTEP]
ring
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
have help₂ : ∀ {a b c d : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (b * c)⁻¹ * (b / d / a) = (d * c * a)⁻¹ := by intros;
  field_simp; ring
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|
⊢ ∀ {a b c d : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (b * c)⁻¹ * (b / d / a) = (d * c * a)⁻¹
[PROOFSTEP]
intros
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|
a✝⁴ b✝ c✝ d✝ : ℝ
a✝³ : a✝⁴ ≠ 0
a✝² : b✝ ≠ 0
a✝¹ : c✝ ≠ 0
a✝ : d✝ ≠ 0
⊢ (b✝ * c✝)⁻¹ * (b✝ / d✝ / a✝⁴) = (d✝ * c✝ * a✝⁴)⁻¹
[PROOFSTEP]
field_simp
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|
a✝⁴ b✝ c✝ d✝ : ℝ
a✝³ : a✝⁴ ≠ 0
a✝² : b✝ ≠ 0
a✝¹ : c✝ ≠ 0
a✝ : d✝ ≠ 0
⊢ b✝ * (d✝ * c✝ * a✝⁴) = b✝ * c✝ * (d✝ * a✝⁴)
[PROOFSTEP]
ring
[GOAL]
case intro.intro.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|
help₂ : ∀ {a b c d : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (b * c)⁻¹ * (b / d / a) = (d * c * a)⁻¹
⊢ |(fract ξ)⁻¹ - ↑v / ↑u'| < (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
calc
  |(fract ξ)⁻¹ - v / u'| = |(fract ξ - u' / v) * (v / u' / fract ξ)| := help₁ hξ₀.ne' Hv.ne' Hu.ne'
  _ = |fract ξ - u' / v| * (v / u' / fract ξ) := by rw [abs_mul, abs_of_pos H₁, abs_sub_comm]
  _ < ((v : ℝ) * (2 * v - 1))⁻¹ * (v / u' / fract ξ) := ((mul_lt_mul_right H₁).mpr h')
  _ = (u' * (2 * v - 1) * fract ξ)⁻¹ := (help₂ hξ₀.ne' Hv.ne' Hv'.ne' Hu.ne')
  _ ≤ ((u' : ℝ) * (2 * u' - 1))⁻¹ := by
    rwa [inv_le_inv (mul_pos (mul_pos Hu Hv') hξ₀) <| mul_pos Hu Hu', mul_assoc, mul_le_mul_left Hu]
      -- The conditions `ass ξ u v` persist in the inductive step.
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|
help₂ : ∀ {a b c d : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (b * c)⁻¹ * (b / d / a) = (d * c * a)⁻¹
⊢ |(fract ξ - ↑u' / ↑v) * (↑v / ↑u' / fract ξ)| = |fract ξ - ↑u' / ↑v| * (↑v / ↑u' / fract ξ)
[PROOFSTEP]
rw [abs_mul, abs_of_pos H₁, abs_sub_comm]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hξ₀ : 0 < fract ξ
u' : ℤ := u - ⌊ξ⌋ * v
hu₀ : 0 < u'
huv : u' < v
hu' : u' = u - ⌊ξ⌋ * v
hu'ℝ : ↑u = ↑u' + ↑⌊ξ⌋ * ↑v
Hu : 0 < ↑u'
Hu' : 0 < 2 * ↑u' - 1
Hv : 0 < ↑v
Hv' : 0 < 2 * ↑v - 1
H₁ : 0 < ↑v / ↑u' / fract ξ
h : |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
h' : |fract ξ - ↑u' / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
H : 2 * ↑u' - 1 ≤ (2 * ↑v - 1) * fract ξ
help₁ : ∀ {a b c : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → |a⁻¹ - b / c| = |(a - c / b) * (b / c / a)|
help₂ : ∀ {a b c d : ℝ}, a ≠ 0 → b ≠ 0 → c ≠ 0 → d ≠ 0 → (b * c)⁻¹ * (b / d / a) = (d * c * a)⁻¹
⊢ (↑u' * (2 * ↑v - 1) * fract ξ)⁻¹ ≤ (↑u' * (2 * ↑u' - 1))⁻¹
[PROOFSTEP]
rwa [inv_le_inv (mul_pos (mul_pos Hu Hv') hξ₀) <| mul_pos Hu Hu', mul_assoc, mul_le_mul_left Hu]
  -- The conditions `ass ξ u v` persist in the inductive step.
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * v)
[PROOFSTEP]
refine' ⟨_, fun huv => _, by exact_mod_cast aux₃ hv h⟩
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ |(fract ξ)⁻¹ - ↑v / ↑(u - ⌊ξ⌋ * v)| < (↑(u - ⌊ξ⌋ * v) * (2 * ↑(u - ⌊ξ⌋ * v) - 1))⁻¹
[PROOFSTEP]
exact_mod_cast aux₃ hv h
[GOAL]
case refine'_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ IsCoprime v (u - ⌊ξ⌋ * v)
[PROOFSTEP]
rw [sub_eq_add_neg, ← neg_mul, isCoprime_comm, IsCoprime.add_mul_right_left_iff]
[GOAL]
case refine'_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ IsCoprime u v
[PROOFSTEP]
exact h.1
[GOAL]
case refine'_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
[PROOFSTEP]
obtain ⟨hv₀, hv₀'⟩ := aux₀ (zero_lt_two.trans_le hv)
[GOAL]
case refine'_2.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
[PROOFSTEP]
have Hv : (v * (2 * v - 1) : ℝ)⁻¹ + (v : ℝ)⁻¹ = 2 / (2 * v - 1) :=
  by
  field_simp [hv₀.ne', hv₀'.ne']
  ring
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
⊢ (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
[PROOFSTEP]
field_simp [hv₀.ne', hv₀'.ne']
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
⊢ (↑v + ↑v * (2 * ↑v - 1)) * (2 * ↑v - 1) = 2 * (↑v * (2 * ↑v - 1) * ↑v)
[PROOFSTEP]
ring
[GOAL]
case refine'_2.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
[PROOFSTEP]
have Huv : (u / v : ℝ) = ⌊ξ⌋ + (v : ℝ)⁻¹ := by rw [sub_eq_iff_eq_add'.mp huv]; field_simp [hv₀.ne']
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
⊢ ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
[PROOFSTEP]
rw [sub_eq_iff_eq_add'.mp huv]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
⊢ ↑(⌊ξ⌋ * v + 1) / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
[PROOFSTEP]
field_simp [hv₀.ne']
[GOAL]
case refine'_2.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
[PROOFSTEP]
have h' := (abs_sub_lt_iff.mp h.2.2).1
[GOAL]
case refine'_2.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : ξ - ↑u / ↑v < (↑v * (2 * ↑v - 1))⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
[PROOFSTEP]
rw [Huv, ← sub_sub, sub_lt_iff_lt_add, self_sub_floor, Hv] at h'
[GOAL]
case refine'_2.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : fract ξ < 2 / (2 * ↑v - 1)
⊢ -(1 / 2) < (fract ξ)⁻¹ - ↑v
[PROOFSTEP]
rwa [lt_sub_iff_add_lt', (by ring : (v : ℝ) + -(1 / 2) = (2 * v - 1) / 2),
  lt_inv (div_pos hv₀' zero_lt_two) (aux₁ hv h), inv_div]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : fract ξ < 2 / (2 * ↑v - 1)
⊢ ↑v + -(1 / 2) = (2 * ↑v - 1) / 2
[PROOFSTEP]
ring
[GOAL]
ξ : ℝ
u v✝ : ℤ
hv : 2 ≤ v✝
h : ContfracLegendre.Ass ξ u v✝
v : ℕ
h' : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
clear h
[GOAL]
ξ : ℝ
u v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
h' : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
have h := h'
[GOAL]
ξ : ℝ
u v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
h' h : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
clear h'
[GOAL]
ξ : ℝ
u v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
h : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
induction v using Nat.strong_induction_on generalizing ξ u with
| h v ih => ?_
[GOAL]
ξ : ℝ
u v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
h : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
induction v using Nat.strong_induction_on generalizing ξ u with
| h v ih => ?_
[GOAL]
case h
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
rcases lt_trichotomy v 1 with (ht | rfl | ht)
[GOAL]
case h.inl
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : v < 1
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
replace h := h.2.2
[GOAL]
case h.inl
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
ht : v < 1
h : |ξ - ↑u / ↑↑v| < (↑↑v * (2 * ↑↑v - 1))⁻¹
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
simp only [Nat.lt_one_iff.mp ht, Nat.cast_zero, div_zero, tsub_zero, zero_mul, cast_zero, inv_zero] at h
[GOAL]
case h.inl
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
ht : v < 1
h : |ξ| < 0
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
exact False.elim (lt_irrefl _ <| (abs_nonneg ξ).trans_lt h)
[GOAL]
case h.inr.inl
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u / ↑1 = convergent ξ n
[PROOFSTEP]
rw [Nat.cast_one, div_one]
[GOAL]
case h.inr.inl
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
h : ContfracLegendre.Ass ξ u ↑1
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
obtain ⟨_, h₁, h₂⟩ := h
[GOAL]
case h.inr.inl.intro.intro
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
cases' le_or_lt (u : ℝ) ξ with ht ht
[GOAL]
case h.inr.inl.intro.intro.inl
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
use 0
[GOAL]
case h
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u = convergent ξ 0
[PROOFSTEP]
rw [convergent_zero, Rat.coe_int_inj, eq_comm, floor_eq_iff]
[GOAL]
case h
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u ≤ ξ ∧ ξ < ↑u + 1
[PROOFSTEP]
convert And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2)
[GOAL]
case h.e'_2.h.e'_4.h.e'_5
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ↑u = ↑u / ↑↑1
[PROOFSTEP]
norm_num
[GOAL]
case h.e'_2.h.e'_4.h.e'_6
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ 1 = (↑↑1 * (2 * ↑↑1 - 1))⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case h.inr.inl.intro.intro.inr
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
replace h₁ := lt_sub_iff_add_lt'.mp (h₁ rfl)
[GOAL]
case h.inr.inl.intro.intro.inr
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
have hξ₁ : ⌊ξ⌋ = u - 1 := by
  rw [floor_eq_iff, cast_sub, cast_one, sub_add_cancel]
  exact ⟨(((sub_lt_sub_iff_left _).mpr one_half_lt_one).trans h₁).le, ht⟩
[GOAL]
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
⊢ ⌊ξ⌋ = u - 1
[PROOFSTEP]
rw [floor_eq_iff, cast_sub, cast_one, sub_add_cancel]
[GOAL]
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
⊢ ↑u - 1 ≤ ξ ∧ ξ < ↑u
[PROOFSTEP]
exact ⟨(((sub_lt_sub_iff_left _).mpr one_half_lt_one).trans h₁).le, ht⟩
[GOAL]
case h.inr.inl.intro.intro.inr
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
cases' eq_or_ne ξ ⌊ξ⌋ with Hξ Hξ
[GOAL]
case h.inr.inl.intro.intro.inr.inl
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁
[GOAL]
case h.inr.inl.intro.intro.inr.inl
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : 1 < 1 / 2
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = ↑⌊ξ⌋
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
exact False.elim (lt_irrefl _ <| h₁.trans one_half_lt_one)
[GOAL]
case h.inr.inl.intro.intro.inr.inr
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
have hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1 :=
  by
  rw [floor_eq_iff, cast_one, le_inv zero_lt_one (fract_pos.mpr Hξ), inv_one, one_add_one_eq_two,
    inv_lt (fract_pos.mpr Hξ) zero_lt_two]
  refine' ⟨(fract_lt_one ξ).le, _⟩
  rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]
  convert h₁ using 1
    -- Porting note: added (`convert` handled this in lean 3)
  rw [sub_eq_add_neg]
  norm_num
[GOAL]
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ ⌊(fract ξ)⁻¹⌋ = 1
[PROOFSTEP]
rw [floor_eq_iff, cast_one, le_inv zero_lt_one (fract_pos.mpr Hξ), inv_one, one_add_one_eq_two,
  inv_lt (fract_pos.mpr Hξ) zero_lt_two]
[GOAL]
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ fract ξ ≤ 1 ∧ 2⁻¹ < fract ξ
[PROOFSTEP]
refine' ⟨(fract_lt_one ξ).le, _⟩
[GOAL]
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ 2⁻¹ < fract ξ
[PROOFSTEP]
rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]
[GOAL]
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ ↑u - (1 - 2⁻¹) < ξ
[PROOFSTEP]
convert h₁ using 1
  -- Porting note: added (`convert` handled this in lean 3)
[GOAL]
case h.e'_3
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ ↑u - (1 - 2⁻¹) = ↑u + -(1 / 2)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
case h.e'_3
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ ↑u + -(1 - 2⁻¹) = ↑u + -(1 / 2)
[PROOFSTEP]
norm_num
[GOAL]
case h.inr.inl.intro.intro.inr.inr
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1
⊢ ∃ n, ↑u = convergent ξ n
[PROOFSTEP]
use 1
[GOAL]
case h
v : ℤ
hv : 2 ≤ v
ξ : ℝ
u : ℤ
ih : ∀ (m : ℕ), m < 1 → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1
⊢ ↑u = convergent ξ 1
[PROOFSTEP]
simp [convergent, hξ₁, hξ₂, cast_sub, cast_one]
[GOAL]
case h.inr.inr
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
obtain ⟨huv₀, huv₁⟩ := aux₂ (Nat.cast_le.mpr ht) h
[GOAL]
case h.inr.inr.intro
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
have Hv : (v : ℚ) ≠ 0 := (Nat.cast_pos.mpr (zero_lt_one.trans ht)).ne'
[GOAL]
case h.inr.inr.intro
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
have huv₁' : (u - ⌊ξ⌋ * v).toNat < v := by zify; rwa [toNat_of_nonneg huv₀.le]
[GOAL]
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
⊢ toNat (u - ⌊ξ⌋ * ↑v) < v
[PROOFSTEP]
zify
[GOAL]
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
⊢ ↑(toNat (u - ⌊ξ⌋ * ↑v)) < ↑v
[PROOFSTEP]
rwa [toNat_of_nonneg huv₀.le]
[GOAL]
case h.inr.inr.intro
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : toNat (u - ⌊ξ⌋ * ↑v) < v
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
have inv : ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * ↑v).toNat :=
  (toNat_of_nonneg huv₀.le).symm ▸ invariant (Nat.cast_le.mpr ht) h
[GOAL]
case h.inr.inr.intro
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : toNat (u - ⌊ξ⌋ * ↑v) < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ ↑v ↑(toNat (u - ⌊ξ⌋ * ↑v))
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
obtain ⟨n, hn⟩ := ih (u - ⌊ξ⌋ * v).toNat huv₁' inv
[GOAL]
case h.inr.inr.intro.intro
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : toNat (u - ⌊ξ⌋ * ↑v) < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ ↑v ↑(toNat (u - ⌊ξ⌋ * ↑v))
n : ℕ
hn : ↑↑v / ↑(toNat (u - ⌊ξ⌋ * ↑v)) = convergent (fract ξ)⁻¹ n
⊢ ∃ n, ↑u / ↑v = convergent ξ n
[PROOFSTEP]
use n + 1
[GOAL]
case h
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : toNat (u - ⌊ξ⌋ * ↑v) < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ ↑v ↑(toNat (u - ⌊ξ⌋ * ↑v))
n : ℕ
hn : ↑↑v / ↑(toNat (u - ⌊ξ⌋ * ↑v)) = convergent (fract ξ)⁻¹ n
⊢ ↑u / ↑v = convergent ξ (n + 1)
[PROOFSTEP]
rw [convergent_succ, ← hn, (by exact_mod_cast toNat_of_nonneg huv₀.le : ((u - ⌊ξ⌋ * v).toNat : ℚ) = u - ⌊ξ⌋ * v),
  cast_ofNat, inv_div, sub_div, mul_div_cancel _ Hv, add_sub_cancel'_right]
[GOAL]
v✝ : ℤ
hv : 2 ≤ v✝
v : ℕ
ih : ∀ (m : ℕ), m < v → ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = convergent ξ n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u ↑v
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * ↑v
huv₁ : u - ⌊ξ⌋ * ↑v < ↑v
Hv : ↑v ≠ 0
huv₁' : toNat (u - ⌊ξ⌋ * ↑v) < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ ↑v ↑(toNat (u - ⌊ξ⌋ * ↑v))
n : ℕ
hn : ↑↑v / ↑(toNat (u - ⌊ξ⌋ * ↑v)) = convergent (fract ξ)⁻¹ n
⊢ ↑(toNat (u - ⌊ξ⌋ * ↑v)) = ↑u - ↑⌊ξ⌋ * ↑v
[PROOFSTEP]
exact_mod_cast toNat_of_nonneg huv₀.le
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ ∃ n, q = convergent ξ n
[PROOFSTEP]
refine' q.num_div_den ▸ exists_rat_eq_convergent' ⟨_, fun hd => _, _⟩
[GOAL]
case refine'_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ IsCoprime q.num ↑q.den
[PROOFSTEP]
exact coprime_iff_nat_coprime.mpr (natAbs_ofNat q.den ▸ q.reduced)
[GOAL]
case refine'_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hd : ↑q.den = 1
⊢ -(1 / 2) < ξ - ↑q.num
[PROOFSTEP]
rw [← q.den_eq_one_iff.mp (Nat.cast_eq_one.mp hd)] at h
[GOAL]
case refine'_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑↑q.num| < 1 / (2 * ↑(↑q.num).den ^ 2)
hd : ↑q.den = 1
⊢ -(1 / 2) < ξ - ↑q.num
[PROOFSTEP]
simpa only [Rat.coe_int_den, Nat.cast_one, one_pow, mul_one] using (abs_lt.mp h).1
[GOAL]
case refine'_3
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹
[PROOFSTEP]
obtain ⟨hq₀, hq₁⟩ := aux₀ (Nat.cast_pos.mpr q.pos)
[GOAL]
case refine'_3.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑↑q.den
hq₁ : 0 < 2 * ↑↑q.den - 1
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹
[PROOFSTEP]
replace hq₁ := mul_pos hq₀ hq₁
[GOAL]
case refine'_3.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑↑q.den
hq₁ : 0 < ↑↑q.den * (2 * ↑↑q.den - 1)
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹
[PROOFSTEP]
have hq₂ : (0 : ℝ) < 2 * (q.den * q.den) := mul_pos zero_lt_two (mul_pos hq₀ hq₀)
[GOAL]
case refine'_3.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑↑q.den
hq₁ : 0 < ↑↑q.den * (2 * ↑↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹
[PROOFSTEP]
rw [cast_ofNat] at *
[GOAL]
case refine'_3.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ |ξ - ↑q.num / ↑q.den| < (↑q.den * (2 * ↑q.den - 1))⁻¹
[PROOFSTEP]
rw [(by norm_cast : (q.num / q.den : ℝ) = (q.num / q.den : ℚ)), Rat.num_div_den]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ ↑q.num / ↑q.den = ↑(↑q.num / ↑q.den)
[PROOFSTEP]
norm_cast
[GOAL]
case refine'_3.intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ |ξ - ↑q| < (↑q.den * (2 * ↑q.den - 1))⁻¹
[PROOFSTEP]
exact h.trans (by rw [← one_div, sq, one_div_lt_one_div hq₂ hq₁, ← sub_pos]; ring_nf; exact hq₀)
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ 1 / (2 * ↑q.den ^ 2) < (↑q.den * (2 * ↑q.den - 1))⁻¹
[PROOFSTEP]
rw [← one_div, sq, one_div_lt_one_div hq₂ hq₁, ← sub_pos]
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ 0 < 2 * (↑q.den * ↑q.den) - ↑q.den * (2 * ↑q.den - 1)
[PROOFSTEP]
ring_nf
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ 0 < ↑q.den
[PROOFSTEP]
exact hq₀
[GOAL]
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ ∃ n, GeneralizedContinuedFraction.convergents (GeneralizedContinuedFraction.of ξ) n = ↑q
[PROOFSTEP]
obtain ⟨n, hn⟩ := exists_rat_eq_convergent h
[GOAL]
case intro
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h✝ : ContfracLegendre.Ass ξ u v
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
n : ℕ
hn : q = convergent ξ n
⊢ ∃ n, GeneralizedContinuedFraction.convergents (GeneralizedContinuedFraction.of ξ) n = ↑q
[PROOFSTEP]
exact ⟨n, hn.symm ▸ continued_fraction_convergent_eq_convergent ξ n⟩