awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Hv : ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + (↑v : ℝ)⁻¹ = 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
rw : HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v + 1) : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹
⊢ HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹

Tactic:
rw [sub_eq_iff_eq_add'.mp huv]

Premises used: Iff.mp, sub_eq_iff_eq_add'
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Hv : ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + (↑v : ℝ)⁻¹ = 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v + 1) : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Hv : ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + (↑v : ℝ)⁻¹ = 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹

Tactic:
have Huv : (u / v : ℝ) = ⌊ξ⌋ + (v : ℝ)⁻¹ := by
      rw [sub_eq_iff_eq_add'.mp huv]; simp [field]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Hv : ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + (↑v : ℝ)⁻¹ = 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Huv : HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹
⊢ ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹

Tactic:
have h' := (abs_sub_lt_iff.mp h.2.2).1
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Hv : ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + (↑v : ℝ)⁻¹ = 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Huv : HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹
h' : ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ fract ξ < 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)

Tactic:
rw [Huv, ← sub_sub, sub_lt_iff_lt_add, self_sub_floor, Hv] at h'

Premises used: sub_sub, Int.self_sub_floor, sub_lt_iff_lt_add
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Hv : ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + (↑v : ℝ)⁻¹ = 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Huv : HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹
h' : fract ξ < 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ (↑v : ℝ) + -(1 / 2) = (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) / 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Hv : ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + (↑v : ℝ)⁻¹ = 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Huv : HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹
h' : fract ξ < 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
refine_2 : (↑v : ℝ) + -(1 / 2) < (fract ξ)⁻¹
refine_2₁ : (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) / 2 < (fract ξ)⁻¹
refine_2₂ : fract ξ < ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) / 2)⁻¹
refine_2₃ refine_2₄ refine_2₅ refine_2₆ : fract ξ < 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)

Tactic:
rwa [lt_sub_iff_add_lt', (by ring : (v : ℝ) + -(1 / 2) = (2 * v - 1) / 2),
      lt_inv_comm₀ (div_pos hv₀' zero_lt_two) (aux₁ hv h), inv_div]

Premises used: lt_sub_iff_add_lt', _private.0.Real.aux₁, lt_inv_comm₀, inv_div, div_pos, zero_lt_two
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n

Tactic:
?_
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
v : ℕ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
h₁ :
  ∀ (v : ℕ)
    (ih :
      ∀ m < v,
        ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
          ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n)
    {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑v : ℤ)),
    ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n

Tactic:
induction v using Nat.strong_induction_on generalizing ξ u with | h v ih => ?_
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
h₁ : ∀ (ht : v < 1), ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
h₂ :
  ∀
    (ih :
      ∀ m < 1,
        ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
          ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n)
    (h : ContfracLegendre.Ass ξ u (↑1 : ℤ)), ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑1 : ℚ) = ξ.convergent n
h₃ : ∀ (ht : 1 < v), ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n

Tactic:
rcases lt_trichotomy v 1 with (ht | rfl | ht)

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : v < 1
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑v : ℤ) : ℝ)| < ((↑(↑v : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑v : ℤ) : ℝ) - 1))⁻¹

Tactic:
replace h := h.2.2
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
ht : v < 1
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑v : ℤ) : ℝ)| < ((↑(↑v : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑v : ℤ) : ℝ) - 1))⁻¹
⊢ |ξ| < 0

Tactic:
simp only [Nat.lt_one_iff.mp ht, Nat.cast_zero, div_zero, tsub_zero, zero_mul,
      cast_zero, inv_zero] at h

Premises used: Int.cast_zero, inv_zero, MulZeroClass.zero_mul, tsub_zero, Nat.lt_one_iff, Iff.mp, Nat.cast_zero, div_zero
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
ht : v < 1
h : |ξ| < 0
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n

Tactic:
False.elim (lt_irrefl _ <| (abs_nonneg ξ).trans_lt h)

Premises used: lt_irrefl, False.elim, LE.le.trans_lt, abs_nonneg
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
ht : v < 1
h : |ξ| < 0
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n

Tactic:
exact False.elim (lt_irrefl _ <| (abs_nonneg ξ).trans_lt h)

Premises used: lt_irrefl, False.elim, LE.le.trans_lt, abs_nonneg
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
h : ContfracLegendre.Ass ξ u (↑1 : ℤ)
h₁ : ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑1 : ℚ) = ξ.convergent n

Tactic:
rw [Nat.cast_one, div_one]

Premises used: div_one, Nat.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
h : ContfracLegendre.Ass ξ u (↑1 : ℤ)
⊢ IsCoprime u (↑1 : ℤ)

Tactic:
obtain ⟨_, h₁, h₂⟩ := h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
h : ContfracLegendre.Ass ξ u (↑1 : ℤ)
left : IsCoprime u (↑1 : ℤ)
⊢ Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)

Tactic:
obtain ⟨_, h₁, h₂⟩ := h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
h : ContfracLegendre.Ass ξ u (↑1 : ℤ)
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹

Tactic:
obtain ⟨_, h₁, h₂⟩ := h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
h : ∀ (ht : (↑u : ℝ) ≤ ξ), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
h₃ : ∀ (ht : ξ < (↑u : ℝ)), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n

Tactic:
rcases le_or_gt (u : ℝ) ξ with ht | ht

Premises used: Int.cast, le_or_gt
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
h : (↑u : ℚ) = ξ.convergent 0
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n

Tactic:
use 0
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
h : (↑u : ℝ) ≤ ξ ∧ ξ < HAdd.hAdd (α := ℝ) (↑u : ℝ) 1
⊢ (↑u : ℚ) = ξ.convergent 0

Tactic:
rw [convergent_zero, Rat.coe_int_inj, eq_comm, floor_eq_iff]

Premises used: Rat.coe_int_inj, Real.convergent_zero, eq_comm, Int.floor_eq_iff
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
⊢ (↑u : ℝ) ≤ ξ ∧
    ξ < HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ) + ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹

Tactic:
And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2)

Premises used: sub_lt_iff_lt_add', And.right, And.intro, Iff.mp, abs_lt
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
h : (↑u : ℝ) = HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)
h₃ : 1 = ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
⊢ (↑u : ℝ) ≤ ξ ∧ ξ < HAdd.hAdd (α := ℝ) (↑u : ℝ) 1

Tactic:
convert! And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2)

Premises used: sub_lt_iff_lt_add', And.right, And.intro, Iff.mp, abs_lt
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
⊢ (↑u : ℝ) = HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
⊢ 1 = ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
⊢ (↑u : ℝ) + -(1 / 2) < ξ

Tactic:
replace h₁ := lt_sub_iff_add_lt'.mp (h₁ rfl)
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
rw : HSub.hSub (α := ℝ) (↑u : ℝ) 1 ≤ ξ ∧ ξ < (↑u : ℝ)
⊢ ⌊ξ⌋ = u - 1

Tactic:
rw [floor_eq_iff, cast_sub, cast_one, sub_add_cancel]

Premises used: Int.cast_sub, Int.floor_eq_iff, sub_add_cancel, Int.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
⊢ HSub.hSub (α := ℝ) (↑u : ℝ) 1 ≤ ξ ∧ ξ < (↑u : ℝ)

Tactic:
⟨(((sub_lt_sub_iff_left _).mpr one_half_lt_one).trans h₁).le, ht⟩

Premises used: Iff.mpr, one_half_lt_one, LT.lt.le, And.intro, LT.lt.trans, sub_lt_sub_iff_left
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
⊢ HSub.hSub (α := ℝ) (↑u : ℝ) 1 ≤ ξ ∧ ξ < (↑u : ℝ)

Tactic:
exact ⟨(((sub_lt_sub_iff_left _).mpr one_half_lt_one).trans h₁).le, ht⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
⊢ ⌊ξ⌋ = u - 1

Tactic:
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⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
h : ∀ (Hξ : ξ = (↑⌊ξ⌋ : ℝ)), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
h₃ : ∀ (Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n

Tactic:
rcases eq_or_ne ξ ⌊ξ⌋ with Hξ | Hξ

Premises used: Int.cast, Int.floor, eq_or_ne
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = (↑⌊ξ⌋ : ℝ)
⊢ 1 < 1 / 2

Tactic:
rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁

Premises used: Int.cast_sub, sub_eq_add_neg, sub_lt_sub_iff_left, Int.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = (↑⌊ξ⌋ : ℝ)
h₃ : 1 < 1 / 2
⊢ ⌊ξ⌋ = u - 1

Tactic:
rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁

Premises used: Int.cast_sub, sub_eq_add_neg, sub_lt_sub_iff_left, Int.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = (↑⌊ξ⌋ : ℝ)
h₃ : 1 < 1 / 2
hξ₂ : ⌊ξ⌋ = u - 1
⊢ ξ = (↑⌊ξ⌋ : ℝ)

Tactic:
rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁

Premises used: Int.cast_sub, sub_eq_add_neg, sub_lt_sub_iff_left, Int.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : 1 < 1 / 2
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = (↑⌊ξ⌋ : ℝ)
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n

Tactic:
False.elim (lt_irrefl _ <| h₁.trans one_half_lt_one)

Premises used: lt_irrefl, False.elim, one_half_lt_one, LT.lt.trans
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : 1 < 1 / 2
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = (↑⌊ξ⌋ : ℝ)
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n

Tactic:
exact False.elim (lt_irrefl _ <| h₁.trans one_half_lt_one)

Premises used: lt_irrefl, False.elim, one_half_lt_one, LT.lt.trans
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
rw : fract ξ ≤ 1 ∧ 2⁻¹ < fract ξ
⊢ ⌊(fract ξ)⁻¹⌋ = 1

Tactic:
rw [floor_eq_iff, cast_one, le_inv_comm₀ zero_lt_one (fract_pos.mpr Hξ), inv_one,
            one_add_one_eq_two, inv_lt_comm₀ (fract_pos.mpr Hξ) zero_lt_two]

Premises used: le_inv_comm₀, Iff.mpr, inv_one, Int.fract_pos, one_add_one_eq_two, Int.floor_eq_iff, zero_lt_one, inv_lt_comm₀, zero_lt_two, Int.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
⊢ fract ξ ≤ 1 ∧ 2⁻¹ < fract ξ

Tactic:
⟨(fract_lt_one ξ).le, ?_⟩

Premises used: LT.lt.le, And.intro, Int.fract_lt_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
refine : 2⁻¹ < fract ξ
⊢ fract ξ ≤ 1 ∧ 2⁻¹ < fract ξ

Tactic:
refine ⟨(fract_lt_one ξ).le, ?_⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
rw : (↑u : ℝ) - HSub.hSub (α := ℝ) 1 2⁻¹ < ξ
⊢ 2⁻¹ < fract ξ

Tactic:
rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]

Premises used: sub_add, lt_sub_iff_add_lt', Int.cast_sub, Int.fract, Int.cast_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
⊢ (↑u : ℝ) + -(1 / 2) < ξ

Tactic:
h₁