-- Mathlib/NumberTheory/Pell.lean
theorem eq_zpow_or_neg_zpow {a₁ : Solution₁ d} (h : IsFundamental a₁) (a : Solution₁ d) :
    ∃ n : ℤ, a = a₁ ^ n ∨ a = -a₁ ^ n

Proof state:
case intro.intro.intro.intro.inr.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, b⁻¹ = a₁ ^ n ∨ b⁻¹ = -a₁ ^ n

Tactic:
exact ⟨-n, Or.inl (by simp [hn])⟩

Result:
no goals

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ -b = -a₁ ^ ↑n

Tactic:
simp [hn]

Result:
no goals

Proof state:
case intro.intro.intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
hb : a ∈ {b, b⁻¹, -b, -b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
obtain ⟨n, hn⟩ := h.eq_pow_of_nonneg hbx hby

Result:
case intro.intro.intro.intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
hb : a ∈ {b, b⁻¹, -b, -b⁻¹}
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Proof state:
case intro.intro.intro.intro.inr.inr.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, -b = a₁ ^ n ∨ -b = -a₁ ^ n

Tactic:
exact ⟨n, Or.inr (by simp [hn])⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
n : ℕ
hbx : 0 < a.x
hby : 0 ≤ a.y
hn : a = a₁ ^ n
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
exact ⟨n, Or.inl (mod_cast hn)⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
hb : a ∈ {b, b⁻¹, -b, -b⁻¹}
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
rcases hb with (rfl | rfl | rfl | hb)

Result:
case intro.intro.intro.intro.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
n : ℕ
hbx : 0 < a.x
hby : 0 ≤ a.y
hn : a = a₁ ^ n
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

case intro.intro.intro.intro.inr.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, b⁻¹ = a₁ ^ n ∨ b⁻¹ = -a₁ ^ n

case intro.intro.intro.intro.inr.inr.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, -b = a₁ ^ n ∨ -b = -a₁ ^ n

case intro.intro.intro.intro.inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a ∈ {-b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Proof state:
case intro.intro.intro.intro.inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a ∈ {-b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
rw [Set.mem_singleton_iff] at hb

Result:
case intro.intro.intro.intro.inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ -b⁻¹ = -a₁ ^ (-↑n)

Tactic:
simp [hn]

Result:
no goals

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
obtain ⟨b, hbx, hby, hb⟩ := exists_pos_variant h.d_pos a

Result:
case intro.intro.intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
hb : a ∈ {b, b⁻¹, -b, -b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Proof state:
case intro.intro.intro.intro.inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
rw [hb]

Result:
case intro.intro.intro.intro.inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ ∃ n, -b⁻¹ = a₁ ^ n ∨ -b⁻¹ = -a₁ ^ n

Proof state:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ b⁻¹ = a₁ ^ (-↑n)

Tactic:
simp [hn]

Result:
no goals

Proof state:
case intro.intro.intro.intro.inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ ∃ n, -b⁻¹ = a₁ ^ n ∨ -b⁻¹ = -a₁ ^ n

Tactic:
exact ⟨-n, Or.inr (by simp [hn])⟩

Result:
no goals