awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1

Tactic:
mod_cast this.trans h

Premises used: Int.cast, HMul.hMul, Int.floor, congrArg, HSub.hSub, cast, Int.cast_ofNat, Nat.cast, Int.cast_mul._simp_1, HAdd.hAdd, congr, LT.lt, Int.cast_lt._simp_1, LT.lt.trans, Int.cast_add._simp_1, 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
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 : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1

Tactic:
exact mod_cast this.trans h

Premises used: LT.lt.trans
-- 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:
have hu₁ : u - ⌊ξ⌋ * v ≤ v := by
    refine _root_.le_of_mul_le_mul_right (le_of_lt_add_one ?_) hv₁
    replace h := h.2
    rw [← sub_lt_iff_lt_add, ← mul_assoc, ← sub_mul, ← add_lt_add_iff_right (v * (2 * v - 1) : ℝ),
      add_comm (1 : ℝ)] at h
    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 ξ
    rw [sub_mul ξ, one_mul, ← sub_add, add_mul] at this
    exact mod_cast this.trans h
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
rwa : IsCoprime (u + -(⌊ξ⌋ * v)) v
rwa₁ : IsCoprime (u + -⌊ξ⌋ * v) v
rwa₂ rwa₃ rwa₄ rwa₅ : IsCoprime u v
⊢ IsCoprime (u - ⌊ξ⌋ * v) v

Tactic:
rwa [sub_eq_add_neg, ← neg_mul, IsCoprime.add_mul_right_left_iff]

Premises used: IsCoprime.add_mul_right_left_iff, sub_eq_add_neg, neg_mul
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
⊢ IsCoprime (u - ⌊ξ⌋ * v) v

Tactic:
have huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v := by
    rwa [sub_eq_add_neg, ← neg_mul, IsCoprime.add_mul_right_left_iff]
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v

Tactic:
⟨lt_of_le_of_ne' hu₀ fun hf => ?_, lt_of_le_of_ne hu₁ fun hf => ?_⟩

Premises used: lt_of_le_of_ne', And.intro, lt_of_le_of_ne
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
refine_1 : ∀ (hf : u - ⌊ξ⌋ * v = 0), False
refine_2 : ∀ (hf : u - ⌊ξ⌋ * v = v), False
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v

Tactic:
refine ⟨lt_of_le_of_ne' hu₀ fun hf => ?_, lt_of_le_of_ne hu₁ fun hf => ?_⟩
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
hf : u - ⌊ξ⌋ * v = 0
⊢ IsCoprime 0 v

Tactic:
rw [hf] at huv_cop
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
hf : u - ⌊ξ⌋ * v = 0
huv_cop₁ : IsCoprime 0 v
⊢ u - ⌊ξ⌋ * v = 0

Tactic:
rw [hf] at huv_cop
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime 0 v
hf : u - ⌊ξ⌋ * v = 0
⊢ v = 1 ∨ v = -1

Tactic:
simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop

Premises used: isCoprime_zero_left, isCoprime_self, Int.isUnit_iff
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = 0
huv_cop : v = 1 ∨ v = -1
refine_1 : ∀ (huv_cop : v = 1), False
refine_1₁ : ∀ (huv_cop : v = -1), False
⊢ False

Tactic:
rcases huv_cop with huv_cop | huv_cop
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = 0
huv_cop : v = 1
linarith : -1 + (2 - v) + (v - 1) = 0
⊢ False

Tactic:
linarith only [hv, huv_cop]
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = 0
huv_cop : v = -1
linarith : HMul.hMul (α := ℤ) 3 (-1) + (2 - v) + (v - -1) = 0
linarith₁ : GT.gt (α := ℤ) 3 0
⊢ False

Tactic:
linarith only [hv, huv_cop]
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
hf : u - ⌊ξ⌋ * v = v
⊢ IsCoprime v v

Tactic:
rw [hf] at huv_cop
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
hf : u - ⌊ξ⌋ * v = v
huv_cop₁ : IsCoprime v v
⊢ u - ⌊ξ⌋ * v = v

Tactic:
rw [hf] at huv_cop
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime v v
hf : u - ⌊ξ⌋ * v = v
⊢ v = 1 ∨ v = -1

Tactic:
simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop

Premises used: isCoprime_zero_left, isCoprime_self, Int.isUnit_iff
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = v
huv_cop : v = 1 ∨ v = -1
refine_2 : ∀ (huv_cop : v = 1), False
refine_2₁ : ∀ (huv_cop : v = -1), False
⊢ False

Tactic:
rcases huv_cop with huv_cop | huv_cop
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = v
huv_cop : v = 1
linarith : -1 + (2 - v) + (v - 1) = 0
⊢ False

Tactic:
linarith only [hv, huv_cop]
-- 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
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = v
huv_cop : v = -1
linarith : HMul.hMul (α := ℤ) 3 (-1) + (2 - v) + (v - -1) = 0
linarith₁ : GT.gt (α := ℤ) 3 0
⊢ False

Tactic:
linarith only [hv, huv_cop]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ 0 < u - ⌊ξ⌋ * v

Tactic:
obtain ⟨hu₀, huv⟩ := aux₂ hv h

Premises used: _private.0.Real.aux₂
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hu₀ : 0 < u - ⌊ξ⌋ * v
⊢ u - ⌊ξ⌋ * v < v

Tactic:
obtain ⟨hu₀, huv⟩ := aux₂ hv h

Premises used: _private.0.Real.aux₂
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hu₀ : 0 < u - ⌊ξ⌋ * v
huv : u - ⌊ξ⌋ * v < v
⊢ 0 < fract ξ

Tactic:
have hξ₀ := aux₁ hv h
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hu₀ : 0 < u - ⌊ξ⌋ * v
huv : u - ⌊ξ⌋ * v < v
hξ₀ : 0 < fract ξ
⊢ let u' := u - ⌊ξ⌋ * v;
  0 < u'

Tactic:
set u' := u - ⌊ξ⌋ * v with hu'
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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'
⊢ let u' := u - ⌊ξ⌋ * v;
  u' < v

Tactic:
set u' := u - ⌊ξ⌋ * v with hu'
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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
⊢ let u' := u - ⌊ξ⌋ * v;
  u' = u - ⌊ξ⌋ * v

Tactic:
set u' := u - ⌊ξ⌋ * v with hu'
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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
⊢ (↑u' : ℝ) = (↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)

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

Tactic:
rw [← hu'ℝ]
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
⊢ (↑u : ℝ) = (↑u' : ℝ) + HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)

Tactic:
replace hu'ℝ := (eq_sub_iff_add_eq.mp hu'ℝ).symm
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑u' : ℝ)

Tactic:
obtain ⟨Hu, Hu'⟩ := aux₀ hu₀

Premises used: _private.0.Real.aux₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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' : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑u' : ℝ) - 1

Tactic:
obtain ⟨Hu, Hu'⟩ := aux₀ hu₀

Premises used: _private.0.Real.aux₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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
⊢ 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
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 : ℝ)
⊢ 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
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
⊢ 0 < HDiv.hDiv (α := ℝ) (↑v : ℝ) (↑u' : ℝ) / fract ξ

Tactic:
have H₁ := div_pos (div_pos Hv Hu) hξ₀
-- Module: Mathlib.NumberTheory.DiophantineApproximation.Basic
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 ξ
⊢ |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹

Tactic:
replace h := h.2.2
-- 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))⁻¹
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))⁻¹
rwa₄ rwa₅ rwa₆ 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))⁻¹

Tactic:
rwa [hu'ℝ, add_div, mul_div_cancel_right₀ _ Hv.ne', ← sub_sub, sub_right_comm] at h

Premises used: sub_right_comm, LT.lt.ne', mul_div_cancel_right₀, sub_sub, 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 : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ |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
-- 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))⁻¹
⊢ -((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹ < ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)

Tactic:
replace h := (abs_lt.mp h).1