awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
rw : |√(↑d : ℝ) + (↑q : ℝ)| * |√(↑d : ℝ) - (↑q : ℝ)| < (↑M : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)
⊢ |(↑d : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 - HPow.hPow (α := ℝ) (β := ℕ) (↑q.num : ℝ) 2| /
      |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2| <
    (↑M : ℝ) / |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2|

Tactic:
rw [← abs_div, abs_sq, sub_div, mul_div_cancel_right₀ _ h0.ne', ← div_pow, h1, ←
      sq_sqrt (Int.cast_pos.mpr h₀).le, sq_sub_sq, abs_mul, ← mul_one_div]

Premises used: Iff.mpr, abs_mul, abs_div, abs_sq, LT.lt.le, Real.sq_sqrt, sub_div, LT.lt.ne', mul_div_cancel_right₀, mul_one_div, div_pow, Int.cast_pos, sq_sub_sq
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
⊢ |√(↑d : ℝ) + (↑q : ℝ)| * |√(↑d : ℝ) - (↑q : ℝ)| < (↑M : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)

Tactic:
mul_lt_mul'' (((abs_add_le ξ q).trans ?_).trans_lt hM₁) h (abs_nonneg _) (abs_nonneg _)

Premises used: Rat.cast, mul_lt_mul'', LE.le.trans, abs_add_le, LE.le.trans_lt, abs_nonneg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
refine : |ξ| + |(↑q : ℝ)| ≤ 2 * |ξ| + 1
⊢ |√(↑d : ℝ) + (↑q : ℝ)| * |√(↑d : ℝ) - (↑q : ℝ)| < (↑M : ℝ) * (1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2)

Tactic:
refine mul_lt_mul'' (((abs_add_le ξ q).trans ?_).trans_lt hM₁) h (abs_nonneg _) (abs_nonneg _)

Premises used: Rat.cast, mul_lt_mul'', LE.le.trans, abs_add_le, LE.le.trans_lt, abs_nonneg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
rw : |(↑q : ℝ)| - |ξ| ≤ 1
⊢ |ξ| + |(↑q : ℝ)| ≤ 2 * |ξ| + 1

Tactic:
rw [two_mul, add_assoc, add_le_add_iff_left, ← sub_le_iff_le_add']

Premises used: add_assoc, add_le_add_iff_left, two_mul, sub_le_iff_le_add'
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
⊢ |(↑q : ℝ) - ξ| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2

Tactic:
rw [mem_setOf, abs_sub_comm] at h

Premises used: Set.mem_setOf, abs_sub_comm
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
h₁ : |(↑q : ℝ) - ξ| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
⊢ 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2

Tactic:
rw [mem_setOf, abs_sub_comm] at h

Premises used: Set.mem_setOf, abs_sub_comm
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
h₁ : |(↑q : ℝ) - ξ| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h0₁ : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
⊢ HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)

Tactic:
rw [mem_setOf, abs_sub_comm] at h

Premises used: Set.mem_setOf, abs_sub_comm
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : |(↑q : ℝ) - ξ| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
⊢ |(↑q : ℝ)| - |ξ| ≤ 1

Tactic:
(abs_sub_abs_le_abs_sub (q : ℝ) ξ).trans (h.le.trans ?_)

Premises used: LT.lt.le, Rat.cast, abs_sub_abs_le_abs_sub, LE.le.trans
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : |(↑q : ℝ) - ξ| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
refine : 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 ≤ 1
⊢ |(↑q : ℝ)| - |ξ| ≤ 1

Tactic:
refine (abs_sub_abs_le_abs_sub (q : ℝ) ξ).trans (h.le.trans ?_)

Premises used: LT.lt.le, Rat.cast, abs_sub_abs_le_abs_sub, LE.le.trans
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : |(↑q : ℝ) - ξ| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
rw : 1 ≤ q.den
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 ≤ 1

Tactic:
rw [div_le_one h0, one_le_sq_iff_one_le_abs, Nat.abs_cast, Nat.one_le_cast]

Premises used: Nat.abs_cast, Nat.one_le_cast, one_le_sq_iff_one_le_abs, div_le_one
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : |(↑q : ℝ) - ξ| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
⊢ 1 ≤ q.den

Tactic:
q.pos

Premises used: Rat.pos, Nat.lt
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
q : ℚ
h : |(↑q : ℝ) - ξ| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
⊢ 1 ≤ q.den

Tactic:
exact q.pos

Premises used: Rat.pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
⊢ Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}

Tactic:
have hM : {q : ℚ | |q.1 ^ 2 - d * (q.2 : ℤ) ^ 2| < M}.Infinite := by
    refine Infinite.mono (fun q h => ?_) (infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational hξ)
    have h0 : 0 < (q.2 : ℝ) ^ 2 := pow_pos (Nat.cast_pos.mpr q.pos) 2
    have h1 : (q.num : ℝ) / (q.den : ℝ) = q := mod_cast q.num_div_den
    rw [mem_setOf, abs_sub_comm, ← @Int.cast_lt ℝ,
      ← div_lt_div_iff_of_pos_right (abs_pos_of_pos h0)]
    push_cast
    rw [← abs_div, abs_sq, sub_div, mul_div_cancel_right₀ _ h0.ne', ← div_pow, h1, ←
      sq_sqrt (Int.cast_pos.mpr h₀).le, sq_sub_sq, abs_mul, ← mul_one_div]
    refine mul_lt_mul'' (((abs_add_le ξ q).trans ?_).trans_lt hM₁) h (abs_nonneg _) (abs_nonneg _)
    rw [two_mul, add_assoc, add_le_add_iff_left, ← sub_le_iff_le_add']
    rw [mem_setOf, abs_sub_comm] at h
    refine (abs_sub_abs_le_abs_sub (q : ℝ) ξ).trans (h.le.trans ?_)
    rw [div_le_one h0, one_le_sq_iff_one_le_abs, Nat.abs_cast, Nat.one_le_cast]
    exact q.pos
-- Module: Mathlib.NumberTheory.Pell
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}
contrapose! :
  ∀
    (hM :
      ∀ (m : ℤ),
        Set.Finite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}),
    Set.Finite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
⊢ ∃ (m : ℤ),
    Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}

Tactic:
contrapose! hM
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM :
  ∀ (m : ℤ),
    Set.Finite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
⊢ Set.Finite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}

Tactic:
(congr_arg _ (ext fun x => ?_)).mp (Finite.biUnion (finite_Ioo (-M) M) fun m _ => hM m)

Premises used: Set.ext, Eq.mp, congr_arg, Set.finite_Ioo, Set.Finite.biUnion, Neg.neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM :
  ∀ (m : ℤ),
    Set.Finite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
refine :
  ∀ (x : ℚ),
    Membership.mem (γ := Set ℚ)
        (⋃ i ∈ Ioo (-M) M, {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = i})
        x ↔
      Membership.mem (γ := Set ℚ)
        {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M} x
⊢ Set.Finite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}

Tactic:
refine (congr_arg _ (ext fun x => ?_)).mp (Finite.biUnion (finite_Ioo (-M) M) fun m _ => hM m)

Premises used: Set.ext, Eq.mp, congr_arg, Set.finite_Ioo, Set.Finite.biUnion, Neg.neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)
hM :
  ∀ (m : ℤ),
    Set.Finite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
x : ℚ
⊢ Membership.mem (γ := Set ℚ)
      (⋃ i ∈ Ioo (-M) M, {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = i}) x ↔
    Membership.mem (γ := Set ℚ)
      {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M} x

Tactic:
simp only [abs_lt, mem_setOf, mem_Ioo, mem_iUnion, exists_prop, exists_eq_right']

Premises used: Set.mem_Ioo, exists_eq_right', Set.mem_iUnion, exists_prop, Set.mem_setOf, abs_lt
-- Module: Mathlib.NumberTheory.Pell
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}
obtain :
  ∀ (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
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0

Tactic:
obtain ⟨m, hm⟩ : ∃ m : ℤ, {q : ℚ | q.1 ^ 2 - d * (q.den : ℤ) ^ 2 = m}.Infinite := by
    contrapose! hM
    refine (congr_arg _ (ext fun x => ?_)).mp (Finite.biUnion (finite_Ioo (-M) M) fun m _ => hM m)
    simp only [abs_lt, mem_setOf, mem_Ioo, mem_iUnion, exists_prop, exists_eq_right']
-- Module: Mathlib.NumberTheory.Pell
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}
obtain :
  ∀ (q : ℚ)
    (hq :
      Membership.mem (γ := Set ℚ)
        {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = 0} q),
    False
⊢ False

Tactic:
obtain ⟨q, hq⟩ := hm.nonempty

Premises used: Set.Infinite.nonempty
-- Module: Mathlib.NumberTheory.Pell
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 :
  Membership.mem (γ := Set ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = 0}
    q
⊢ HPow.hPow (β := ℕ) q.num 2 = HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 * d

Tactic:
rw [mem_setOf, sub_eq_zero, mul_comm] at hq

Premises used: sub_eq_zero, Set.mem_setOf, mul_comm
-- Module: Mathlib.NumberTheory.Pell
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
obtain : ∀ (a : ℤ) (ha : q.num = (↑q.den : ℤ) * a), False
⊢ False

Tactic:
obtain ⟨a, ha⟩ := (Int.pow_dvd_pow_iff two_ne_zero).mp ⟨d, hq⟩

Premises used: Int.pow_dvd_pow_iff, two_ne_zero, Exists.intro, Iff.mp
-- Module: Mathlib.NumberTheory.Pell
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
⊢ 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

Premises used: Iff.mpr, pow_pos, Rat.pos, LT.lt.ne', mul_right_inj', OfNat.ofNat, mul_pow, Int.natCast_pos
-- Module: Mathlib.NumberTheory.Pell
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
hq₁ : HPow.hPow (β := ℕ) a 2 = d
⊢ q.num = (↑q.den : ℤ) * a

Tactic:
rw [ha, mul_pow, mul_right_inj' (pow_pos (Int.natCast_pos.mpr q.pos) 2).ne'] at hq

Premises used: Iff.mpr, pow_pos, Rat.pos, LT.lt.ne', mul_right_inj', OfNat.ofNat, mul_pow, Int.natCast_pos
-- Module: Mathlib.NumberTheory.Pell
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 : ℚ
a : ℤ
hq : HPow.hPow (β := ℕ) a 2 = d
ha : q.num = (↑q.den : ℤ) * a
⊢ False

Tactic:
hd ⟨a, sq a ▸ hq.symm⟩

Premises used: Eq.rec, sq, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.Pell
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 : ℚ
a : ℤ
hq : HPow.hPow (β := ℕ) a 2 = d
ha : q.num = (↑q.den : ℤ) * a
⊢ False

Tactic:
exact hd ⟨a, sq a ▸ hq.symm⟩

Premises used: Eq.rec, sq, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.Pell
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}
⊢ 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⟩
-- Module: Mathlib.NumberTheory.Pell
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
⊢ NeZero m.natAbs

Tactic:
haveI := neZero_iff.mpr (Int.natAbs_ne_zero.mpr hm₀)
-- Module: Mathlib.NumberTheory.Pell
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))
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
⊢ ∃ (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

Premises used: Set.mapsTo_univ, Set.finite_univ, Set.Infinite.exists_ne_map_eq_of_mapsTo
-- Module: Mathlib.NumberTheory.Pell
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₂
⊢ 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

Premises used: Int.cast, Rat.num, Rat.den, Prod.ext_iff, Nat.cast, Iff.mp
-- Module: Mathlib.NumberTheory.Pell
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)
⊢ 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

Premises used: Int.cast, Rat.num, Rat.den, Prod.ext_iff, Nat.cast, Iff.mp
-- Module: Mathlib.NumberTheory.Pell
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 : Eq (α := ZMod m.natAbs) (↑(q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)) : ZMod m.natAbs) 0
⊢ m ∣ q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)

Tactic:
rw [← Int.natAbs_dvd, ← ZMod.intCast_zmod_eq_zero_iff_dvd]

Premises used: ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natAbs_dvd
-- Module: Mathlib.NumberTheory.Pell
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)
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
⊢ Eq (α := ZMod m.natAbs) (↑(q₁.num * q₂.num - d * HMul.hMul (α := ℤ) (↑q₁.den : ℤ) (↑q₂.den : ℤ)) : ZMod m.natAbs) 0

Tactic:
push_cast