awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
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
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
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 (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
⊢ 0 < 2 * v - 1
have linarith : 2 * v - 1 ≤ 0 → HMul.hMul (α := ℤ) 3 (-1) + (2 * v - 1 - 0) + 2 * (2 - v) = 0
Tactic: linarith only [hv]
-- 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 : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
linarith : 2 * v - 1 ≤ 0 → HMul.hMul (α := ℤ) 3 (-1) + (2 * v - 1 - 0) + 2 * (2 - v) = 0
⊢ 0 < 2 * v - 1
have linarith₁ : 2 * v - 1 ≤ 0 → GT.gt (α := ℤ) 3 0
Tactic: linarith only [hv]
-- 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 : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
linarith : 2 * v - 1 ≤ 0 → HMul.hMul (α := ℤ) 3 (-1) + (2 * v - 1 - 0) + 2 * (2 - v) = 0
linarith₁ : 2 * v - 1 ≤ 0 → GT.gt (α := ℤ) 3 0
⊢ 0 < 2 * v - 1
have linarith₂ : 2 * v - 1 ≤ 0 → GT.gt (α := ℤ) 2 0
Tactic: linarith only [hv]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have hv₁ : 0 < 2 * v - 1
Tactic: have hv₁ : 0 < 2 * v - 1 := by linarith only [hv]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have 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))
Tactic: rw [← one_div, lt_div_iff₀ (mul_pos hv₀ hv₀'), ← abs_of_pos (mul_pos hv₀ hv₀'), ← abs_mul,
    sub_mul, ← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ hv₀.ne', abs_sub_comm, abs_lt,
    lt_sub_iff_add_lt, sub_lt_iff_lt_add, mul_assoc] at h
Cleared hypotheses: h, hv₀, hv₀', hv₁
-- 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
⊢ 0 ≤ u - ⌊ξ⌋ * v
have refine : 0 ≤ (u - ⌊ξ⌋ * v) * (2 * v - 1)
Tactic: refine (mul_nonneg_iff_of_pos_right hv₁).mp ?_
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)
have h₁ : -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Tactic: replace h := h.1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
h : -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)
have h₁ : -1 < ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Tactic: rw [← lt_sub_iff_add_lt, ← mul_assoc, ← sub_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h :
  -1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)) < (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) ∧
    (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have hu₀ : 0 ≤ u - ⌊ξ⌋ * v
Tactic: have hu₀ : 0 ≤ u - ⌊ξ⌋ * v := by
    refine (mul_nonneg_iff_of_pos_right hv₁).mp ?_
    rw [← sub_one_lt_iff, zero_sub]
    replace h := h.1
    rw [← lt_sub_iff_add_lt, ← mul_assoc, ← sub_mul] at h
    exact mod_cast
      h.trans_le
        ((mul_le_mul_iff_left₀ <| hv₀').mpr <|
          (sub_le_sub_iff_left (u : ℝ)).mpr ((mul_le_mul_iff_left₀ hv₀).mpr (floor_le ξ)))
-- 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
⊢ u - ⌊ξ⌋ * v ≤ v
have refine : (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
Tactic: refine _root_.le_of_mul_le_mul_right (le_of_lt_add_one ?_) hv₁
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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) * (2 * v - 1) < v * (2 * v - 1) + 1
have h₁ : (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
Tactic: replace h := h.2
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) < 1 + ξ * ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
have h₁ : ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
  (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + 1
Tactic: rw [← sub_lt_iff_lt_add, ← mul_assoc, ← sub_mul, ← add_lt_add_iff_right (v * (2 * v - 1) : ℝ),
      add_comm (1 : ℝ)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h :
  ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
    (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + 1
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
have this : ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
  ((↑u : ℝ) - (ξ - 1) * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Tactic: have :=
      flip mul_lt_mul_of_pos_right hv₀' <| (sub_lt_sub_iff_left (u : ℝ)).mpr <|
          flip mul_lt_mul_of_pos_right hv₀ <| sub_right_lt_of_lt_add <| lt_floor_add_one ξ
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₀' : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h :
  ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
    (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + 1
this :
  ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
    ((↑u : ℝ) - (ξ - 1) * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
have this₁ : ((↑u : ℝ) - HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) <
  ((↑u : ℝ) - ξ * (↑v : ℝ)) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1) + (↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1)
Tactic: rw [sub_mul ξ, one_mul, ← sub_add, add_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have hu₁ : 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
-- 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
⊢ IsCoprime (u - ⌊ξ⌋ * v) v
have rwa : IsCoprime (u + -(⌊ξ⌋ * v)) v
Tactic: rwa [sub_eq_add_neg, ← neg_mul, IsCoprime.add_mul_right_left_iff]
-- 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
rwa : IsCoprime (u + -(⌊ξ⌋ * v)) v
⊢ IsCoprime (u - ⌊ξ⌋ * v) v
have rwa₁ : IsCoprime (u + -⌊ξ⌋ * v) v
Tactic: rwa [sub_eq_add_neg, ← neg_mul, IsCoprime.add_mul_right_left_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have huv_cop : 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]
-- 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
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have refine_1 : ∀ (hf : u - ⌊ξ⌋ * v = 0), False
Tactic: refine ⟨lt_of_le_of_ne' hu₀ fun hf => ?_, lt_of_le_of_ne hu₁ fun hf => ?_⟩
-- 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
huv_cop : IsCoprime (u - ⌊ξ⌋ * v) v
refine_1 : ∀ (hf : u - ⌊ξ⌋ * v = 0), False
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have refine_2 : ∀ (hf : u - ⌊ξ⌋ * v = v), False
Tactic: refine ⟨lt_of_le_of_ne' hu₀ fun hf => ?_, lt_of_le_of_ne hu₁ fun hf => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
⊢ False
have huv_cop₁ : IsCoprime 0 v
Tactic: rw [hf] at huv_cop
Cleared hypotheses: huv_cop, hf
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
⊢ False
have huv_cop₁ : v = 1 ∨ v = -1
Tactic: simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop
Cleared hypotheses: 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 = 0
huv_cop : v = 1 ∨ v = -1
⊢ False
have refine_1 : ∀ (huv_cop : v = 1), False
Tactic: rcases huv_cop with huv_cop | huv_cop
Cleared hypotheses: 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 = 0
huv_cop : v = 1 ∨ v = -1
refine_1 : ∀ (huv_cop : v = 1), False
⊢ False
have refine_1₁ : ∀ (huv_cop : v = -1), False
Tactic: rcases huv_cop with huv_cop | huv_cop
Cleared hypotheses: 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 = 0
huv_cop : v = 1
⊢ False
have linarith : -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 = 0
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 = 0
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
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
⊢ False
have huv_cop₁ : IsCoprime v v
Tactic: rw [hf] at huv_cop
Cleared hypotheses: huv_cop, hf
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
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
⊢ False
have huv_cop₁ : v = 1 ∨ v = -1
Tactic: simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop
Cleared hypotheses: 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 ∨ v = -1
⊢ False
have refine_2 : ∀ (huv_cop : v = 1), False
Tactic: rcases huv_cop with huv_cop | huv_cop
Cleared hypotheses: 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 ∨ v = -1
refine_2 : ∀ (huv_cop : v = 1), False
⊢ False
have refine_2₁ : ∀ (huv_cop : v = -1), False
Tactic: rcases huv_cop with huv_cop | huv_cop
Cleared hypotheses: 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
⊢ False
have linarith : -1 + (2 - v) + (v - 1) = 0
Tactic: linarith only [hv, huv_cop]