awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
v : ℕ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have h₁ : ∀ (v : ℕ)
  (ih :
    ∀ m < v,
      ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
        ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n)
  {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑v : ℤ)),
  ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
Tactic: induction v using Nat.strong_induction_on generalizing ξ u with | h v ih => ?_
Cleared hypotheses: ξ, u, v, h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have h₁ : ∀ (ht : v < 1), ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
Tactic: rcases lt_trichotomy v 1 with (ht | rfl | ht)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
h₁ : ∀ (ht : v < 1), ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have h₂ : ∀
  (ih :
    ∀ m < 1,
      ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
        ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n)
  (h : ContfracLegendre.Ass ξ u (↑1 : ℤ)), ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑1 : ℚ) = ξ.convergent n
Tactic: rcases lt_trichotomy v 1 with (ht | rfl | ht)
Cleared hypotheses: v, ih, h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
h₁ : ∀ (ht : v < 1), ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
h₂ :
  ∀
    (ih :
      ∀ m < 1,
        ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
          ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n)
    (h : ContfracLegendre.Ass ξ u (↑1 : ℤ)), ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑1 : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have h₃ : ∀ (ht : 1 < v), ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
Tactic: rcases lt_trichotomy v 1 with (ht | rfl | ht)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : v < 1
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
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 (hypothesis)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
ht : v < 1
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑v : ℤ) : ℝ)| < ((↑(↑v : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑v : ℤ) : ℝ) - 1))⁻¹
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have h₁ : |ξ| < 0
Tactic: simp only [Nat.lt_one_iff.mp ht, Nat.cast_zero, div_zero, tsub_zero, zero_mul,
      cast_zero, inv_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
h : ContfracLegendre.Ass ξ u (↑1 : ℤ)
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑1 : ℚ) = ξ.convergent n
have h₁ : ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
Tactic: rw [Nat.cast_one, div_one]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
h : ContfracLegendre.Ass ξ u (↑1 : ℤ)
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have left : IsCoprime u (↑1 : ℤ)
Tactic: obtain ⟨_, h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
h : ContfracLegendre.Ass ξ u (↑1 : ℤ)
left : IsCoprime u (↑1 : ℤ)
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
Tactic: obtain ⟨_, h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
h : ContfracLegendre.Ass ξ u (↑1 : ℤ)
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h₂ : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
Tactic: obtain ⟨_, h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h : ∀ (ht : (↑u : ℝ) ≤ ξ), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
Tactic: rcases le_or_gt (u : ℝ) ξ with ht | ht
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
h : ∀ (ht : (↑u : ℝ) ≤ ξ), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h₃ : ∀ (ht : ξ < (↑u : ℝ)), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
Tactic: rcases le_or_gt (u : ℝ) ξ with ht | ht
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h : (↑u : ℚ) = ξ.convergent 0
Tactic: use 0
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
⊢ (↑u : ℚ) = ξ.convergent 0
have h : (↑u : ℝ) ≤ ξ ∧ ξ < HAdd.hAdd (α := ℝ) (↑u : ℝ) 1
Tactic: rw [convergent_zero, Rat.coe_int_inj, eq_comm, floor_eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
⊢ (↑u : ℝ) ≤ ξ ∧ ξ < HAdd.hAdd (α := ℝ) (↑u : ℝ) 1
have h : (↑u : ℝ) = HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)
Tactic: convert! And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : (↑u : ℝ) ≤ ξ
h : (↑u : ℝ) = HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)
⊢ (↑u : ℝ) ≤ ξ ∧ ξ < HAdd.hAdd (α := ℝ) (↑u : ℝ) 1
have h₃ : 1 = ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
Tactic: convert! And.intro ht (sub_lt_iff_lt_add'.mp (abs_lt.mp h₂).2)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₁ : Eq (α := ℤ) (↑1 : ℤ) 1 → -(1 / 2) < ξ - (↑u : ℝ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h₃ : (↑u : ℝ) + -(1 / 2) < ξ
Tactic: replace h₁ := lt_sub_iff_add_lt'.mp (h₁ rfl)
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
⊢ ⌊ξ⌋ = u - 1
have rw : HSub.hSub (α := ℝ) (↑u : ℝ) 1 ≤ ξ ∧ ξ < (↑u : ℝ)
Tactic: rw [floor_eq_iff, cast_sub, cast_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have hξ₁ : ⌊ξ⌋ = u - 1
Tactic: have hξ₁ : ⌊ξ⌋ = u - 1 := by
        rw [floor_eq_iff, cast_sub, cast_one, sub_add_cancel]
        exact ⟨(((sub_lt_sub_iff_left _).mpr one_half_lt_one).trans h₁).le, ht⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h : ∀ (Hξ : ξ = (↑⌊ξ⌋ : ℝ)), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
Tactic: rcases eq_or_ne ξ ⌊ξ⌋ with Hξ | Hξ
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
h : ∀ (Hξ : ξ = (↑⌊ξ⌋ : ℝ)), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h₃ : ∀ (Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)), ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
Tactic: rcases eq_or_ne ξ ⌊ξ⌋ with Hξ | Hξ
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ = (↑⌊ξ⌋ : ℝ)
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h₃ : 1 < 1 / 2
Tactic: rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁
Cleared hypotheses: h₁, hξ₁, Hξ
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
⊢ ⌊(fract ξ)⁻¹⌋ = 1
have rw : fract ξ ≤ 1 ∧ 2⁻¹ < fract ξ
Tactic: rw [floor_eq_iff, cast_one, le_inv_comm₀ zero_lt_one (fract_pos.mpr Hξ), inv_one,
            one_add_one_eq_two, inv_lt_comm₀ (fract_pos.mpr Hξ) zero_lt_two]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
⊢ fract ξ ≤ 1 ∧ 2⁻¹ < fract ξ
have refine : 2⁻¹ < fract ξ
Tactic: refine ⟨(fract_lt_one ξ).le, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
⊢ 2⁻¹ < fract ξ
have rw : (↑u : ℝ) - HSub.hSub (α := ℝ) 1 2⁻¹ < ξ
Tactic: rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
⊢ (↑u : ℝ) - HSub.hSub (α := ℝ) 1 2⁻¹ < ξ
have h : (↑u : ℝ) - HSub.hSub (α := ℝ) 1 2⁻¹ = (↑u : ℝ) + -(1 / 2)
Tactic: convert! h₁ using 1
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1
Tactic: have hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1 := by
          rw [floor_eq_iff, cast_one, le_inv_comm₀ zero_lt_one (fract_pos.mpr Hξ), inv_one,
            one_add_one_eq_two, inv_lt_comm₀ (fract_pos.mpr Hξ) zero_lt_two]
          refine ⟨(fract_lt_one ξ).le, ?_⟩
          rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]
          convert! h₁ using 1
          rw [sub_eq_add_neg]
          norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u : ℤ
ih :
  ∀ m < 1,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
left : IsCoprime u (↑1 : ℤ)
h₂ :
  |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑(↑1 : ℤ) : ℝ)| < ((↑(↑1 : ℤ) : ℝ) * (HMul.hMul (α := ℝ) 2 (↑(↑1 : ℤ) : ℝ) - 1))⁻¹
ht : ξ < (↑u : ℝ)
h₁ : (↑u : ℝ) + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ (↑⌊ξ⌋ : ℝ)
hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1
⊢ ∃ (n : ℕ), (↑u : ℚ) = ξ.convergent n
have h : (↑u : ℚ) = ξ.convergent 1
Tactic: use 1
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
Tactic: obtain ⟨huv₀, huv₁⟩ := aux₂ (Nat.cast_le.mpr ht) h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Tactic: obtain ⟨huv₀, huv₁⟩ := aux₂ (Nat.cast_le.mpr ht) h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have Hv : Ne (α := ℚ) (↑v : ℚ) 0
Tactic: have Hv : (v : ℚ) ≠ 0 := (Nat.cast_pos.mpr (zero_lt_one.trans ht)).ne'
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
⊢ (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
have zify : LT.lt (α := ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ) (↑v : ℤ)
Tactic: zify
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have huv₁' : (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
Tactic: have huv₁' : (u - ⌊ξ⌋ * v).toNat < v := by zify; rwa [toNat_of_nonneg huv₀.le]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
huv₁' : (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have inv : ContfracLegendre.Ass (fract ξ)⁻¹ (↑v : ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ)
Tactic: have inv : ContfracLegendre.Ass (fract ξ)⁻¹ v (u - ⌊ξ⌋ * ↑v).toNat :=
      (toNat_of_nonneg huv₀.le).symm ▸ invariant (Nat.cast_le.mpr ht) h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
huv₁' : (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ (↑v : ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ)
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have h₁ : ∀ (n : ℕ) (hn : HDiv.hDiv (α := ℚ) (↑(↑v : ℤ) : ℚ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℚ) = (fract ξ)⁻¹.convergent n),
  ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
Tactic: obtain ⟨n, hn⟩ := ih (u - ⌊ξ⌋ * v).toNat huv₁' inv
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
huv₁' : (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ (↑v : ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ)
n : ℕ
hn : HDiv.hDiv (α := ℚ) (↑(↑v : ℤ) : ℚ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℚ) = (fract ξ)⁻¹.convergent n
⊢ ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent n
have h₁ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
Tactic: use n + 1
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
v : ℕ
ih :
  ∀ m < v,
    ∀ {ξ : ℝ} {u : ℤ} (h : ContfracLegendre.Ass ξ u (↑m : ℤ)),
      ∃ (n : ℕ), HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑m : ℚ) = ξ.convergent n
ξ : ℝ
u : ℤ
h : ContfracLegendre.Ass ξ u (↑v : ℤ)
ht : 1 < v
huv₀ : 0 < u - ⌊ξ⌋ * (↑v : ℤ)
huv₁ : u - ⌊ξ⌋ * (↑v : ℤ) < (↑v : ℤ)
Hv : Ne (α := ℚ) (↑v : ℚ) 0
huv₁' : (u - ⌊ξ⌋ * (↑v : ℤ)).toNat < v
inv : ContfracLegendre.Ass (fract ξ)⁻¹ (↑v : ℤ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℤ)
n : ℕ
hn : HDiv.hDiv (α := ℚ) (↑(↑v : ℤ) : ℚ) (↑(u - ⌊ξ⌋ * (↑v : ℤ)).toNat : ℚ) = (fract ξ)⁻¹.convergent n
⊢ HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = ξ.convergent (n + 1)
have h₁ : HDiv.hDiv (α := ℚ) (↑u : ℚ) (↑v : ℚ) = (↑⌊ξ⌋ : ℚ) + ((fract ξ)⁻¹.convergent n)⁻¹
Tactic: rw [convergent_succ, ← hn,
      (mod_cast toNat_of_nonneg huv₀.le : ((u - ⌊ξ⌋ * v).toNat : ℚ) = u - ⌊ξ⌋ * v),
      cast_natCast, inv_div, sub_div, mul_div_cancel_right₀ _ Hv, add_sub_cancel]