-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_pow_of_pell {m n k} :
    n ^ k = m ↔ k = 0 ∧ m = 1 ∨0 < k ∧ (n = 0 ∧ m = 0 ∨
      0 < n ∧ ∃ (w a t z : ℕ) (a1 : 1 < a), xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
      2 * a * n = t + (n * n + 1) ∧ m < t ∧
      n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)

Proof state:
case mpr
m n k : ℕ
⊢ k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ w a t z,
              ∃ (a1 : 1 < a),
                xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                  2 * a * n = t + (n * n + 1) ∧
                    m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1) →
    n ^ k = m

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨hk0, ⟨rfl, rfl⟩ | ⟨hn0, w, a, t, z, a1, tm, ta, mt, nw, kw, zp⟩⟩)

Result:
case mpr.inl.intro
n : ℕ
⊢ n ^ 0 = 1

case mpr.inr.intro.inl.intro
k : ℕ
hk0 : 0 < k
⊢ 0 ^ k = 0

case mpr.inr.intro.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w a t z : ℕ
a1 : 1 < a
tm : xn a1 k ≡ yn a1 k * (a - n) + m [MOD t]
ta : 2 * a * n = t + (n * n + 1)
mt : m < t
nw : n ≤ w
kw : k ≤ w
zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ n ^ k = m

Proof state:
case mpr.inl.intro
n : ℕ
⊢ n ^ 0 = 1

Tactic:
exact _root_.pow_zero n

Result:
no goals

Proof state:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := n ⊔ k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
t : ℕ
te : ↑t = 2 * ↑a * ↑n - ↑n * ↑n - 1
nt✝ nt : ↑(n ^ k) < ↑t
tm : x ≡ y * (a - n) + n ^ k [MOD t]
⊢ 2 * a * n = t + (n * n + 1)

Tactic:
zify

Result:
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := n ⊔ k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
z : ℕ
ze : yn w1 w = w * z
t : ℕ
te : ↑t = 2 * ↑a * ↑n - ↑n * ↑n - 1
nt✝ nt : ↑(n ^ k) < ↑t
tm : x ≡ y * (a - n) + n ^ k [MOD t]
⊢ 2 * ↑a * ↑n = ↑t + (↑n * ↑n + 1)

Proof state:
case mpr.inr.intro.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ n ^ k = m

Tactic:
have hj0 : 0 < j := by
  apply Nat.pos_of_ne_zero
  rintro rfl
  exact lt_irrefl 1 a1

Result:
case mpr.inr.intro.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
⊢ n ^ k = m

Proof state:
case mp
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := n ⊔ k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
⊢ ∃ w a t z,
    ∃ (a1 : 1 < a),
      xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
        2 * a * n = t + (n * n + 1) ∧
          n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1

Tactic:
have na : n ≤ a := nw.trans (n_lt_xn w1 w).le

Result:
case mp
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := n ⊔ k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
⊢ ∃ w a t z,
    ∃ (a1 : 1 < a),
      xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
        2 * a * n = t + (n * n + 1) ∧
          n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1

Proof state:
case mpr.inr.intro.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
this✝ : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
this : n ^ k % t = m % t
⊢ n ^ k = m

Tactic:
rw [← te] at nt

Result:
case mpr.inr.intro.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < ↑t
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
this✝ : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]
this : n ^ k % t = m % t
⊢ n ^ k = m

Proof state:
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ xn a1 k ≡ yn a1 k * (xn hw1 j - n) + n ^ k [MOD t]

Tactic:
apply modEq_of_dvd

Result:
case a
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hj0 : 0 < j
wj : w ≤ j
hnka : n ^ k < xn hw1 j
nt : ↑(n ^ k) < 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
na : n ≤ xn hw1 j
te : ↑t = 2 * ↑(xn hw1 j) * ↑n - ↑n * ↑n - 1
⊢ ↑t ∣ ↑(yn a1 k * (xn hw1 j - n) + n ^ k) - ↑(xn a1 k)

Proof state:
case mp
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := n ⊔ k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
⊢ ∃ w a t z,
    ∃ (a1 : 1 < a),
      xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
        2 * a * n = t + (n * n + 1) ∧
          n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1

Tactic:
set y := yn a1 k

Result:
case mp
n k : ℕ
hk : 0 < k
hn : 0 < n
w : ℕ := n ⊔ k
nw : n ≤ w
kw : k ≤ w
wpos : 0 < w
w1 : 1 < w + 1
a : ℕ := xn w1 w
a1 : 1 < a
na : n ≤ a
x : ℕ := xn a1 k
y : ℕ := yn a1 k
⊢ ∃ w a t z,
    ∃ (a1 : 1 < a),
      xn a1 k ≡ yn a1 k * (a - n) + n ^ k [MOD t] ∧
        2 * a * n = t + (n * n + 1) ∧
          n ^ k < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1