awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = v
huv_cop : v = -1
⊢ False
have linarith : HMul.hMul (α := ℤ) 3 (-1) + (2 - v) + (v - -1) = 0
Tactic: linarith only [hv, huv_cop]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = v
huv_cop : v = -1
linarith : HMul.hMul (α := ℤ) 3 (-1) + (2 - v) + (v - -1) = 0
⊢ False
have linarith₁ : GT.gt (α := ℤ) 3 0
Tactic: linarith only [hv, huv_cop]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ |(fract ξ)⁻¹ - (↑v : ℝ) / ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ))| <
    (((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) *
        (2 * ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) - 1))⁻¹
have hu₀ : 0 < u - ⌊ξ⌋ * v
Tactic: obtain ⟨hu₀, huv⟩ := aux₂ hv h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hu₀ : 0 < u - ⌊ξ⌋ * v
⊢ |(fract ξ)⁻¹ - (↑v : ℝ) / ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ))| <
    (((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) *
        (2 * ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) - 1))⁻¹
have huv : u - ⌊ξ⌋ * v < v
Tactic: obtain ⟨hu₀, huv⟩ := aux₂ hv h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hu₀ : 0 < u - ⌊ξ⌋ * v
huv : u - ⌊ξ⌋ * v < v
⊢ |(fract ξ)⁻¹ - (↑v : ℝ) / ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ))| <
    (((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) *
        (2 * ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) - 1))⁻¹
have hξ₀ : 0 < fract ξ
Tactic: have hξ₀ := aux₁ hv h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hu₀ : 0 < u - ⌊ξ⌋ * v
huv : u - ⌊ξ⌋ * v < v
hξ₀ : 0 < fract ξ
hu₁ :
  let u' := u - ⌊ξ⌋ * v;
  0 < u'
huv₁ :
  let u' := u - ⌊ξ⌋ * v;
  u' < v
⊢ |(fract ξ)⁻¹ - (↑v : ℝ) / ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ))| <
    (((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) *
        (2 * ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) - 1))⁻¹
have hu' : let u' := u - ⌊ξ⌋ * v;
u' = u - ⌊ξ⌋ * v
Tactic: set u' := u - ⌊ξ⌋ * v with hu'
Cleared hypotheses: hu₀, huv
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
⊢ |(fract ξ)⁻¹ - (↑v : ℝ) / ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ))| <
    (((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) *
        (2 * ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) - 1))⁻¹
have hu'ℝ : (↑u' : ℝ) = (↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Tactic: have hu'ℝ : (u' : ℝ) = u - ⌊ξ⌋ * v := mod_cast hu'
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
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
hu'ℝ : (↑u' : ℝ) = (↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
⊢ |(fract ξ)⁻¹ - (↑v : ℝ) / ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ))| <
    (((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) *
        (2 * ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) - 1))⁻¹
have rw : |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
Tactic: rw [← hu'ℝ]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
hu'ℝ : (↑u' : ℝ) = (↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have hu'ℝ₁ : (↑u : ℝ) = (↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Tactic: replace hu'ℝ := (eq_sub_iff_add_eq.mp hu'ℝ).symm
Cleared hypotheses: hu'ℝ
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
hu'ℝ : (↑u : ℝ) = (↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Tactic: obtain ⟨Hu, Hu'⟩ := aux₀ hu₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
hu'ℝ : (↑u : ℝ) = (↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Tactic: obtain ⟨Hu, Hu'⟩ := aux₀ hu₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
hu'ℝ : (↑u : ℝ) = (↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
Tactic: obtain ⟨Hv, Hv'⟩ := aux₀ (zero_lt_two.trans_le hv)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
hu'ℝ : (↑u : ℝ) = (↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)
Hu : LT.lt (α := ℝ) 0 (↑u' : ℝ)
Hu' : 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1
Hv : LT.lt (α := ℝ) 0 (↑v : ℝ)
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have Hv' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Tactic: obtain ⟨Hv, Hv'⟩ := aux₀ (zero_lt_two.trans_le hv)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
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
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have H₁ : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
Tactic: have H₁ := div_pos (div_pos Hv Hu) hξ₀
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
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 ξ
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have h₁ : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: replace h := h.2.2
Cleared hypotheses: 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))⁻¹
⊢ |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
have rwa : ∀
  (h :
    |ξ - ((↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) / (↑v : ℝ)| <
      ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: rwa [hu'ℝ, add_div, mul_div_cancel_right₀ _ Hv.ne', ← sub_sub, sub_right_comm] at h
Cleared hypotheses: 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))⁻¹
rwa :
  ∀
    (h :
      |ξ - ((↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) / (↑v : ℝ)| <
        ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
have rwa₁ : ∀
  (h :
    |ξ - (HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) / (↑v : ℝ))| <
      ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: rwa [hu'ℝ, add_div, mul_div_cancel_right₀ _ Hv.ne', ← sub_sub, sub_right_comm] at h
Cleared hypotheses: 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))⁻¹
rwa :
  ∀
    (h :
      |ξ - ((↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) / (↑v : ℝ)| <
        ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
rwa₁ :
  ∀
    (h :
      |ξ - (HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) / (↑v : ℝ))| <
        ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
have rwa₂ : ∀ (h : |ξ - (HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ) + (↑⌊ξ⌋ : ℝ))| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: rwa [hu'ℝ, add_div, mul_div_cancel_right₀ _ Hv.ne', ← sub_sub, sub_right_comm] at h
Cleared hypotheses: 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))⁻¹
rwa :
  ∀
    (h :
      |ξ - ((↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) / (↑v : ℝ)| <
        ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
rwa₁ :
  ∀
    (h :
      |ξ - (HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) / (↑v : ℝ))| <
        ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
rwa₂ :
  ∀
    (h :
      |ξ - (HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ) + (↑⌊ξ⌋ : ℝ))| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
have rwa₃ : ∀ (h : |ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ) - (↑⌊ξ⌋ : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: rwa [hu'ℝ, add_div, mul_div_cancel_right₀ _ Hv.ne', ← sub_sub, sub_right_comm] at h
Cleared hypotheses: 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))⁻¹
rwa :
  ∀
    (h :
      |ξ - ((↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) / (↑v : ℝ)| <
        ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
rwa₁ :
  ∀
    (h :
      |ξ - (HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) / (↑v : ℝ))| <
        ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
rwa₂ :
  ∀
    (h :
      |ξ - (HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ) + (↑⌊ξ⌋ : ℝ))| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
rwa₃ :
  ∀ (h : |ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ) - (↑⌊ξ⌋ : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
    |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
have rwa₄ : ∀ (h : |ξ - (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹),
  |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: rwa [hu'ℝ, add_div, mul_div_cancel_right₀ _ Hv.ne', ← sub_sub, sub_right_comm] at h
Cleared hypotheses: h
-- 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))⁻¹
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
have h' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: have h' : |fract ξ - u' / v| < ((v : ℝ) * (2 * v - 1))⁻¹ := by
    rwa [hu'ℝ, add_div, mul_div_cancel_right₀ _ Hv.ne', ← sub_sub, sub_right_comm] at h
-- 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))⁻¹
⊢ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
have h₁ : -((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ < ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)
Tactic: replace h := (abs_lt.mp h).1
Cleared hypotheses: h
-- 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' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h : -((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ < ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
have this : (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) *
    (-((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) =
  HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ)
Tactic: have : (2 * (v : ℝ) - 1) * (-((v : ℝ) * (2 * v - 1))⁻¹ + u' / v) = 2 * u' - (1 + u') / v := by
      field
-- 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' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h : -((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ < ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)
this :
  (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) *
      (-((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) =
    HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
have h₁ : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ) <
  (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
Tactic: 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
Cleared hypotheses: h, this
-- 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' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h :
  HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ) <
    (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
this :
  (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) *
      (-((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) =
    HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
have refine : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ)
Tactic: refine LE.le.trans ?_ h.le
-- 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' : |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h :
  HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ) <
    (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
this :
  (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) *
      (-((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) =
    HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ)
have rw : HAdd.hAdd (α := ℝ) (↑u' : ℝ) 1 ≤ (↑v : ℝ)
Tactic: rw [sub_le_sub_iff_left, div_le_one Hv, add_comm]