awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
a : Solution₁ d
Hx : 1 < a.x
Hy : 0 < a.y
H : ∀ (a_1 : Solution₁ d), ∃ (n : ℤ), a_1 = a ^ n ∨ a_1 = -a ^ n
n₁ : ℤ
hn₁ : a₁ = a ^ n₁ ∨ a₁ = -a ^ n₁
n₂ : ℤ
hn₂ : a = a₁ ^ n₂ ∨ a = -a₁ ^ n₂
inl :
  ∀ (Hx : 1 < (a₁ ^ n₂).x) (Hy : 0 < (a₁ ^ n₂).y)
    (H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n)
    (hn₁ : a₁ = (a₁ ^ n₂) ^ n₁ ∨ a₁ = -(a₁ ^ n₂) ^ n₁), a₁ ^ n₂ = a₁
inr :
  ∀ (Hx : 1 < (-a₁ ^ n₂).x) (Hy : 0 < (-a₁ ^ n₂).y)
    (H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n)
    (hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁), -a₁ ^ n₂ = a₁
⊢ a = a₁

Tactic:
rcases hn₂ with (rfl | rfl)

Premises used: rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ = (a₁ ^ n₂) ^ n₁ ∨ a₁ = -(a₁ ^ n₂) ^ n₁
⊢ a₁ ^ (n₂ * n₁ - 1) = 1 ∨ -a₁ ^ (n₂ * n₁ - 1) = 1

Tactic:
rw [← zpow_mul, eq_comm, @eq_comm _ a₁, ← mul_inv_eq_one, ← @mul_inv_eq_one _ _ _ a₁, ←
      zpow_neg_one, neg_mul, ← zpow_add, ← sub_eq_add_neg] at hn₁

Premises used: zpow_add, zpow_neg_one, mul_inv_eq_one, zpow_mul, sub_eq_add_neg, eq_comm, neg_mul
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁ - 1) = 1 ∨ -a₁ ^ (n₂ * n₁ - 1) = 1
inl : ∀ (hn₁ : a₁ ^ (n₂ * n₁ - 1) = 1), a₁ ^ n₂ = a₁
inl₁ : ∀ (hn₁ : -a₁ ^ (n₂ * n₁ - 1) = 1), a₁ ^ n₂ = a₁
⊢ a₁ ^ n₂ = a₁

Tactic:
rcases hn₁ with hn₁ | hn₁
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁ - 1) = 1
inl :
  ∀ (Hx : 1 < (HPow.hPow (β := ℤ) a₁ 1).x) (Hy : 0 < (HPow.hPow (β := ℤ) a₁ 1).y)
    (H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ 1 ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ 1 ^ n)
    (hn₁ : a₁ ^ (1 * n₁ - 1) = 1), HPow.hPow (β := ℤ) a₁ 1 = a₁
inl₁ :
  ∀ (Hx : 1 < (HPow.hPow (β := ℤ) a₁ (-1)).x) (Hy : 0 < (HPow.hPow (β := ℤ) a₁ (-1)).y)
    (H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ (-1) ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ (-1) ^ n)
    (hn₁ : a₁ ^ (-1 * n₁ - 1) = 1), HPow.hPow (β := ℤ) a₁ (-1) = a₁
⊢ a₁ ^ n₂ = a₁

Tactic:
rcases Int.isUnit_iff.mp
          (.of_mul_eq_one _ <|
            sub_eq_zero.mp <| (ha₁.zpow_eq_one_iff (n₂ * n₁ - 1)).mp hn₁) with
        (rfl | rfl)

Premises used: HMul.hMul, Pell.IsFundamental.zpow_eq_one_iff, sub_eq_zero, IsUnit.of_mul_eq_one, HSub.hSub, Iff.mp, Int.isUnit_iff, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (HPow.hPow (β := ℤ) a₁ 1).x
Hy : 0 < (HPow.hPow (β := ℤ) a₁ 1).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ 1 ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ 1 ^ n
hn₁ : a₁ ^ (1 * n₁ - 1) = 1
inl inl₁ : a₁ = a₁
⊢ HPow.hPow (β := ℤ) a₁ 1 = a₁

Tactic:
rw [zpow_one]

Premises used: zpow_one
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (HPow.hPow (β := ℤ) a₁ (-1)).x
Hy : 0 < (HPow.hPow (β := ℤ) a₁ (-1)).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ (-1) ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ (-1) ^ n
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
⊢ a₁.y < 0

Tactic:
rw [zpow_neg_one, y_inv, lt_neg, neg_zero] at Hy

Premises used: lt_neg, zpow_neg_one, Pell.Solution₁.y_inv, neg_zero
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (HPow.hPow (β := ℤ) a₁ (-1)).x
Hy : 0 < (HPow.hPow (β := ℤ) a₁ (-1)).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ (-1) ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ (-1) ^ n
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
Hy₁ : a₁.y < 0
⊢ ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ (-1) ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ (-1) ^ n

Tactic:
rw [zpow_neg_one, y_inv, lt_neg, neg_zero] at Hy

Premises used: lt_neg, zpow_neg_one, Pell.Solution₁.y_inv, neg_zero
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (HPow.hPow (β := ℤ) a₁ (-1)).x
Hy : 0 < (HPow.hPow (β := ℤ) a₁ (-1)).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ (-1) ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ (-1) ^ n
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
Hy₁ : a₁.y < 0
H₁ : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ (-1) ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ (-1) ^ n
⊢ a₁ ^ (-1 * n₁ - 1) = 1

Tactic:
rw [zpow_neg_one, y_inv, lt_neg, neg_zero] at Hy

Premises used: lt_neg, zpow_neg_one, Pell.Solution₁.y_inv, neg_zero
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (HPow.hPow (β := ℤ) a₁ (-1)).x
Hy : a₁.y < 0
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ (-1) ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ (-1) ^ n
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
⊢ HPow.hPow (β := ℤ) a₁ (-1) = a₁

Tactic:
False.elim (lt_irrefl _ <| ha₁.2.1.trans Hy)

Premises used: lt_irrefl, False.elim, And.right, And.left, LT.lt.trans
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (HPow.hPow (β := ℤ) a₁ (-1)).x
Hy : a₁.y < 0
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = HPow.hPow (β := ℤ) a₁ (-1) ^ n ∨ a = -HPow.hPow (β := ℤ) a₁ (-1) ^ n
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
⊢ HPow.hPow (β := ℤ) a₁ (-1) = a₁

Tactic:
exact False.elim (lt_irrefl _ <| ha₁.2.1.trans Hy)

Premises used: lt_irrefl, False.elim, And.right, And.left, LT.lt.trans
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : -a₁ ^ (n₂ * n₁ - 1) = 1
⊢ HPow.hPow (β := ℤ) a₁ 0 = -a₁ ^ (n₂ * n₁ - 1)

Tactic:
rw [← zpow_zero a₁, eq_comm] at hn₁

Premises used: zpow_zero, eq_comm
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : HPow.hPow (β := ℤ) a₁ 0 = -a₁ ^ (n₂ * n₁ - 1)
⊢ a₁ ^ n₂ = a₁

Tactic:
False.elim (ha₁.zpow_ne_neg_zpow hn₁)

Premises used: Pell.IsFundamental.zpow_ne_neg_zpow, False.elim
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : HPow.hPow (β := ℤ) a₁ 0 = -a₁ ^ (n₂ * n₁ - 1)
⊢ a₁ ^ n₂ = a₁

Tactic:
exact False.elim (ha₁.zpow_ne_neg_zpow hn₁)

Premises used: Pell.IsFundamental.zpow_ne_neg_zpow, False.elim
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (-a₁ ^ n₂).x
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ (a₁ ^ n₂).x < -1

Tactic:
rw [x_neg, lt_neg] at Hx

Premises used: lt_neg, Pell.Solution₁.x_neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (-a₁ ^ n₂).x
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
Hx₁ : (a₁ ^ n₂).x < -1
⊢ 0 < (-a₁ ^ n₂).y

Tactic:
rw [x_neg, lt_neg] at Hx

Premises used: lt_neg, Pell.Solution₁.x_neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (-a₁ ^ n₂).x
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
Hx₁ : (a₁ ^ n₂).x < -1
Hy₁ : 0 < (-a₁ ^ n₂).y
⊢ ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n

Tactic:
rw [x_neg, lt_neg] at Hx

Premises used: lt_neg, Pell.Solution₁.x_neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (-a₁ ^ n₂).x
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
Hx₁ : (a₁ ^ n₂).x < -1
Hy₁ : 0 < (-a₁ ^ n₂).y
H₁ : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
⊢ a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁

Tactic:
rw [x_neg, lt_neg] at Hx

Premises used: lt_neg, Pell.Solution₁.x_neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : (a₁ ^ n₂).x < -1
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ LT.lt (α := ℤ) 0 (-1)

Tactic:
have := (x_zpow_pos (zero_lt_one.trans ha₁.1) n₂).trans Hx
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : (a₁ ^ n₂).x < -1
Hy : 0 < (-a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ (n : ℤ), a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
this : LT.lt (α := ℤ) 0 (-1)
⊢ -a₁ ^ n₂ = a₁

Tactic:
norm_num at this
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
⊢ (1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ (n : ℤ), b = a ^ n ∨ b = -a ^ n) ↔ IsFundamental a

Tactic:
⟨fun h => ?_, fun H => ⟨H.1, H.2.1, H.eq_zpow_or_neg_zpow⟩⟩

Premises used: Pell.IsFundamental.eq_zpow_or_neg_zpow, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
refine : ∀ (h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ (n : ℤ), b = a ^ n ∨ b = -a ^ n), IsFundamental a
⊢ (1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ (n : ℤ), b = a ^ n ∨ b = -a ^ n) ↔ IsFundamental a

Tactic:
refine ⟨fun h => ?_, fun H => ⟨H.1, H.2.1, H.eq_zpow_or_neg_zpow⟩⟩
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ (n : ℤ), b = a ^ n ∨ b = -a ^ n
⊢ 0 < d

Tactic:
have h₀ := d_pos_of_one_lt_x h.1
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ (n : ℤ), b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
⊢ ¬IsSquare d

Tactic:
have hd := d_nonsquare_of_one_lt_x h.1
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ (n : ℤ), b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
obtain : ∀ (a₁ : Solution₁ d) (ha₁ : IsFundamental a₁), IsFundamental a
⊢ IsFundamental a

Tactic:
obtain ⟨a₁, ha₁⟩ := IsFundamental.exists_of_not_isSquare h₀ hd

Premises used: Pell.IsFundamental.exists_of_not_isSquare
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ (n : ℤ), b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
obtain :
  ∀ (b : Solution₁ d)
    (hb₂ :
      ∀ (y : Solution₁ d),
        (fun (a₁ : Solution₁ d) ↦ 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ (n : ℤ), a = a₁ ^ n ∨ a = -a₁ ^ n) y →
          y = b),
    IsFundamental a
⊢ IsFundamental a

Tactic:
obtain ⟨b, -, hb₂⟩ := existsUnique_pos_generator h₀ hd

Premises used: Pell.existsUnique_pos_generator
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ (n : ℤ), b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
b : Solution₁ d
hb₂ :
  ∀ (y : Solution₁ d),
    (fun (a₁ : Solution₁ d) ↦ 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ (n : ℤ), a = a₁ ^ n ∨ a = -a₁ ^ n) y → y = b
rwa : IsFundamental b
rwa₁ rwa₂ rwa₃ rwa₄ : IsFundamental a₁
⊢ IsFundamental a

Tactic:
rwa [hb₂ a h, ← hb₂ a₁ ⟨ha₁.1, ha₁.2.1, ha₁.eq_zpow_or_neg_zpow⟩]

Premises used: Pell.IsFundamental.eq_zpow_or_neg_zpow, And.right, And.left, And.intro
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
d x y : ℤ
simp : x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1
⊢ IsPell (d := d) { re := x, im := y } ↔
    HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) = 1

Tactic:
simp [Zsqrtd.ext_iff, IsPell, mul_comm]

Premises used: mul_comm, Zsqrtd.ext_iff, Pell.IsPell
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
d x y : ℤ
⊢ x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
d x y : ℤ
rw :
  IsPell (d := d) { re := x, im := y } ↔
    HMul.hMul (α := ℤ√d) (star { re := x, im := y : ℤ√d }) { re := x, im := y : ℤ√d } = 1 ∧
      HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) = 1
rw₁ :
  HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) = 1 ↔
    HMul.hMul (α := ℤ√d) (star { re := x, im := y : ℤ√d }) { re := x, im := y : ℤ√d } = 1 ∧
      HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) = 1
rw₂ :
  HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) = 1 ↔
    HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) = 1 ∧
      HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) = 1
rw₃ rw₄ :
  HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) = 1 ↔
    HMul.hMul (α := ℤ√d) { re := x, im := y : ℤ√d } (star { re := x, im := y : ℤ√d }) = 1
⊢ IsPell (d := d) { re := x, im := y } ↔ Membership.mem (γ := Submonoid (ℤ√d)) (unitary (ℤ√d)) { re := x, im := y }

Tactic:
rw [Unitary.mem_iff, isPell_norm, mul_comm (star _), and_self_iff]

Premises used: Pell.isPell_norm, mul_comm, Unitary.mem_iff, and_self_iff, Star.star
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
d : ℤ
b c : ℤ√d
hb : IsPell b
hc : IsPell c
⊢ b * c * star (b * c) = 1

Tactic:
simp [mul_comm, mul_left_comm c, mul_assoc,
    star_mul, isPell_norm.1 hb, isPell_norm.1 hc]

Premises used: Pell.isPell_norm, mul_assoc, mul_left_comm, Iff.mp, mul_comm, StarMul.star_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
d x y : ℤ
⊢ IsPell (d := d) { re := x, im := y } ↔ IsPell (d := d) (star { re := x, im := y })

Tactic:
simp [IsPell]

Premises used: Pell.IsPell
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ LT.lt (α := ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ pell a1 n = (xn a1 n, yn a1 n)

Tactic:
show pell a1 n = ((pell a1 n).1, (pell a1 n).2) from
    match pell a1 n with
    | (_, _) => rfl

Premises used: Pell.xn, Prod.mk, Prod.fst, Pell.yn, Eq, Prod.snd, rfl, _private.0.Pell.pell_val.match_1, Pell.pell
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ xn a1 0 = 1

Tactic:
rfl

Premises used: Pell.xn, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ yn a1 0 = 0

Tactic:
rfl

Premises used: Pell.yn, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ xn a1 (n + 1) = xn a1 n * a + d a1 * yn a1 n

Tactic:
rfl

Premises used: Pell.xn, Pell.yn, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 (n + 1) = xn a1 n + yn a1 n * a

Tactic:
rfl

Premises used: Pell.xn, Pell.yn, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ xn a1 1 = a

Tactic:
simp
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ yn a1 1 = 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ a * 1 ≤ a * a

Tactic:
have := @Nat.mul_le_mul_left 1 a a (le_of_lt a1)
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
this : a * 1 ≤ a * a
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : a ≤ a * a), a ≤ a * a
⊢ a ≤ a * a

Tactic:
rwa [mul_one] at this

Premises used: mul_one
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
this : 1 ≤ a * a
rw : HSub.hSub (α := ℤ) (↑(a * a) : ℤ) (↑1 : ℤ) = az a * az a - 1
⊢ (↑(d a1) : ℤ) = az a * az a - 1

Tactic:
rw [Pell.d, Int.ofNat_sub this]

Premises used: Int.ofNat_sub, _private.0.Pell.d
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
this : 1 ≤ a * a
⊢ HSub.hSub (α := ℤ) (↑(a * a) : ℤ) (↑1 : ℤ) = az a * az a - 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ xz a1 (n + 1) = xz a1 n * az a + (↑(d a1) : ℤ) * yz a1 n

Tactic:
rfl

Premises used: Pell.xn, Pell.xz, Pell.yn, Int.add, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yz a1 (n + 1) = xz a1 n + yz a1 n * az a

Tactic:
rfl

Premises used: Pell.xn, Pell.yz, Pell.yn, Int.add, rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 n).re = (↑(xn a1 n) : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 n).im = (↑(yn a1 n) : ℤ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell (d := (↑(d a1) : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) }
rw : HSub.hSub (α := ℤ) (↑(x * x) : ℤ) (↑(d a1 * y * y) : ℤ) = (↑1 : ℤ)
⊢ Eq (α := ℤ) (↑(x * x - d a1 * y * y) : ℤ) (↑1 : ℤ)

Tactic:
rw [Int.ofNat_sub (Int.le_of_ofNat_le_ofNat <| Int.le.intro_sub _ h)]

Premises used: Int.ofNat_sub, Int.le_of_ofNat_le_ofNat, Int.le.intro_sub
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell (d := (↑(d a1) : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) }
⊢ HSub.hSub (α := ℤ) (↑(x * x) : ℤ) (↑(d a1 * y * y) : ℤ) = (↑1 : ℤ)

Tactic:
h

Premises used: Int.mul, Pell.IsPell
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
x y : ℕ
h : IsPell (d := (↑(d a1) : ℤ)) { re := (↑x : ℤ), im := (↑y : ℤ) }
⊢ HSub.hSub (α := ℤ) (↑(x * x) : ℤ) (↑(d a1 * y * y) : ℤ) = (↑1 : ℤ)

Tactic:
exact h
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - d a1 * y * y = 1
rw : Eq (α := ℤ) (↑1 : ℤ) 1
⊢ HSub.hSub (α := ℤ) (↑(x * x) : ℤ) (↑(d a1 * y * y) : ℤ) = 1

Tactic:
rw [← Int.ofNat_sub <| le_of_lt <| Nat.lt_of_sub_eq_succ h, h]

Premises used: Int.ofNat_sub, le_of_lt, Nat.lt_of_sub_eq_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
x y : ℕ
h : x * x - d a1 * y * y = 1
⊢ Eq (α := ℤ) (↑1 : ℤ) 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
re : (pellZd a1 (n + 1)).re = (pellZd a1 n * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) }).re
im : (pellZd a1 (n + 1)).im = (pellZd a1 n * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) }).im
⊢ pellZd a1 (n + 1) = pellZd a1 n * { re := (↑a : ℤ), im := 1 }

Tactic:
ext
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 1)).re = (pellZd a1 n * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) }).re

Tactic:
simp
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 1)).im = (pellZd a1 n * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) }).im

Tactic:
simp
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
⊢ az a * az a - HMul.hMul (α := ℤ) (↑(d a1) : ℤ) 1 * 1 = 1

Tactic:
simp [dz_val]

Premises used: Pell.dz_val
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
o : IsPell (d := (↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 } := ⋯
⊢ IsPell (pellZd a1 (n + 1))

Tactic:
simpa using Pell.isPell_mul (isPell_pellZd n) o

Premises used: Pell.isPell_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ xz a1 n * xz a1 n - (↑(d a1) : ℤ) * yz a1 n * yz a1 n = 1

Tactic:
isPell_pellZd a1 n

Premises used: Pell.yz, Pell.xz, Pell.isPell_pellZd, Pell.IsPell
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - (↑(d a1) : ℤ) * yz a1 n * yz a1 n = 1 := ⋯
⊢ HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 n) : ℤ) - (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = 1

Tactic:
pn

Premises used: Pell.xz, Int.mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - (↑(d a1) : ℤ) * yz a1 n * yz a1 n = 1 := ⋯
⊢ HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 n) : ℤ) - (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = 1

Tactic:
exact pn
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - (↑(d a1) : ℤ) * yz a1 n * yz a1 n = 1 := ⋯
repeat' repeat'₁ repeat'₂ repeat'₃ :
  HMul.hMul (α := ℤ) (↑(xn a1 n) : ℤ) (↑(xn a1 n) : ℤ) - (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = 1
⊢ HSub.hSub (α := ℤ) (↑(xn a1 n * xn a1 n) : ℤ) (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = 1

Tactic:
repeat' rw [Int.natCast_mul]; exact pn

Premises used: Int.natCast_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - (↑(d a1) : ℤ) * yz a1 n * yz a1 n = 1 := ⋯
h : HSub.hSub (α := ℤ) (↑(xn a1 n * xn a1 n) : ℤ) (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = 1
hl : d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n
rw : HSub.hSub (α := ℤ) (↑(xn a1 n * xn a1 n) : ℤ) (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = (↑1 : ℤ)
⊢ Eq (α := ℤ) (↑(xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n) : ℤ) (↑1 : ℤ)

Tactic:
rw [Int.ofNat_sub hl]

Premises used: Int.ofNat_sub
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - (↑(d a1) : ℤ) * yz a1 n * yz a1 n = 1 := ⋯
h : HSub.hSub (α := ℤ) (↑(xn a1 n * xn a1 n) : ℤ) (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = 1
hl : d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n
⊢ HSub.hSub (α := ℤ) (↑(xn a1 n * xn a1 n) : ℤ) (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = (↑1 : ℤ)

Tactic:
h
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
pn : xz a1 n * xz a1 n - (↑(d a1) : ℤ) * yz a1 n * yz a1 n = 1 := ⋯
h : HSub.hSub (α := ℤ) (↑(xn a1 n * xn a1 n) : ℤ) (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = 1
hl : d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n
⊢ HSub.hSub (α := ℤ) (↑(xn a1 n * xn a1 n) : ℤ) (↑(d a1 * yn a1 n * yn a1 n) : ℤ) = (↑1 : ℤ)

Tactic:
exact h
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
rw : d a1 + 1 = a * a
⊢ n * n + 1 = a * a

Tactic:
rw [← h]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
⊢ d a1 + 1 = a * a

Tactic:
Nat.succ_pred_eq_of_pos (asq_pos a1)

Premises used: Nat.succ_pred_eq_of_pos, Pell.asq_pos, _private.0.Pell.d, Nat.pred
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
⊢ d a1 + 1 = a * a

Tactic:
exact Nat.succ_pred_eq_of_pos (asq_pos a1)

Premises used: Nat.succ_pred_eq_of_pos, Pell.asq_pos
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
rw : n * n < n * n + 1
⊢ n * n < a * a

Tactic:
rw [← this]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
⊢ n * n < n * n + 1

Tactic:
Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
⊢ n * n < n * n + 1

Tactic:
exact Nat.lt_succ_self _

Premises used: Nat.lt_succ_self
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
na : n < a
rw : (n + 1) * (n + 1) ≤ a * a
⊢ (n + 1) * (n + 1) ≤ n * n + 1

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
h : d a1 = n * n
this : n * n + 1 = a * a
na : n < a
⊢ (n + 1) * (n + 1) ≤ a * a

Tactic:
Nat.mul_self_le_mul_self na

Premises used: Nat.mul_self_le_mul_self