awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
⊢ a = b
have rw : HDiv.hDiv (α := ℚ) (↑a.num : ℚ) (↑a.den : ℚ) = b
Tactic: rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
rw : HDiv.hDiv (α := ℚ) (↑a.num : ℚ) (↑a.den : ℚ) = b
⊢ a = b
have rw₁ : HDiv.hDiv (α := ℚ) (↑a.num : ℚ) (↑a.den : ℚ) = HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ)
Tactic: rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
rw : HDiv.hDiv (α := ℚ) (↑a.num : ℚ) (↑a.den : ℚ) = b
rw₁ : HDiv.hDiv (α := ℚ) (↑a.num : ℚ) (↑a.den : ℚ) = HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ)
⊢ a = b
have rw₂ : HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑a.den : ℚ) = HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ)
Tactic: rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
rw : HDiv.hDiv (α := ℚ) (↑a.num : ℚ) (↑a.den : ℚ) = b
rw₁ : HDiv.hDiv (α := ℚ) (↑a.num : ℚ) (↑a.den : ℚ) = HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ)
rw₂ : HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑a.den : ℚ) = HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ)
⊢ a = b
have rw₃ : HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ) = HDiv.hDiv (α := ℚ) (↑b.num : ℚ) (↑b.den : ℚ)
Tactic: rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
⊢ s.Finite
have hinj : Function.Injective f
Tactic: have hinj : Function.Injective f := by
    intro a b hab
    simp only [f, Prod.mk_inj] at hab
    rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : xy ∈ f '' s
⊢ Membership.mem (γ := Set (ℤ × ℕ))
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}) xy
have hxy₁ : ∃ x ∈ s, f x = xy
Tactic: simp only [mem_image] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
hxy : ∃ x ∈ s, f x = xy
⊢ Membership.mem (γ := Set (ℤ × ℕ))
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}) xy
have obtain : ∀ (q : ℚ) (hq₁ : q ∈ s) (hq₂ : f q = xy),
  Membership.mem (γ := Set (ℤ × ℕ))
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}) xy
Tactic: obtain ⟨q, hq₁, hq₂⟩ := hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
⊢ Membership.mem (γ := Set (ℤ × ℕ))
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}) xy
have hd : q.den ≤ ξ.den
Tactic: obtain ⟨hd, hn⟩ := den_le_and_le_num_le_of_sub_lt_one_div_den_sq hq₁
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
⊢ Membership.mem (γ := Set (ℤ × ℕ))
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}) xy
have hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
Tactic: obtain ⟨hd, hn⟩ := den_le_and_le_num_le_of_sub_lt_one_div_den_sq hq₁
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
⊢ Membership.mem (γ := Set (ℤ × ℕ))
    (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}) xy
have simp_rw : ∃ (i : ℕ) (_ : i ∈ Ioc 0 ξ.den), xy ∈ SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑i : ℚ)⌉ - 1) (⌊ξ * (↑i : ℚ)⌋ + 1)) {i}
Tactic: simp_rw [mem_iUnion]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
⊢ ∃ (i : ℕ) (_ : i ∈ Ioc 0 ξ.den), xy ∈ SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑i : ℚ)⌉ - 1) (⌊ξ * (↑i : ℚ)⌋ + 1)) {i}
have refine : xy ∈ SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑q.den : ℚ)⌉ - 1) (⌊ξ * (↑q.den : ℚ)⌋ + 1)) {q.den}
Tactic: refine ⟨q.den, Set.mem_Ioc.mpr ⟨q.pos, hd⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
xy : ℤ × ℕ
q : ℚ
hq₁ : q ∈ s
hq₂ : f q = xy
hd : q.den ≤ ξ.den
hn : ⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1
⊢ xy ∈ SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑q.den : ℚ)⌉ - 1) (⌊ξ * (↑q.den : ℚ)⌋ + 1)) {q.den}
have simp : ∃ (x : ℤ), (⌈ξ * (↑q.den : ℚ)⌉ - 1 ≤ x ∧ x ≤ ⌊ξ * (↑q.den : ℚ)⌋ + 1) ∧ (x, q.den) = xy
Tactic: simp only [prod_singleton, mem_image, mem_Icc]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
⊢ s.Finite
have H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}
Tactic: have H : f '' s ⊆ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * y⌉ - 1) (⌊ξ * y⌋ + 1) ×ˢ {y} := by
    intro xy hxy
    simp only [mem_image] at hxy
    obtain ⟨q, hq₁, hq₂⟩ := hxy
    obtain ⟨hd, hn⟩ := den_le_and_le_num_le_of_sub_lt_one_div_den_sq hq₁
    simp_rw [mem_iUnion]
    refine ⟨q.den, Set.mem_Ioc.mpr ⟨q.pos, hd⟩, ?_⟩
    simp only [prod_singleton, mem_image, mem_Icc]
    exact ⟨q.num, hn, hq₂⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun (q : ℚ) ↦ (q.num, q.den)
s : Set ℚ := {q : ℚ | |ξ - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2}
hinj : Function.Injective f
H : f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y}
⊢ s.Finite
have refine : Set.Finite (α := ℤ × ℕ)
  (⋃ y ∈ Ioc 0 ξ.den, SProd.sprod (β := Set ℕ) (Icc (⌈ξ * (↑y : ℚ)⌉ - 1) (⌊ξ * (↑y : ℚ)⌋ + 1)) {y})
Tactic: refine (Finite.subset ?_ H).of_finite_image hinj.injOn
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
⊢ Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} ↔ Irrational ξ
have h : ∀ (h : Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}) (a b : ℤ),
  b ≠ 0 → ξ ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
Tactic: refine
    ⟨fun h => (irrational_iff_ne_rational ξ).mpr fun a b _ => ?_,
      Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational⟩
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
h : Set.Infinite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
a b : ℤ
h_1 : b ≠ 0
⊢ ξ ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
have contrapose! : ∀ (h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
  Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ Set.Finite (α := ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2}
have h₁ : ∀ (q : ℚ),
  |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 ↔
    |HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
Tactic: convert! Rat.finite_rat_abs_sub_lt_one_div_den_sq ((a : ℚ) / b) with q
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
q : ℚ
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 = (↑(1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2) : ℝ)
have push_cast : 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 = 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
q : ℚ
⊢ |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 ↔
    |HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
have h₁ : |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - (↑q : ℝ)| < (↑(1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2) : ℝ) ↔
  |HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
Tactic: rw [h, (by (push_cast; rfl) : (1 : ℝ) / (q.den : ℝ) ^ 2 = (1 / (q.den : ℚ) ^ 2 : ℚ))]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
a b : ℤ
h_1 : b ≠ 0
h : ξ = HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
q : ℚ
⊢ |HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) - (↑q : ℝ)| < (↑(1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2) : ℝ) ↔
    |HDiv.hDiv (α := ℚ) (↑a : ℚ) (↑b : ℚ) - q| < 1 / HPow.hPow (α := ℚ) (β := ℕ) (↑q.den : ℚ) 2
have h₁ : |Rat.divInt a b - q| < HDiv.hDiv (α := ℚ) 1 (↑(HPow.hPow (β := ℕ) q.den 2) : ℚ) ↔
  |Rat.divInt a b - q| < HDiv.hDiv (α := ℚ) 1 (↑(HPow.hPow (β := ℕ) q.den 2) : ℚ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
n : ℕ
⊢ convergent 0 n = 0
have zero : convergent 0 0 = 0
Tactic: induction n with
  | zero => simp only [convergent_zero, floor_zero, cast_zero]
  | succ n ih =>
    simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
n : ℕ
zero : convergent 0 0 = 0
⊢ convergent 0 n = 0
have succ : ∀ (n : ℕ) (ih : convergent 0 n = 0), convergent 0 (n + 1) = 0
Tactic: induction n with
  | zero => simp only [convergent_zero, floor_zero, cast_zero]
  | succ n ih =>
    simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℤ
n : ℕ
⊢ convergent (↑ξ : ℝ) n = (↑ξ : ℚ)
have zero : convergent (↑ξ : ℝ) 0 = (↑ξ : ℚ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℤ
n : ℕ
zero : convergent (↑ξ : ℝ) 0 = (↑ξ : ℚ)
⊢ convergent (↑ξ : ℝ) n = (↑ξ : ℚ)
have succ : ∀ (n : ℕ), convergent (↑ξ : ℝ) (n + 1) = (↑ξ : ℚ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
v : ℤ
hv : 0 < v
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
have norm_cast : 0 < 2 * v - 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ 0 < fract ξ
have hv₀ : LT.lt (α := ℝ) 0 (↑v : ℝ)
Tactic: have hv₀ : (0 : ℝ) < v := cast_pos.mpr (zero_lt_two.trans_le hv)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
⊢ 0 < fract ξ
have hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
Tactic: obtain ⟨hv₁, hv₂⟩ := aux₀ (zero_lt_two.trans_le hv)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
⊢ 0 < fract ξ
have hcop : IsCoprime u v
Tactic: obtain ⟨hcop, _, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
⊢ 0 < fract ξ
have left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
Tactic: obtain ⟨hcop, _, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
⊢ 0 < fract ξ
have h₁ : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: obtain ⟨hcop, _, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
⊢ 0 < fract ξ
have refine : ∀ (hf : ξ = (↑⌊ξ⌋ : ℝ)), False
Tactic: refine fract_pos.mpr fun hf => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
⊢ False
have h₁ : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: rw [hf] at h
Cleared hypotheses: h, hf
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
⊢ HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1 < 1
have refine : (↑v : ℝ)⁻¹ ≤ |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)|
Tactic: refine (mul_lt_iff_lt_one_right hv₀).1 ((inv_lt_inv₀ hv₀ (mul_pos hv₁ hv₂)).1 (h.trans_le' ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
⊢ (↑v : ℝ)⁻¹ ≤ |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)|
have h' : (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)) / (↑v : ℝ)
Tactic: have h' : (⌊ξ⌋ : ℝ) - u / v = (⌊ξ⌋ * v - u) / v := by field
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
h' : (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)) / (↑v : ℝ)
⊢ (↑v : ℝ)⁻¹ ≤ |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)|
have rw : 1 ≤ |HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)|
Tactic: rw [h', abs_div, abs_of_pos hv₀, ← one_div, div_le_div_iff_of_pos_right hv₀]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
h' : (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)) / (↑v : ℝ)
⊢ 1 ≤ |HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)|
have norm_cast : 1 ≤ |⌊ξ⌋ * v - u|
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
h' : (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ) = (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑u : ℝ)) / (↑v : ℝ)
⊢ 1 ≤ |⌊ξ⌋ * v - u|
have rw : ⌊ξ⌋ * v ≠ u
Tactic: rw [← zero_add (1 : ℤ), add_one_le_iff, abs_pos, sub_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hf : ξ = (↑⌊ξ⌋ : ℝ)
hcop : IsCoprime (⌊ξ⌋ * v) v
left : v = 1 → -(1 / 2) < ξ - (↑(⌊ξ⌋ * v) : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' :
  (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ) =
    (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑(⌊ξ⌋ * v) : ℝ)) / (↑v : ℝ)
⊢ False
have inl : v = 1 → False
Tactic: cases isUnit_iff.mp (isCoprime_self.mp (IsCoprime.mul_left_iff.mp hcop).2)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hf : ξ = (↑⌊ξ⌋ : ℝ)
hcop : IsCoprime (⌊ξ⌋ * v) v
left : v = 1 → -(1 / 2) < ξ - (↑(⌊ξ⌋ * v) : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
h' :
  (↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑(⌊ξ⌋ * v) : ℝ) (↑v : ℝ) =
    (HMul.hMul (α := ℝ) (↑⌊ξ⌋ : ℝ) (↑v : ℝ) - (↑(⌊ξ⌋ * v) : ℝ)) / (↑v : ℝ)
inl : v = 1 → False
⊢ False
have inr : v = -1 → False
Tactic: cases isUnit_iff.mp (isCoprime_self.mp (IsCoprime.mul_left_iff.mp hcop).2)
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
⊢ False
have H : HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1 < 1
Tactic: have H : (2 * v - 1 : ℝ) < 1 := by
    refine (mul_lt_iff_lt_one_right hv₀).1 ((inv_lt_inv₀ hv₀ (mul_pos hv₁ hv₂)).1 (h.trans_le' ?_))
    have h' : (⌊ξ⌋ : ℝ) - u / v = (⌊ξ⌋ * v - u) / v := by field
    rw [h', abs_div, abs_of_pos hv₀, ← one_div, div_le_div_iff_of_pos_right hv₀]
    norm_cast
    rw [← zero_add (1 : ℤ), add_one_le_iff, abs_pos, sub_ne_zero]
    rintro rfl
    cases isUnit_iff.mp (isCoprime_self.mp (IsCoprime.mul_left_iff.mp hcop).2) <;> lia
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
H : HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1 < 1
⊢ False
have H₁ : 2 * v - 1 < 1
Tactic: norm_cast at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
H : 2 * v - 1 < 1
⊢ False
have linarith : HMul.hMul (α := ℤ) 3 (-1) + 2 * (2 - v) + (2 * v - 1 + 1 - 1) = 0
Tactic: linarith only [hv, H]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
H : 2 * v - 1 < 1
linarith : HMul.hMul (α := ℤ) 3 (-1) + 2 * (2 - v) + (2 * v - 1 + 1 - 1) = 0
⊢ False
have linarith₁ : GT.gt (α := ℤ) 3 0
Tactic: linarith only [hv, H]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (goal)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : LT.lt (α := ℝ) 0 (↑v : ℝ)
hv₂ : 0 < HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
h : |(↑⌊ξ⌋ : ℝ) - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
hf : ξ = (↑⌊ξ⌋ : ℝ)
H : 2 * v - 1 < 1
linarith : HMul.hMul (α := ℤ) 3 (-1) + 2 * (2 - v) + (2 * v - 1 + 1 - 1) = 0
linarith₁ : GT.gt (α := ℤ) 3 0
⊢ False
have linarith₂ : GT.gt (α := ℤ) 2 0
Tactic: linarith only [hv, H]
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have hcop : IsCoprime u v
Tactic: obtain ⟨hcop, _, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hcop : IsCoprime u v
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
Tactic: obtain ⟨hcop, _, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.DiophantineApproximation.Basic (hypothesis)
Goal:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
hcop : IsCoprime u v
left : v = 1 → -(1 / 2) < ξ - (↑u : ℝ)
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
have h₁ : |ξ - HDiv.hDiv (α := ℝ) (↑u : ℝ) (↑v : ℝ)| < ((↑v : ℝ) * (HMul.hMul (α := ℝ) 2 (↑v : ℝ) - 1))⁻¹
Tactic: obtain ⟨hcop, _, h⟩ := h
Cleared hypotheses: h