awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = 0}
q : ℚ
hq : HPow.hPow (β := ℕ) q.num 2 = HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 * d
⊢ False
have obtain : ∀ (a : ℤ) (ha : q.num = (↑q.den : ℤ) * a), False
Tactic: obtain ⟨a, ha⟩ := (Int.pow_dvd_pow_iff two_ne_zero).mp ⟨d, hq⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (hypothesis)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = 0}
q : ℚ
hq : HPow.hPow (β := ℕ) q.num 2 = HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 * d
a : ℤ
ha : q.num = (↑q.den : ℤ) * a
⊢ False
have hq₁ : HPow.hPow (β := ℕ) a 2 = d
Tactic: rw [ha, mul_pow, mul_right_inj' (pow_pos (Int.natCast_pos.mpr q.pos) 2).ne'] at hq
Cleared hypotheses: hq, ha
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (hypothesis)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have hm₀ : m ≠ 0
Tactic: have hm₀ : m ≠ 0 := by
    rintro rfl
    obtain ⟨q, hq⟩ := hm.nonempty
    rw [mem_setOf, sub_eq_zero, mul_comm] at hq
    obtain ⟨a, ha⟩ := (Int.pow_dvd_pow_iff two_ne_zero).mp ⟨d, hq⟩
    rw [ha, mul_pow, mul_right_inj' (pow_pos (Int.natCast_pos.mpr q.pos) 2).ne'] at hq
    exact hd ⟨a, sq a ▸ hq.symm⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (hypothesis)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have this : NeZero m.natAbs
Tactic: haveI := neZero_iff.mpr (Int.natAbs_ne_zero.mpr hm₀)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have obtain : ∀ (q₁ : ℚ) (h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m) (q₂ : ℚ)
  (h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m) (hne : q₁ ≠ q₂)
  (hqf : f q₁ = f q₂), ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
Tactic: obtain ⟨q₁, h₁ : q₁.num ^ 2 - d * (q₁.den : ℤ) ^ 2 = m,
      q₂, h₂ : q₂.num ^ 2 - d * (q₂.den : ℤ) ^ 2 = m, hne, hqf⟩ :=
    hm.exists_ne_map_eq_of_mapsTo (mapsTo_univ f _) finite_univ
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (hypothesis)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
Tactic: obtain ⟨hq1 : (q₁.num : ZMod m.natAbs) = q₂.num, hq2 : (q₁.den : ZMod m.natAbs) = q₂.den⟩ :=
    Prod.ext_iff.mp hqf
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (hypothesis)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
Tactic: obtain ⟨hq1 : (q₁.num : ZMod m.natAbs) = q₂.num, hq2 : (q₁.den : ZMod m.natAbs) = q₂.den⟩ :=
    Prod.ext_iff.mp hqf
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
⊢ m ∣ q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)
have rw : Eq (α := ZMod m.natAbs) (↑(q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)) : ZMod m.natAbs) 0
Tactic: rw [← Int.natAbs_dvd, ← ZMod.intCast_zmod_eq_zero_iff_dvd]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
⊢ Eq (α := ZMod m.natAbs) (↑(q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)) : ZMod m.natAbs) 0
have push_cast : HMul.hMul (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) -
    (↑d : ZMod m.natAbs) * HMul.hMul (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs) =
  0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
⊢ HMul.hMul (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) -
      (↑d : ZMod m.natAbs) * HMul.hMul (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs) =
    0
have rw : HPow.hPow (α := ZMod m.natAbs) (β := ℕ) (↑q₂.num : ZMod m.natAbs) 2 -
    (↑d : ZMod m.natAbs) * HPow.hPow (α := ZMod m.natAbs) (β := ℕ) (↑q₂.den : ZMod m.natAbs) 2 =
  0
Tactic: rw [hq1, hq2, ← sq, ← sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
⊢ HPow.hPow (α := ZMod m.natAbs) (β := ℕ) (↑q₂.num : ZMod m.natAbs) 2 -
      (↑d : ZMod m.natAbs) * HPow.hPow (α := ZMod m.natAbs) (β := ℕ) (↑q₂.den : ZMod m.natAbs) 2 =
    0
have norm_cast : Eq (α := ZMod m.natAbs) (↑(HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)) : ZMod m.natAbs) 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
⊢ Eq (α := ZMod m.natAbs) (↑(HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)) : ZMod m.natAbs) 0
have rw : (↑m.natAbs : ℤ) ∣ HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)
Tactic: rw [ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natAbs_dvd, Nat.cast_pow, ← h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
rw : (↑m.natAbs : ℤ) ∣ HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)
⊢ Eq (α := ZMod m.natAbs) (↑(HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)) : ZMod m.natAbs) 0
have rw₁ : m ∣ HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)
Tactic: rw [ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natAbs_dvd, Nat.cast_pow, ← h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
rw : (↑m.natAbs : ℤ) ∣ HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)
rw₁ : m ∣ HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)
⊢ Eq (α := ZMod m.natAbs) (↑(HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)) : ZMod m.natAbs) 0
have rw₂ : m ∣ HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2
Tactic: rw [ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natAbs_dvd, Nat.cast_pow, ← h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
rw : (↑m.natAbs : ℤ) ∣ HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)
rw₁ : m ∣ HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)
rw₂ : m ∣ HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2
⊢ Eq (α := ZMod m.natAbs) (↑(HPow.hPow (β := ℕ) q₂.num 2 - d * (↑(HPow.hPow (β := ℕ) q₂.den 2) : ℤ)) : ZMod m.natAbs) 0
have rw₃ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 ∣
  HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2
Tactic: rw [ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natAbs_dvd, Nat.cast_pow, ← h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (hypothesis)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have hd₁ : m ∣ q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)
Tactic: have hd₁ : m ∣ q₁.num * q₂.num - d * (q₁.den * q₂.den) := by
    rw [← Int.natAbs_dvd, ← ZMod.intCast_zmod_eq_zero_iff_dvd]
    push_cast
    rw [hq1, hq2, ← sq, ← sq]
    norm_cast
    rw [ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natAbs_dvd, Nat.cast_pow, ← h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
hd₁ : m ∣ q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)
⊢ m ∣ q₁.num * (↑q₂.den : ℤ) - q₂.num * (↑q₁.den : ℤ)
have rw : Eq (α := ZMod m.natAbs) (↑(q₂.num * (↑q₁.den : ℤ)) : ZMod m.natAbs) (↑(q₁.num * (↑q₂.den : ℤ)) : ZMod m.natAbs)
Tactic: rw [← Int.natAbs_dvd, ← ZMod.intCast_eq_intCast_iff_dvd_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
hd₁ : m ∣ q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)
⊢ Eq (α := ZMod m.natAbs) (↑(q₂.num * (↑q₁.den : ℤ)) : ZMod m.natAbs) (↑(q₁.num * (↑q₂.den : ℤ)) : ZMod m.natAbs)
have push_cast : HMul.hMul (α := ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) =
  HMul.hMul (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
hd₁ : m ∣ q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)
⊢ HMul.hMul (α := ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) =
    HMul.hMul (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
have rw : HMul.hMul (α := ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) =
  HMul.hMul (α := ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
Tactic: rw [hq1, hq2]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM : Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
m : ℤ
hm : Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
hm₀ : m ≠ 0
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun (q : ℚ) ↦ ((↑q.num : ZMod m.natAbs), (↑q.den : ZMod m.natAbs))
q₁ : ℚ
h₁ : HPow.hPow (β := ℕ) q₁.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₁.den : ℤ) 2 = m
q₂ : ℚ
h₂ : HPow.hPow (β := ℕ) q₂.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q₂.den : ℤ) 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : Eq (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs)
hq2 : Eq (α := ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
hd₁ : m ∣ q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)
rw :
  HMul.hMul (α := ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) =
    HMul.hMul (α := ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
⊢ HMul.hMul (α := ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) (↑q₁.den : ZMod m.natAbs) =
    HMul.hMul (α := ZMod m.natAbs) (↑q₁.num : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
have rw₁ : HMul.hMul (α := ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs) =
  HMul.hMul (α := ZMod m.natAbs) (↑q₂.num : ZMod m.natAbs) (↑q₂.den : ZMod m.natAbs)
Tactic: rw [hq1, hq2]