awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
refine : (↑v : ℝ)⁻¹ ≤ |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)|
⊢ HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1 < 1

Tactic:
refine (mul_lt_iff_lt_one_right hv₀).1 ((inv_lt_inv₀ hv₀ (mul_pos hv₁ hv₂)).1 (h.trans_le' ?_))

Premises used: LT.lt.trans_le', mul_pos, Iff.mp, mul_lt_iff_lt_one_right, inv_lt_inv₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
⊢ (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)) / (↑v : ℝ)

Tactic:
field
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
⊢ (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)) / (↑v : ℝ)

Tactic:
have h' : (⌊ξ⌋ : ℝ) - u / v = (⌊ξ⌋ * v - u) / v := by field
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
h' : (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)) / (↑v : ℝ)
rw : 1 ≤ |HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)|
⊢ (↑v : ℝ)⁻¹ ≤ |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)|

Tactic:
rw [h', abs_div, abs_of_pos hv₀, ← one_div, div_le_div_iff_of_pos_right hv₀]

Premises used: abs_div, div_le_div_iff_of_pos_right, one_div, abs_of_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
h' : (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)) / (↑v : ℝ)
norm_cast : 1 ≤ |⌊ξ⌋ * v - u|
⊢ 1 ≤ |HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)|

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
h' : (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)) / (↑v : ℝ)
rw : ⌊ξ⌋ * v ≠ u
⊢ 1 ≤ |⌊ξ⌋ * v - u|

Tactic:
rw [← zero_add (1 : ℤ), add_one_le_iff, abs_pos, sub_ne_zero]

Premises used: sub_ne_zero, Int.add_one_le_iff, zero_add, abs_pos, OfNat.ofNat
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hf : ξ = (↑⌊ξ⌋ : ℝ)
hcop : IsCoprime (⌊ξ⌋ * v) v
left : v = 1 → -(1 / 2) < ξ - (↑(⌊ξ⌋ * v) : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' :
  (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ) =
    (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑(⌊ξ⌋ * v) : ℝ)) / (↑v : ℝ)
inl : v = 1 → False
inr : v = -1 → False
⊢ False

Tactic:
cases isUnit_iff.mp (isCoprime_self.mp (IsCoprime.mul_left_iff.mp hcop).2)

Premises used: isCoprime_self, And.right, Iff.mp, Int.isUnit_iff, IsCoprime.mul_left_iff
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hf : ξ = (↑⌊ξ⌋ : ℝ)
hcop : IsCoprime (⌊ξ⌋ * v) v
left : v = 1 → -(1 / 2) < ξ - (↑(⌊ξ⌋ * v) : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' :
  (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ) =
    (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑(⌊ξ⌋ * v) : ℝ)) / (↑v : ℝ)
h_1 : v = 1
⊢ False

Tactic:
lia
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hf : ξ = (↑⌊ξ⌋ : ℝ)
hcop : IsCoprime (⌊ξ⌋ * v) v
left : v = 1 → -(1 / 2) < ξ - (↑(⌊ξ⌋ * v) : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' :
  (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ) =
    (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑(⌊ξ⌋ * v) : ℝ)) / (↑v : ℝ)
h_1 : v = -1
⊢ False

Tactic:
lia
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1 < 1

Tactic:
have H : (2 * v - 1 : ℝ) < 1 := by
    refine (mul_lt_iff_lt_one_right hv₀).1 ((inv_lt_inv₀ hv₀ (mul_pos hv₁ hv₂)).1 (h.trans_le' ?_))
    have h' : (⌊ξ⌋ : ℝ) - u / v = (⌊ξ⌋ * v - u) / v := by field
    rw [h', abs_div, abs_of_pos hv₀, ← one_div, div_le_div_iff_of_pos_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) <;> lia
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
H : HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1 < 1
⊢ 2 * v - 1 < 1

Tactic:
norm_cast at H
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
H : 2 * v - 1 < 1
linarith : HMul.hMul (α := ℤ) 3 (-1) + 2 * (2 - v) + (2 * v - 1 + 1 - 1) = 0
linarith₁ : GT.gt (α := ℤ) 3 0
linarith₂ : GT.gt (α := ℤ) 2 0
⊢ False

Tactic:
linarith only [hv, H]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ IsCoprime u v

Tactic:
obtain ⟨hcop, _, h⟩ := h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hcop : IsCoprime u v
⊢ v = 1 → -(1 / 2) < ξ - (↑u : ℝ)

Tactic:
obtain ⟨hcop, _, h⟩ := h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹

Tactic:
obtain ⟨hcop, _, h⟩ := h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ LT.lt (α := ℝ) 0 (↑v : ℝ)

Tactic:
obtain ⟨hv₀, hv₀'⟩ := aux₀ (zero_lt_two.trans_le hv)

Premises used: _private.0.Real.aux₀, LT.lt.trans_le, zero_lt_two
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1

Tactic:
obtain ⟨hv₀, hv₀'⟩ := aux₀ (zero_lt_two.trans_le hv)

Premises used: _private.0.Real.aux₀, LT.lt.trans_le, zero_lt_two
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
linarith : 2 * v - 1 ≤ 0 → HMul.hMul (α := ℤ) 3 (-1) + (2 * v - 1 - 0) + 2 * (2 - v) = 0
linarith₁ : 2 * v - 1 ≤ 0 → GT.gt (α := ℤ) 3 0
linarith₂ : 2 * v - 1 ≤ 0 → GT.gt (α := ℤ) 2 0
⊢ 0 < 2 * v - 1

Tactic:
linarith only [hv]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
⊢ 0 < 2 * v - 1

Tactic:
have hv₁ : 0 < 2 * v - 1 := by linarith only [hv]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
⊢ -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))

Tactic:
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

Premises used: div_mul_cancel₀, lt_div_iff₀, mul_assoc, abs_mul, LT.lt.ne', sub_mul, mul_pos, one_div, abs_lt, sub_lt_iff_lt_add, abs_sub_comm, abs_of_pos, lt_sub_iff_add_lt
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
h₁ :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
⊢ LT.lt (α := ℝ) 0 (↑v : ℝ)

Tactic:
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

Premises used: div_mul_cancel₀, lt_div_iff₀, mul_assoc, abs_mul, LT.lt.ne', sub_mul, mul_pos, one_div, abs_lt, sub_lt_iff_lt_add, abs_sub_comm, abs_of_pos, lt_sub_iff_add_lt
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
h₁ :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₂ : LT.lt (α := ℝ) 0 (↑v : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1

Tactic:
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

Premises used: div_mul_cancel₀, lt_div_iff₀, mul_assoc, abs_mul, LT.lt.ne', sub_mul, mul_pos, one_div, abs_lt, sub_lt_iff_lt_add, abs_sub_comm, abs_of_pos, lt_sub_iff_add_lt
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
h₁ :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₂ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀'₁ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
⊢ 0 < 2 * v - 1

Tactic:
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

Premises used: div_mul_cancel₀, lt_div_iff₀, mul_assoc, abs_mul, LT.lt.ne', sub_mul, mul_pos, one_div, abs_lt, sub_lt_iff_lt_add, abs_sub_comm, abs_of_pos, lt_sub_iff_add_lt
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 ≤ u - ⌊ξ⌋ * v

Tactic:
(mul_nonneg_iff_of_pos_right hv₁).mp ?_

Premises used: mul_nonneg_iff_of_pos_right, Iff.mp
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
refine : 0 ≤ (u - ⌊ξ⌋ * v) * (2 * v - 1)
⊢ 0 ≤ u - ⌊ξ⌋ * v

Tactic:
refine (mul_nonneg_iff_of_pos_right hv₁).mp ?_

Premises used: mul_nonneg_iff_of_pos_right, Iff.mp
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
⊢ -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)

Tactic:
replace h := h.1
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
h : -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ -1 < ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)

Tactic:
rw [← lt_sub_iff_add_lt, ← mul_assoc, ← sub_mul] at h

Premises used: mul_assoc, sub_mul, lt_sub_iff_add_lt
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
h : -1 < ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)

Tactic:
mod_cast
      h.trans_le
        ((mul_le_mul_iff_left₀ <| hv₀').mpr <|
          (sub_le_sub_iff_left (u : ℝ)).mpr ((mul_le_mul_iff_left₀ hv₀).mpr (floor_le ξ)))

Premises used: Iff.mpr, Int.cast, HMul.hMul, Int.floor, congrArg, Int.cast_negSucc._simp_1, HSub.hSub, cast, sub_le_sub_iff_left, Int.cast_ofNat, Nat.cast, Int.cast_mul._simp_1, LT.lt.trans_le, congr, LT.lt, Int.cast_lt._simp_1, Int.floor_le, congrFun', Int.negSucc, mul_le_mul_iff_left₀, OfNat.ofNat, Eq.symm, Nat.cast_one, Neg.neg, Int.cast_one, Eq.trans, Int.cast_sub._simp_1
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
h : -1 < ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)

Tactic:
exact mod_cast
      h.trans_le
        ((mul_le_mul_iff_left₀ <| hv₀').mpr <|
          (sub_le_sub_iff_left (u : ℝ)).mpr ((mul_le_mul_iff_left₀ hv₀).mpr (floor_le ξ)))

Premises used: Iff.mpr, Int.cast, sub_le_sub_iff_left, LT.lt.trans_le, Int.floor_le, mul_le_mul_iff_left₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 ≤ u - ⌊ξ⌋ * v

Tactic:
have hu₀ : 0 ≤ u - ⌊ξ⌋ * v := by
    refine (mul_nonneg_iff_of_pos_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_iff_left₀ <| hv₀').mpr <|
          (sub_le_sub_iff_left (u : ℝ)).mpr ((mul_le_mul_iff_left₀ hv₀).mpr (floor_le ξ)))
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
⊢ u - ⌊ξ⌋ * v ≤ v

Tactic:
_root_.le_of_mul_le_mul_right (le_of_lt_add_one ?_) hv₁

Premises used: le_of_mul_le_mul_right, Int.le_of_lt_add_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
refine : (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
⊢ u - ⌊ξ⌋ * v ≤ v

Tactic:
refine _root_.le_of_mul_le_mul_right (le_of_lt_add_one ?_) hv₁

Premises used: le_of_mul_le_mul_right, Int.le_of_lt_add_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
⊢ (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))

Tactic:
replace h := h.2
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
⊢ ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
    (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + 1

Tactic:
rw [← sub_lt_iff_lt_add, ← mul_assoc, ← sub_mul, ← add_lt_add_iff_right (v * (2 * v - 1) : ℝ),
      add_comm (1 : ℝ)] at h

Premises used: Int.cast, HMul.hMul, mul_assoc, HSub.hSub, add_comm, sub_mul, sub_lt_iff_lt_add, OfNat.ofNat, add_lt_add_iff_right
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h :
  ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
    (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + 1
⊢ ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
    ((↑u : ℝ) - (ξ - 1) * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)

Tactic:
have :=
      flip mul_lt_mul_of_pos_right hv₀' <| (sub_lt_sub_iff_left (u : ℝ)).mpr <|
          flip mul_lt_mul_of_pos_right hv₀ <| sub_right_lt_of_lt_add <| lt_floor_add_one ξ
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h :
  ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
    (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + 1
this :
  ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
    ((↑u : ℝ) - (ξ - 1) * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
    ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)

Tactic:
rw [sub_mul ξ, one_mul, ← sub_add, add_mul] at this

Premises used: sub_add, add_mul, sub_mul, one_mul