awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
rw :
  0 < (1 + d * HPow.hPow (β := ℕ) a.y 2) * (1 + d * HPow.hPow (β := ℕ) b.y 2) - HPow.hPow (β := ℕ) (d * (a.y * b.y)) 2
⊢ |d * (a.y * b.y)| < a.x * b.x

Tactic:
rw [← abs_of_pos ha, ← abs_of_pos hb, ← abs_mul, ← sq_lt_sq, mul_pow a.x, a.prop_x, b.prop_x, ←
    sub_pos]

Premises used: sub_pos, Pell.Solution₁.x, abs_mul, sq_lt_sq, Pell.Solution₁.prop_x, abs_of_pos, mul_pow
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
ring_nf : 0 < 1 + d * HPow.hPow (β := ℕ) a.y 2 + d * HPow.hPow (β := ℕ) b.y 2
⊢ 0 < (1 + d * HPow.hPow (β := ℕ) a.y 2) * (1 + d * HPow.hPow (β := ℕ) b.y 2) - HPow.hPow (β := ℕ) (d * (a.y * b.y)) 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
inl : ∀ (h : 0 ≤ d), 0 < 1 + d * HPow.hPow (β := ℕ) a.y 2 + d * HPow.hPow (β := ℕ) b.y 2
inr : ∀ (h : d < 0), 0 < 1 + d * HPow.hPow (β := ℕ) a.y 2 + d * HPow.hPow (β := ℕ) b.y 2
⊢ 0 < 1 + d * HPow.hPow (β := ℕ) a.y 2 + d * HPow.hPow (β := ℕ) b.y 2

Tactic:
rcases le_or_gt 0 d with h | h

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : 0 ≤ d
⊢ 0 < 1 + d * HPow.hPow (β := ℕ) a.y 2 + d * HPow.hPow (β := ℕ) b.y 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : d < 0
inr : 0 < 1 + d * HPow.hPow (α := ℤ) (β := ℕ) 0 2 + d * HPow.hPow (α := ℤ) (β := ℕ) 0 2
⊢ 0 < 1 + d * HPow.hPow (β := ℕ) a.y 2 + d * HPow.hPow (β := ℕ) b.y 2

Tactic:
rw [(eq_zero_of_d_neg h a).resolve_left ha.ne', (eq_zero_of_d_neg h b).resolve_left hb.ne']

Premises used: Or.resolve_left, Pell.Solution₁.eq_zero_of_d_neg, LT.lt.ne'
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : d < 0
⊢ 0 < 1 + d * HPow.hPow (α := ℤ) (β := ℕ) 0 2 + d * HPow.hPow (α := ℤ) (β := ℕ) 0 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
hbx : 0 < b.x
hby : 0 < b.y
simp : 0 < a.x * b.y + a.y * b.x
⊢ 0 < (a * b).y

Tactic:
simp only [y_mul]

Premises used: Pell.Solution₁.y_mul
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a b : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
hbx : 0 < b.x
hby : 0 < b.y
⊢ 0 < a.x * b.y + a.y * b.x

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
⊢ 0 < (HPow.hPow (β := ℕ) a 0).x

Tactic:
simp only [pow_zero, x_one, zero_lt_one]

Premises used: Pell.Solution₁.x_one, pow_zero, zero_lt_one
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
ih : 0 < (a ^ n).x
⊢ 0 < (a ^ n * a).x

Tactic:
x_mul_pos ih hax

Premises used: Pell.Solution₁.x_mul_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
ih : 0 < (a ^ n).x
⊢ 0 < (a ^ n * a).x

Tactic:
exact x_mul_pos ih hax

Premises used: Pell.Solution₁.x_mul_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
zero : 0 < (HPow.hPow (β := ℕ) a 0).x
succ : ∀ (n : ℕ) (ih : 0 < (a ^ n).x), 0 < (a ^ (n + 1)).x
⊢ 0 < (a ^ n).x

Tactic:
induction n with
  | zero => simp only [pow_zero, x_one, zero_lt_one]
  | succ n ih => rw [pow_succ]; exact x_mul_pos ih hax

Premises used: pow_succ, Pell.Solution₁.x_one, pow_zero, zero_lt_one
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
⊢ 0 < (a ^ Nat.succ 0).y

Tactic:
simp only [pow_one, hay]

Premises used: pow_one
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
ih : 0 < (a ^ n.succ).y
succ : 0 < (a * a ^ (n + 1)).y
⊢ 0 < (a ^ (n + 1).succ).y

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
ih : 0 < (a ^ n.succ).y
⊢ 0 < (a * a ^ (n + 1)).y

Tactic:
y_mul_pos hax hay (x_pow_pos hax _) ih

Premises used: Pell.Solution₁.y_mul_pos, Pell.Solution₁.x_pow_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
ih : 0 < (a ^ n.succ).y
⊢ 0 < (a * a ^ (n + 1)).y

Tactic:
exact y_mul_pos hax hay (x_pow_pos hax _) ih

Premises used: Pell.Solution₁.y_mul_pos, Pell.Solution₁.x_pow_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
zero : 0 < (a ^ Nat.succ 0).y
succ : ∀ (n : ℕ) (ih : 0 < (a ^ n.succ).y), 0 < (a ^ (n + 1).succ).y
⊢ 0 < (a ^ n.succ).y

Tactic:
induction n with
  | zero => simp only [pow_one, hay]
  | succ n ih => rw [pow_succ']; exact y_mul_pos hax hay (x_pow_pos hax _) ih

Premises used: pow_one, pow_succ'
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℤ
hn : 0 < n
⊢ 0 ≤ n

Tactic:
hn.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℤ
hn : 0 < n
lift : ∀ (n : ℕ) (hn : LT.lt (α := ℤ) 0 (↑n : ℤ)), 0 < (HPow.hPow (β := ℤ) a (↑n : ℤ)).y
⊢ 0 < (a ^ n).y

Tactic:
lift n to ℕ using hn.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : LT.lt (α := ℤ) 0 (↑n : ℤ)
norm_cast : ∀ (hn : 0 < n), 0 < (a ^ n).y
⊢ 0 < (HPow.hPow (β := ℤ) a (↑n : ℤ)).y

Tactic:
norm_cast at hn ⊢
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < n
rw : 0 < (a ^ n.pred.succ).y
⊢ 0 < (a ^ n).y

Tactic:
rw [← Nat.succ_pred_eq_of_pos hn]

Premises used: Nat.succ_pred_eq_of_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < n
⊢ 0 < (a ^ n.pred.succ).y

Tactic:
y_pow_succ_pos hax hay _

Premises used: Pell.Solution₁.y_pow_succ_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
hn : 0 < n
⊢ 0 < (a ^ n.pred.succ).y

Tactic:
exact y_pow_succ_pos hax hay _

Premises used: Pell.Solution₁.y_pow_succ_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
ofNat : 0 < (a ^ n).x
⊢ 0 < (a ^ Int.ofNat n).x

Tactic:
rw [Int.ofNat_eq_natCast, zpow_natCast]

Premises used: zpow_natCast, Int.ofNat_eq_natCast
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ n).x

Tactic:
x_pow_pos hax n

Premises used: Pell.Solution₁.x_pow_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ n).x

Tactic:
exact x_pow_pos hax n

Premises used: Pell.Solution₁.x_pow_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
negSucc : 0 < (a ^ (n + 1))⁻¹.x
⊢ 0 < (a ^ Int.negSucc n).x

Tactic:
rw [zpow_negSucc]

Premises used: zpow_negSucc
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ (n + 1))⁻¹.x

Tactic:
x_pow_pos hax (n + 1)

Premises used: Pell.Solution₁.x, npowRec, HAdd.hAdd, Pell.Solution₁.x_pow_pos, Int.neg.match_1, OfNat.ofNat, Int.add, Int.neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ (n + 1))⁻¹.x

Tactic:
exact x_pow_pos hax (n + 1)

Premises used: HAdd.hAdd, Pell.Solution₁.x_pow_pos, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℤ
ofNat : ∀ (n : ℕ), 0 < (a ^ Int.ofNat n).x
negSucc : ∀ (n : ℕ), 0 < (a ^ Int.negSucc n).x
⊢ 0 < (a ^ n).x

Tactic:
cases n with
  | ofNat n =>
    rw [Int.ofNat_eq_natCast, zpow_natCast]
    exact x_pow_pos hax n
  | negSucc n =>
    rw [zpow_negSucc]
    exact x_pow_pos hax (n + 1)

Premises used: zpow_natCast, zpow_negSucc, Int.ofNat_eq_natCast
-- Module: Mathlib.NumberTheory.Pell
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
negSucc : ∀ (n : ℕ), (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign
⊢ (a ^ n).y.sign = n.sign

Tactic:
rcases n with ((_ | n) | n)
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
⊢ (a ^ Int.ofNat 0).y.sign = (Int.ofNat 0).sign

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
ofNat : (a ^ (n + 1)).y.sign = Int.sign (↑(n + 1) : ℤ)
⊢ (a ^ Int.ofNat (n + 1)).y.sign = (Int.ofNat (n + 1)).sign

Tactic:
rw [Int.ofNat_eq_natCast, zpow_natCast]

Premises used: zpow_natCast, Int.ofNat_eq_natCast
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1)).y.sign = Int.sign (↑(n + 1) : ℤ)

Tactic:
Int.sign_eq_one_of_pos (y_pow_succ_pos hax hay n)

Premises used: Pell.Solution₁.y_pow_succ_pos, Int.sign, Int.sign_eq_one_of_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1)).y.sign = Int.sign (↑(n + 1) : ℤ)

Tactic:
exact Int.sign_eq_one_of_pos (y_pow_succ_pos hax hay n)

Premises used: Pell.Solution₁.y_pow_succ_pos, Int.sign_eq_one_of_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
negSucc : (a ^ (n + 1))⁻¹.y.sign = (Int.negSucc n).sign
⊢ (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign

Tactic:
rw [zpow_negSucc]

Premises used: zpow_negSucc
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1))⁻¹.y.sign = (Int.negSucc n).sign

Tactic:
Int.sign_eq_neg_one_of_neg (neg_neg_of_pos (y_pow_succ_pos hax hay n))

Premises used: Pell.Solution₁.y_pow_succ_pos, Int.sign_eq_neg_one_of_neg, Int.sign, neg_neg_of_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1))⁻¹.y.sign = (Int.negSucc n).sign

Tactic:
exact Int.sign_eq_neg_one_of_neg (neg_neg_of_pos (y_pow_succ_pos hax hay n))

Premises used: Pell.Solution₁.y_pow_succ_pos, Int.sign_eq_neg_one_of_neg, neg_neg_of_pos
-- Module: Mathlib.NumberTheory.Pell
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

Tactic:
(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, ?_, ?_⟩)

Premises used: lt_or_gt_of_ne, LT.lt.le, le_total, Pell.Solution₁.y, Inv.inv, And.intro, Exists.intro, Or.elim, OfNat.ofNat, Pell.Solution₁.x_ne_zero, Neg.neg
-- Module: Mathlib.NumberTheory.Pell
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
refine_9 : ∀ (hy : a.y ≤ 0) (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

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, ?_, ?_⟩)

Premises used: lt_or_gt_of_ne, LT.lt.le, le_total, Pell.Solution₁.y, Or.elim, OfNat.ofNat, Pell.Solution₁.x_ne_zero
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
refine_1 : a.x < 0
⊢ 0 < (-a⁻¹).x

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Premises used: neg_pos, true_or, Pell.Solution₁.y_neg, neg_neg, Pell.Solution₁.y_inv, Pell.Solution₁.x_neg, Pell.Solution₁.x_inv, neg_nonneg, Set.mem_singleton_iff, neg_inv, inv_inv, Set.mem_insert_iff, or_true
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
refine_2 : 0 ≤ a.y
⊢ 0 ≤ (-a⁻¹).y

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Premises used: neg_pos, true_or, Pell.Solution₁.y_neg, neg_neg, Pell.Solution₁.y_inv, Pell.Solution₁.x_neg, Pell.Solution₁.x_inv, neg_nonneg, Set.mem_singleton_iff, neg_inv, inv_inv, Set.mem_insert_iff, or_true
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ Membership.mem (γ := Set (Solution₁ d)) {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹} a

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Premises used: neg_pos, true_or, Pell.Solution₁.y_neg, neg_neg, Pell.Solution₁.y_inv, Pell.Solution₁.x_neg, Pell.Solution₁.x_inv, neg_nonneg, Set.mem_singleton_iff, neg_inv, inv_inv, Set.mem_insert_iff, or_true
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
refine_4 : a.x < 0
⊢ 0 < (-a).x

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Premises used: neg_pos, true_or, Pell.Solution₁.y_neg, neg_neg, Pell.Solution₁.y_inv, Pell.Solution₁.x_neg, Pell.Solution₁.x_inv, neg_nonneg, Set.mem_singleton_iff, neg_inv, inv_inv, Set.mem_insert_iff, or_true
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
refine_5 : a.y ≤ 0
⊢ 0 ≤ (-a).y

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Premises used: neg_pos, true_or, Pell.Solution₁.y_neg, neg_neg, Pell.Solution₁.y_inv, Pell.Solution₁.x_neg, Pell.Solution₁.x_inv, neg_nonneg, Set.mem_singleton_iff, neg_inv, inv_inv, Set.mem_insert_iff, or_true
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ Membership.mem (γ := Set (Solution₁ d)) {-a, (-a)⁻¹, - -a, -(-a)⁻¹} a

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Premises used: neg_pos, true_or, Pell.Solution₁.y_neg, neg_neg, Pell.Solution₁.y_inv, Pell.Solution₁.x_neg, Pell.Solution₁.x_inv, neg_nonneg, Set.mem_singleton_iff, neg_inv, inv_inv, Set.mem_insert_iff, or_true
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : 0 < a.x
⊢ Membership.mem (γ := Set (Solution₁ d)) {a, a⁻¹, -a, -a⁻¹} a

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Premises used: neg_pos, true_or, Pell.Solution₁.y_neg, neg_neg, Pell.Solution₁.y_inv, Pell.Solution₁.x_neg, Pell.Solution₁.x_inv, neg_nonneg, Set.mem_singleton_iff, neg_inv, inv_inv, Set.mem_insert_iff, or_true
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
refine_8 : a.y ≤ 0
⊢ 0 ≤ a⁻¹.y

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Premises used: neg_pos, true_or, Pell.Solution₁.y_neg, neg_neg, Pell.Solution₁.y_inv, Pell.Solution₁.x_neg, Pell.Solution₁.x_inv, neg_nonneg, Set.mem_singleton_iff, neg_inv, inv_inv, Set.mem_insert_iff, or_true
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ Membership.mem (γ := Set (Solution₁ d)) {a⁻¹, a⁻¹⁻¹, -a⁻¹, -a⁻¹⁻¹} a

Tactic:
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or,
        x_neg, x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true]

Premises used: neg_pos, true_or, Pell.Solution₁.y_neg, neg_neg, Pell.Solution₁.y_inv, Pell.Solution₁.x_neg, Pell.Solution₁.x_inv, neg_nonneg, Set.mem_singleton_iff, neg_inv, inv_inv, Set.mem_insert_iff, or_true
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ a.x < 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 ≤ a.y

Tactic:
assumption
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.x < 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a.y ≤ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ a.y ≤ 0

Tactic:
assumption
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
⊢ Irrational ξ

Tactic:
irrational_nrt_of_notint_nrt 2 d (sq_sqrt <| Int.cast_nonneg h₀.le) ?_ two_pos

Premises used: two_pos, irrational_nrt_of_notint_nrt, LT.lt.le, Real.sq_sqrt, Int.cast_nonneg, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
refine : ¬∃ (y : ℤ), ξ = (↑y : ℝ)
⊢ Irrational ξ

Tactic:
refine irrational_nrt_of_notint_nrt 2 d (sq_sqrt <| Int.cast_nonneg h₀.le) ?_ two_pos

Premises used: two_pos, irrational_nrt_of_notint_nrt, LT.lt.le, Real.sq_sqrt, Int.cast_nonneg, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
x : ℤ
hx : ξ = (↑x : ℝ)
⊢ False

Tactic:
hd ⟨x, @Int.cast_injective ℝ _ _ d (x * x) ?_⟩

Premises used: Exists.intro, Int.cast_injective
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
x : ℤ
hx : ξ = (↑x : ℝ)
refine : Eq (α := ℝ) (↑d : ℝ) (↑(x * x) : ℝ)
⊢ False

Tactic:
refine hd ⟨x, @Int.cast_injective ℝ _ _ d (x * x) ?_⟩

Premises used: Exists.intro, Int.cast_injective
-- Module: Mathlib.NumberTheory.Pell
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 = ξ * ξ
rw₃ rw₄ : √(↑d : ℝ) * √(↑d : ℝ) = ξ * ξ
⊢ Eq (α := ℝ) (↑d : ℝ) (↑(x * x) : ℝ)

Tactic:
rw [← sq_sqrt <| Int.cast_nonneg h₀.le, Int.cast_mul, ← hx, sq]

Premises used: LT.lt.le, Real.sq_sqrt, Int.cast_nonneg, sq, Int.cast_mul
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
⊢ 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]
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √(↑d : ℝ)
hξ : Irrational ξ
obtain :
  ∀ (M : ℤ) (hM₁ : 2 * |ξ| + 1 < (↑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₁⟩ := exists_int_gt (2 * |ξ| + 1)

Premises used: HMul.hMul, abs, exists_int_gt, HAdd.hAdd, OfNat.ofNat
-- 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:
Infinite.mono (fun q h => ?_) (infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational hξ)

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

Tactic:
refine Infinite.mono (fun q h => ?_) (infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational hξ)

Premises used: Set.Infinite.mono, Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational
-- 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
⊢ 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2

Tactic:
have h0 : 0 < (q.2 : ℝ) ^ 2 := pow_pos (Nat.cast_pos.mpr q.pos) 2
-- 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
⊢ HDiv.hDiv (α := ℝ) (↑q.num : ℝ) (↑q.den : ℝ) = (↑q : ℝ)

Tactic:
have h1 : (q.num : ℝ) / (q.den : ℝ) = q := mod_cast q.num_div_den
-- 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 * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2 - HPow.hPow (β := ℕ) q.num 2| : ℝ) /
      |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2| <
    (↑M : ℝ) / |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2|
⊢ Membership.mem (γ := Set ℚ)
    {q : ℚ | |HPow.hPow (β := ℕ) q.num 2 - d * HPow.hPow (α := ℤ) (β := ℕ) (↑q.den : ℤ) 2| < M} q

Tactic:
rw [mem_setOf, abs_sub_comm, ← @Int.cast_lt ℝ,
      ← div_lt_div_iff_of_pos_right (abs_pos_of_pos h0)]

Premises used: abs_pos_of_pos, div_lt_div_iff_of_pos_right, Int.cast_lt, 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 : ℝ)
push_cast :
  |(↑d : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2 - HPow.hPow (α := ℝ) (β := ℕ) (↑q.num : ℝ) 2| /
      |HPow.hPow (α := ℝ) (β := ℕ) (↑q.den : ℝ) 2| <
    (↑M : ℝ) / |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:
push_cast