awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
Tactic: 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
    rw [hu'ℝ, add_div, mul_div_cancel_right₀ _ Hv.ne', ← sub_sub, sub_right_comm, self_sub_floor,
      lt_sub_iff_add_lt, ← mul_lt_mul_iff_right₀ 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
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| =
    |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|
have rw : |HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) - (fract ξ)⁻¹| =
  |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|
Tactic: rw [abs_sub_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
⊢ |HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) - (fract ξ)⁻¹| =
    |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|
have e_a : HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) - (fract ξ)⁻¹ =
  (fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
⊢ |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)| =
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
have rw : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * |HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ| =
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
Tactic: rw [abs_mul, abs_of_pos H₁]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
rw :
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * |HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ| =
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
⊢ |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)| =
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
have rw₁ : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ) =
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
Tactic: rw [abs_mul, abs_of_pos H₁]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
⊢ ((↑u' : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ))⁻¹ ≤ ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have hb : 0 < (↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
hb : 0 < (↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1)
⊢ ((↑u' : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ))⁻¹ ≤ ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have hba : LE.le (α := ℝ) 0 (↑u' : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have v₁ : |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| =
  |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|
Tactic: calc
    |(fract ξ)⁻¹ - v / u'| = |(fract ξ - u' / v) * (v / u' / fract ξ)| := by
      rw [abs_sub_comm]; congr 1; field
    _ = |fract ξ - u' / v| * (v / u' / fract ξ) := by rw [abs_mul, abs_of_pos H₁]
    _ < ((v : ℝ) * (2 * v - 1))⁻¹ * (v / u' / fract ξ) := by gcongr
    _ = (u' * ((2 * v - 1) * fract ξ))⁻¹ := by field
    _ ≤ (u' * (2 * u' - 1) : ℝ)⁻¹ := by gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
v₁ :
  |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| =
    |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have v₂ : |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)| =
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
Tactic: calc
    |(fract ξ)⁻¹ - v / u'| = |(fract ξ - u' / v) * (v / u' / fract ξ)| := by
      rw [abs_sub_comm]; congr 1; field
    _ = |fract ξ - u' / v| * (v / u' / fract ξ) := by rw [abs_mul, abs_of_pos H₁]
    _ < ((v : ℝ) * (2 * v - 1))⁻¹ * (v / u' / fract ξ) := by gcongr
    _ = (u' * ((2 * v - 1) * fract ξ))⁻¹ := by field
    _ ≤ (u' * (2 * u' - 1) : ℝ)⁻¹ := by gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
v₁ :
  |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| =
    |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|
v₂ :
  |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)| =
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have v₃ : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ) <
  ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
Tactic: calc
    |(fract ξ)⁻¹ - v / u'| = |(fract ξ - u' / v) * (v / u' / fract ξ)| := by
      rw [abs_sub_comm]; congr 1; field
    _ = |fract ξ - u' / v| * (v / u' / fract ξ) := by rw [abs_mul, abs_of_pos H₁]
    _ < ((v : ℝ) * (2 * v - 1))⁻¹ * (v / u' / fract ξ) := by gcongr
    _ = (u' * ((2 * v - 1) * fract ξ))⁻¹ := by field
    _ ≤ (u' * (2 * u' - 1) : ℝ)⁻¹ := by gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
v₁ :
  |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| =
    |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|
v₂ :
  |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)| =
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
v₃ :
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ) <
    ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have v₄ : ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ) =
  ((↑u' : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ))⁻¹
Tactic: calc
    |(fract ξ)⁻¹ - v / u'| = |(fract ξ - u' / v) * (v / u' / fract ξ)| := by
      rw [abs_sub_comm]; congr 1; field
    _ = |fract ξ - u' / v| * (v / u' / fract ξ) := by rw [abs_mul, abs_of_pos H₁]
    _ < ((v : ℝ) * (2 * v - 1))⁻¹ * (v / u' / fract ξ) := by gcongr
    _ = (u' * ((2 * v - 1) * fract ξ))⁻¹ := by field
    _ ≤ (u' * (2 * u' - 1) : ℝ)⁻¹ := by gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
H : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
v₁ :
  |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| =
    |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|
v₂ :
  |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)| =
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
v₃ :
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ) <
    ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
v₄ :
  ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ) =
    ((↑u' : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ))⁻¹
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have v₅ : ((↑u' : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ))⁻¹ ≤ ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
Tactic: calc
    |(fract ξ)⁻¹ - v / u'| = |(fract ξ - u' / v) * (v / u' / fract ξ)| := by
      rw [abs_sub_comm]; congr 1; field
    _ = |fract ξ - u' / v| * (v / u' / fract ξ) := by rw [abs_mul, abs_of_pos H₁]
    _ < ((v : ℝ) * (2 * v - 1))⁻¹ * (v / u' / fract ξ) := by gcongr
    _ = (u' * ((2 * v - 1) * fract ξ))⁻¹ := by field
    _ ≤ (u' * (2 * u' - 1) : ℝ)⁻¹ := by gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * v)
have refine_1 : IsCoprime v (u - ⌊ξ⌋ * v)
Tactic: refine ⟨?_, fun huv => ?_, mod_cast aux₃ hv h⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
refine_1 : IsCoprime v (u - ⌊ξ⌋ * v)
⊢ ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * v)
have refine_2 : ∀ (huv : u - ⌊ξ⌋ * v = 1), -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
Tactic: refine ⟨?_, fun huv => ?_, mod_cast aux₃ hv h⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ IsCoprime v (u - ⌊ξ⌋ * v)
have refine_1 : IsCoprime u v
Tactic: rw [sub_eq_add_neg, ← neg_mul, isCoprime_comm, IsCoprime.add_mul_right_left_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
⊢ -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
have hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Tactic: obtain hv₀' := (aux₀ (zero_lt_two.trans_le hv)).2
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
⊢ -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
have Hv : ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + (↑v : ℝ)⁻¹ = 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Tactic: have Hv : (v * (2 * v - 1) : ℝ)⁻¹ + (v : ℝ)⁻¹ = 2 / (2 * v - 1) := by
      simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 : ℝ)⁻¹
have rw : HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v + 1) : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹
Tactic: rw [sub_eq_iff_eq_add'.mp huv]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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)
⊢ -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
have Huv : HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = HAdd.hAdd (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)⁻¹
Tactic: have Huv : (u / v : ℝ) = ⌊ξ⌋ + (v : ℝ)⁻¹ := by
      rw [sub_eq_iff_eq_add'.mp huv]; simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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 : ℝ)⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
have h' : ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: have h' := (abs_sub_lt_iff.mp h.2.2).1
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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))⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
have h'₁ : fract ξ < 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Tactic: rw [Huv, ← sub_sub, sub_lt_iff_lt_add, self_sub_floor, Hv] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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)
⊢ -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
have refine_2 : (↑v : ℝ) + -(1 / 2) < (fract ξ)⁻¹
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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 ξ)⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
have refine_2₁ : (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) / 2 < (fract ξ)⁻¹
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]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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 ξ)⁻¹
⊢ -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
have refine_2₂ : fract ξ < ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) / 2)⁻¹
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]