-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xy_modEq_yn (n) :
    ∀ k, xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2] ∧ yn a1 (n * k) ≡
        k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
  | 0 => by constructor <;> simpa using Nat.ModEq.refl _
  | k + 1 => by
    let ⟨hx, hy⟩ := xy_modEq_yn n k
    have L : xn a1 (n * k) * xn a1 n + d a1 * yn a1 (n * k) * yn a1 n ≡
        xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2] :=
      (hx.mul_right _).add <|
        modEq_zero_iff_dvd.2 <| by
          rw [_root_.pow_succ]
          exact
            mul_dvd_mul_right
              (dvd_mul_of_dvd_right
                (modEq_zero_iff_dvd.1 <|
                  (hy.of_dvd <| by simp [_root_.pow_succ]).trans <|
                    modEq_zero_iff_dvd.2 <| by simp)
                _) _
    have R : xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡
        xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3] :=
      ModEq.add
          (by
            rw [_root_.pow_succ]
            exact hx.mul_right' _) <| by
        have : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
⊢ k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n

Tactic:
rcases k with - | k <;> simp [_root_.pow_succ]

Result:
case succ
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2]
hy : yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]
L :
  xn a1 (n * (k + 1)) * xn a1 n + Pell.d a1 * yn a1 (n * (k + 1)) * yn a1 n ≡ xn a1 n ^ (k + 1) * xn a1 n + 0 [MOD
    yn a1 n ^ 2]
⊢ (k + 1) * xn a1 n ^ k * yn a1 n * xn a1 n = (k + 1) * (xn a1 n ^ k * xn a1 n) * yn a1 n

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧
    yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
let ⟨hx, hy⟩ := xy_modEq_yn n k

Result:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧
    yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
R :
  xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    yn a1 n ^ 3]
⊢ xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2] ∧
    yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
rw [add_tsub_cancel_right, Nat.mul_succ, xn_add, yn_add, pow_succ (xn _ n), Nat.succ_mul,
  add_comm (k * xn _ n ^ k) (xn _ n ^ k), right_distrib]

Result:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
R :
  xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
    yn a1 n ^ 3]
⊢ xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n [MOD yn a1 n ^ 2] ∧
    xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n ≡ xn a1 n ^ k * yn a1 n + k * xn a1 n ^ k * yn a1 n [MOD
      yn a1 n ^ 3]

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
⊢ xn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 2 * yn a1 n]

Tactic:
exact hx.mul_right' _

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
this : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ k * yn a1 n [MOD yn a1 n ^ 3]

Tactic:
rw [← this]

Result:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
L : xn a1 (n * k) * xn a1 n + Pell.d a1 * yn a1 (n * k) * yn a1 n ≡ xn a1 n ^ k * xn a1 n + 0 [MOD yn a1 n ^ 2]
this : k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n = k * xn a1 n ^ k * yn a1 n
⊢ yn a1 (n * k) * xn a1 n ≡ k * xn a1 n ^ (k - 1) * yn a1 n * xn a1 n [MOD yn a1 n ^ 3]

Proof state:
case succ
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2]
hy : yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]
L :
  xn a1 (n * (k + 1)) * xn a1 n + Pell.d a1 * yn a1 (n * (k + 1)) * yn a1 n ≡ xn a1 n ^ (k + 1) * xn a1 n + 0 [MOD
    yn a1 n ^ 2]
⊢ (k + 1) * xn a1 n ^ k * yn a1 n * xn a1 n = (k + 1) * (xn a1 n ^ k * xn a1 n) * yn a1 n

Tactic:
ring_nf

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * k) ≡ xn a1 n ^ k [MOD yn a1 n ^ 2]
hy : yn a1 (n * k) ≡ k * xn a1 n ^ (k - 1) * yn a1 n [MOD yn a1 n ^ 3]
⊢ yn a1 n ^ 1 ∣ yn a1 n ^ 3

Tactic:
simp [_root_.pow_succ]

Result:
no goals