awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 (↑v : ℝ) - 1) *
      (-((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) =
    HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ)

Tactic:
field
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 (↑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
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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' : ℝ) - 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

Premises used: sub_right_comm, LT.lt.ne', mul_div_cancel_right₀, sub_sub, Int.self_sub_floor, mul_lt_mul_iff_right₀, lt_sub_iff_add_lt, add_div
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
h₁ :
  HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ) <
    (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ
⊢ (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:
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

Premises used: sub_right_comm, LT.lt.ne', mul_div_cancel_right₀, sub_sub, Int.self_sub_floor, mul_lt_mul_iff_right₀, lt_sub_iff_add_lt, add_div
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 ξ

Tactic:
LE.le.trans ?_ h.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
refine : HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ

Tactic:
refine LE.le.trans ?_ h.le

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
rw : HAdd.hAdd (α := ℝ) (↑u' : ℝ) 1 ≤ (↑v : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1 ≤ HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - HAdd.hAdd (α := ℝ) 1 (↑u' : ℝ) / (↑v : ℝ)

Tactic:
rw [sub_le_sub_iff_left, div_le_one Hv, add_comm]

Premises used: sub_le_sub_iff_left, add_comm, div_le_one
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑u' : ℝ) 1 ≤ (↑v : ℝ)

Tactic:
mod_cast huv

Premises used: Int.cast, congrArg, cast, LE.le, Int.cast_le._simp_1, Nat.cast, HAdd.hAdd, Int.cast_add._simp_1, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, Int.cast_one, Eq.trans
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑u' : ℝ) 1 ≤ (↑v : ℝ)

Tactic:
exact mod_cast huv
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 ξ

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
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 :
  |HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) - (fract ξ)⁻¹| =
    |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| =
    |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|

Tactic:
rw [abs_sub_comm]

Premises used: abs_sub_comm
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 ξ
e_a :
  HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) - (fract ξ)⁻¹ =
    (fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)
⊢ |HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) - (fract ξ)⁻¹| =
    |(fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)) * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)|

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 ξ)

Tactic:
field
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 ξ)
rw₁ 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 ξ)

Tactic:
rw [abs_mul, abs_of_pos H₁]

Premises used: abs_mul, abs_of_pos
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 ξ
ha : 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ
⊢ |fract ξ - HDiv.hDiv (α := ℝ) (↑u' : ℝ) (↑v : ℝ)| * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ) <
    ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ * (HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ) =
    ((↑u' : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ))⁻¹

Tactic:
field
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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)
hba : LE.le (α := ℝ) 0 (↑u' : ℝ)
⊢ ((↑u' : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ))⁻¹ ≤ ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 ξ))⁻¹
v₅ :
  ((↑u' : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) * fract ξ))⁻¹ ≤ ((↑u' : ℝ) * (HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1))⁻¹
⊢ |(fract ξ)⁻¹ - HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ)| < ((↑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

Premises used: Int.cast, HMul.hMul, Int.fract, HSub.hSub, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * v)

Tactic:
⟨?_, fun huv => ?_, mod_cast aux₃ hv h⟩

Premises used: _private.0.Real.aux₃, Int.cast, HMul.hMul, Int.floor, abs, congrArg, Int.fract, Rat.divInt, HSub.hSub, cast, Rat.cast_divInt._simp_1, HDiv.hDiv, Rat.cast, Int.cast_ofNat, Nat.cast, Real.ContfracLegendre.Ass, Inv.inv, Int.cast_mul._simp_1, And.intro, congr, LT.lt, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, Int.cast_one, Eq.trans, Int.cast_sub._simp_1
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
refine_1 : IsCoprime v (u - ⌊ξ⌋ * v)
refine_2 : ∀ (huv : u - ⌊ξ⌋ * v = 1), -(1 / 2) < (fract ξ)⁻¹ - (↑v : ℝ)
⊢ ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * v)

Tactic:
refine ⟨?_, fun huv => ?_, mod_cast aux₃ hv h⟩
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
refine_1 : IsCoprime u v
⊢ IsCoprime v (u - ⌊ξ⌋ * v)

Tactic:
rw [sub_eq_add_neg, ← neg_mul, isCoprime_comm, IsCoprime.add_mul_right_left_iff]

Premises used: isCoprime_comm, IsCoprime.add_mul_right_left_iff, sub_eq_add_neg, neg_mul
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ IsCoprime u v

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ IsCoprime u v

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1

Tactic:
obtain hv₀' := (aux₀ (zero_lt_two.trans_le hv)).2

Premises used: _private.0.Real.aux₀, And.right, LT.lt.trans_le, zero_lt_two
-- 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
⊢ ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ + (↑v : ℝ)⁻¹ = 2 / (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)

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
⊢ ((↑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]