awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℤ
ofNat : (a ^ Int.ofNat 0).y.sign = (Int.ofNat 0).sign
⊢ (a ^ n).y.sign = n.sign
have ofNat₁ : ∀ (n : ℕ), (a ^ Int.ofNat (n + 1)).y.sign = (Int.ofNat (n + 1)).sign
Tactic: rcases n with ((_ | n) | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℤ
ofNat : (a ^ Int.ofNat 0).y.sign = (Int.ofNat 0).sign
ofNat₁ : ∀ (n : ℕ), (a ^ Int.ofNat (n + 1)).y.sign = (Int.ofNat (n + 1)).sign
⊢ (a ^ n).y.sign = n.sign
have negSucc : ∀ (n : ℕ), (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign
Tactic: rcases n with ((_ | n) | n)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.ofNat (n + 1)).y.sign = (Int.ofNat (n + 1)).sign
have ofNat : (a ^ (n + 1)).y.sign = Int.sign (↑(n + 1) : ℤ)
Tactic: rw [Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign
have negSucc : (a ^ (n + 1))⁻¹.y.sign = (Int.negSucc n).sign
Tactic: rw [zpow_negSucc]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
⊢ ∃ (b : Solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ Membership.mem (γ := Set (Solution₁ d)) {b, b⁻¹, -b, -b⁻¹} a
have refine_1 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 < (-a⁻¹).x
Tactic: refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
refine_1 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 < (-a⁻¹).x
⊢ ∃ (b : Solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ Membership.mem (γ := Set (Solution₁ d)) {b, b⁻¹, -b, -b⁻¹} a
have refine_2 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 ≤ (-a⁻¹).y
Tactic: refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
refine_1 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 < (-a⁻¹).x
refine_2 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 ≤ (-a⁻¹).y
⊢ ∃ (b : Solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ Membership.mem (γ := Set (Solution₁ d)) {b, b⁻¹, -b, -b⁻¹} a
have refine_3 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹} a
Tactic: refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
refine_1 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 < (-a⁻¹).x
refine_2 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 ≤ (-a⁻¹).y
refine_3 :
  ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹} a
⊢ ∃ (b : Solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ Membership.mem (γ := Set (Solution₁ d)) {b, b⁻¹, -b, -b⁻¹} a
have refine_4 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 < (-a).x
Tactic: refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
refine_1 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 < (-a⁻¹).x
refine_2 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 ≤ (-a⁻¹).y
refine_3 :
  ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹} a
refine_4 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 < (-a).x
⊢ ∃ (b : Solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ Membership.mem (γ := Set (Solution₁ d)) {b, b⁻¹, -b, -b⁻¹} a
have refine_5 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 ≤ (-a).y
Tactic: refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
refine_1 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 < (-a⁻¹).x
refine_2 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 ≤ (-a⁻¹).y
refine_3 :
  ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹} a
refine_4 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 < (-a).x
refine_5 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 ≤ (-a).y
⊢ ∃ (b : Solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ Membership.mem (γ := Set (Solution₁ d)) {b, b⁻¹, -b, -b⁻¹} a
have refine_6 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a, (-a)⁻¹, - -a, -(-a)⁻¹} a
Tactic: refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
refine_1 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 < (-a⁻¹).x
refine_2 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 ≤ (-a⁻¹).y
refine_3 :
  ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹} a
refine_4 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 < (-a).x
refine_5 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 ≤ (-a).y
refine_6 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a, (-a)⁻¹, - -a, -(-a)⁻¹} a
⊢ ∃ (b : Solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ Membership.mem (γ := Set (Solution₁ d)) {b, b⁻¹, -b, -b⁻¹} a
have refine_7 : ∀ (hy : 0 ≤ a.y) (hx : 0 < a.x), Membership.mem (γ := Set (Solution₁ d)) {a, a⁻¹, -a, -a⁻¹} a
Tactic: refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
refine_1 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 < (-a⁻¹).x
refine_2 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 ≤ (-a⁻¹).y
refine_3 :
  ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹} a
refine_4 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 < (-a).x
refine_5 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 ≤ (-a).y
refine_6 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a, (-a)⁻¹, - -a, -(-a)⁻¹} a
refine_7 : ∀ (hy : 0 ≤ a.y) (hx : 0 < a.x), Membership.mem (γ := Set (Solution₁ d)) {a, a⁻¹, -a, -a⁻¹} a
⊢ ∃ (b : Solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ Membership.mem (γ := Set (Solution₁ d)) {b, b⁻¹, -b, -b⁻¹} a
have refine_8 : ∀ (hy : a.y ≤ 0) (hx : 0 < a.x), 0 ≤ a⁻¹.y
Tactic: refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
refine_1 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 < (-a⁻¹).x
refine_2 : ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), 0 ≤ (-a⁻¹).y
refine_3 :
  ∀ (hy : 0 ≤ a.y) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹} a
refine_4 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 < (-a).x
refine_5 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), 0 ≤ (-a).y
refine_6 : ∀ (hy : a.y ≤ 0) (hx : a.x < 0), Membership.mem (γ := Set (Solution₁ d)) {-a, (-a)⁻¹, - -a, -(-a)⁻¹} a
refine_7 : ∀ (hy : 0 ≤ a.y) (hx : 0 < a.x), Membership.mem (γ := Set (Solution₁ d)) {a, a⁻¹, -a, -a⁻¹} a
refine_8 : ∀ (hy : a.y ≤ 0) (hx : 0 < a.x), 0 ≤ a⁻¹.y
⊢ ∃ (b : Solution₁ d), 0 < b.x ∧ 0 ≤ b.y ∧ Membership.mem (γ := Set (Solution₁ d)) {b, b⁻¹, -b, -b⁻¹} a
have refine_9 : ∀ (hy : a.y ≤ 0) (hx : 0 < a.x), Membership.mem (γ := Set (Solution₁ d)) {a⁻¹, a⁻¹⁻¹, -a⁻¹, -a⁻¹⁻¹} a
Tactic: refine
        (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
          ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, ?_, ?_, ?_⟩) fun hy hx => ⟨-a, ?_, ?_, ?_⟩)
          ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, ?_⟩) fun hy hx => ⟨a⁻¹, hx, ?_, ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
⊢ Irrational ξ
have refine : ¬∃ (y : ℤ), ξ = (↑y : ℝ)
Tactic: refine irrational_nrt_of_notint_nrt 2 d (sq_sqrt <| Int.cast_nonneg h₀.le) ?_ two_pos
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
x : ℤ
hx : ξ = (↑x : ℝ)
⊢ False
have refine : Eq (α := ℝ) (↑d : ℝ) (↑(x * x) : ℝ)
Tactic: refine hd ⟨x, @Int.cast_injective ℝ _ _ d (x * x) ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
x : ℤ
hx : ξ = (↑x : ℝ)
⊢ Eq (α := ℝ) (↑d : ℝ) (↑(x * x) : ℝ)
have rw : HPow.hPow (β := ℕ) (√(↑d : ℝ)) 2 = (↑(x * x) : ℝ)
Tactic: rw [← sq_sqrt <| Int.cast_nonneg h₀.le, Int.cast_mul, ← hx, sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
x : ℤ
hx : ξ = (↑x : ℝ)
rw : HPow.hPow (β := ℕ) (√(↑d : ℝ)) 2 = (↑(x * x) : ℝ)
⊢ Eq (α := ℝ) (↑d : ℝ) (↑(x * x) : ℝ)
have rw₁ : HPow.hPow (β := ℕ) (√(↑d : ℝ)) 2 = HMul.hMul (α := ℝ) (↑x : ℝ) (↑x : ℝ)
Tactic: rw [← sq_sqrt <| Int.cast_nonneg h₀.le, Int.cast_mul, ← hx, sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
x : ℤ
hx : ξ = (↑x : ℝ)
rw : HPow.hPow (β := ℕ) (√(↑d : ℝ)) 2 = (↑(x * x) : ℝ)
rw₁ : HPow.hPow (β := ℕ) (√(↑d : ℝ)) 2 = HMul.hMul (α := ℝ) (↑x : ℝ) (↑x : ℝ)
⊢ Eq (α := ℝ) (↑d : ℝ) (↑(x * x) : ℝ)
have rw₂ : HPow.hPow (β := ℕ) (√(↑d : ℝ)) 2 = ξ * ξ
Tactic: rw [← sq_sqrt <| Int.cast_nonneg h₀.le, Int.cast_mul, ← hx, sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
x : ℤ
hx : ξ = (↑x : ℝ)
rw : HPow.hPow (β := ℕ) (√(↑d : ℝ)) 2 = (↑(x * x) : ℝ)
rw₁ : HPow.hPow (β := ℕ) (√(↑d : ℝ)) 2 = HMul.hMul (α := ℝ) (↑x : ℝ) (↑x : ℝ)
rw₂ : HPow.hPow (β := ℕ) (√(↑d : ℝ)) 2 = ξ * ξ
⊢ Eq (α := ℝ) (↑d : ℝ) (↑(x * x) : ℝ)
have rw₃ : √(↑d : ℝ) * √(↑d : ℝ) = ξ * ξ
Tactic: rw [← sq_sqrt <| Int.cast_nonneg h₀.le, Int.cast_mul, ← hx, sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (hypothesis)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have hξ : Irrational ξ
Tactic: have hξ : Irrational ξ := by
    refine irrational_nrt_of_notint_nrt 2 d (sq_sqrt <| Int.cast_nonneg h₀.le) ?_ two_pos
    rintro ⟨x, hx⟩
    refine hd ⟨x, @Int.cast_injective ℝ _ _ d (x * x) ?_⟩
    rw [← sq_sqrt <| Int.cast_nonneg h₀.le, Int.cast_mul, ← hx, sq]
-- Lean 4 proof step from Mathlib.NumberTheory.Pell (goal)
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have obtain : ∀ (M : ℤ) (hM₁ : 2 * |ξ| + 1 < (↑M : ℝ)),
  ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
Tactic: obtain ⟨M, hM₁⟩ := exists_int_gt (2 * |ξ| + 1)
-- 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 : ℝ)
⊢ Set.Infinite (α := ℚ) {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M}
have refine : ∀ (q : ℚ) (h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q),
  Membership.mem (γ := Set ℚ)
    {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M} q
Tactic: refine Infinite.mono (fun q h => ?_) (infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational 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 : ℝ)
q : ℚ
h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
⊢ Membership.mem (γ := Set ℚ)
    {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M} q
have h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
Tactic: have h0 : 0 < (q.2 : ℝ) ^ 2 := pow_pos (Nat.cast_pos.mpr q.pos) 2
-- 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 : ℝ)
q : ℚ
h : Membership.mem (γ := Set ℚ) {q : ℚ | |ξ - (↑q : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2} q
h0 : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
⊢ Membership.mem (γ := Set ℚ)
    {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M} q
have h1 : HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)
Tactic: have h1 : (q.num : ℝ) / (q.den : ℝ) = q := mod_cast q.num_div_den
-- 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 : ℝ)
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 : ℝ)
⊢ Membership.mem (γ := Set ℚ)
    {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M} q
have rw : (↑|d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 - HPow.hPow (β := ℕ) q.num 2| : ℝ) /
    |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2| <
  (↑M : ℝ) / |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2|
Tactic: rw [mem_setOf, abs_sub_comm, ← @Int.cast_lt ℝ,
      ← div_lt_div_iff_of_pos_right (abs_pos_of_pos h0)]
-- 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 : ℝ)
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 * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 - HPow.hPow (β := ℕ) q.num 2| : ℝ) /
      |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2| <
    (↑M : ℝ) / |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2|
have push_cast : |(↑d : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 - HPow.hPow (α := ℝ) (β := ℕ) (↑q.num : ℝ) 2| /
    |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2| <
  (↑M : ℝ) / |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2|
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 : ℝ)
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 : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 - HPow.hPow (α := ℝ) (β := ℕ) (↑q.num : ℝ) 2| /
      |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2| <
    (↑M : ℝ) / |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2|
have rw : |√(↑d : ℝ) + (↑q : ℝ)| * |√(↑d : ℝ) - (↑q : ℝ)| < (↑M : ℝ) * (1 / 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]
-- 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 : ℝ)
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)
have refine : |ξ| + |(↑q : ℝ)| ≤ 2 * |ξ| + 1
Tactic: refine mul_lt_mul'' (((abs_add_le ξ q).trans ?_).trans_lt hM₁) h (abs_nonneg _) (abs_nonneg _)
-- 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 : ℝ)
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 : ℝ)| ≤ 2 * |ξ| + 1
have rw : |(↑q : ℝ)| - |ξ| ≤ 1
Tactic: rw [two_mul, add_assoc, add_le_add_iff_left, ← sub_le_iff_le_add']
-- 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 : ℝ)
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
have h₁ : |(↑q : ℝ) - ξ| < 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2
Tactic: rw [mem_setOf, abs_sub_comm] at h
Cleared hypotheses: h, h0, h1
-- 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 : ℝ)
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
have refine : 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 ≤ 1
Tactic: refine (abs_sub_abs_le_abs_sub (q : ℝ) ξ).trans (h.le.trans ?_)
-- 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 : ℝ)
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 / HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 ≤ 1
have rw : 1 ≤ q.den
Tactic: rw [div_le_one h0, one_le_sq_iff_one_le_abs, Nat.abs_cast, Nat.one_le_cast]
-- 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 : ℝ)
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have hM : 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
-- 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 : ℤ),
    Set.Infinite (α := ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = m}
have 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}
Tactic: contrapose! hM
Cleared hypotheses: 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 :
  ∀ (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}
have 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
Tactic: refine (congr_arg _ (ext fun x => ?_)).mp (Finite.biUnion (finite_Ioo (-M) M) fun m _ => hM m)
-- 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}
⊢ ∃ (x : ℤ) (y : ℤ), HPow.hPow (β := ℕ) x 2 - d * HPow.hPow (β := ℕ) y 2 = 1 ∧ y ≠ 0
have 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
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']
-- 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}
⊢ False
have obtain : ∀ (q : ℚ)
  (hq :
    Membership.mem (γ := Set ℚ)
      {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = 0} q),
  False
Tactic: obtain ⟨q, hq⟩ := hm.nonempty
-- 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 :
  Membership.mem (γ := Set ℚ) {q : ℚ | HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 = 0}
    q
⊢ False
have hq₁ : HPow.hPow (β := ℕ) q.num 2 = HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 * d
Tactic: rw [mem_setOf, sub_eq_zero, mul_comm] at hq
Cleared hypotheses: hq