-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem pellZd_succ_succ (n) :
    pellZd a1 (n + 2) + pellZd a1 n = (2 * a : ℕ) * pellZd a1 (n + 1)

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := Zsqrtd.re 1 + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).re,
      im := Zsqrtd.im 1 + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).im } =
    {
      re :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).re +
          ↑(Pell.d a1) * { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).im,
      im :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).im +
          { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).re }

Tactic:
rw [dz_val]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := Zsqrtd.re 1 + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).re,
      im := Zsqrtd.im 1 + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).im } =
    {
      re :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).re +
          (az a * az a - 1) * { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).im,
      im :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).im +
          { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).re }

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := Zsqrtd.re 1 + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).re,
      im := Zsqrtd.im 1 + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).im } =
    {
      re :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).re +
          (az a * az a - 1) * { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).im,
      im :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).im +
          { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).re }

Tactic:
dsimp [az]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1), im := 0 + (↑a * 1 + 1 * ↑a) } =
    { re := ↑a * (2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (0 + 0 * ↑a),
      im := ↑a * (0 + 0 * ↑a) + 1 * (2 * ↑a + (↑a * ↑a - 1) * 0 * 0) }

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 1 + { re := ↑a, im := 1 } * { re := ↑a, im := 1 } = { re := ↑a, im := 1 } * (2 * { re := ↑a, im := 0 })

Tactic:
change (⟨_, _⟩ : ℤ√(d a1)) = ⟨_, _⟩

Result:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := Zsqrtd.re 1 + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).re,
      im := Zsqrtd.im 1 + ({ re := ↑a, im := 1 } * { re := ↑a, im := 1 }).im } =
    {
      re :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).re +
          ↑(Pell.d a1) * { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).im,
      im :=
        { re := ↑a, im := 1 }.re * (2 * { re := ↑a, im := 0 }).im +
          { re := ↑a, im := 1 }.im * (2 * { re := ↑a, im := 0 }).re }

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 1 + { re := ↑a, im := 1 } * { re := ↑a, im := 1 } = { re := ↑a, im := 1 } * (2 * ↑a)

Tactic:
rw [Zsqrtd.natCast_val]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 1 + { re := ↑a, im := 1 } * { re := ↑a, im := 1 } = { re := ↑a, im := 1 } * (2 * { re := ↑a, im := 0 })

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ { re := 1 + (↑a * ↑a + (↑a * ↑a - 1) * 1 * 1), im := 0 + (↑a * 1 + 1 * ↑a) } =
    { re := ↑a * (2 * ↑a + (↑a * ↑a - 1) * 0 * 0) + (↑a * ↑a - 1) * 1 * (0 + 0 * ↑a),
      im := ↑a * (0 + 0 * ↑a) + 1 * (2 * ↑a + (↑a * ↑a - 1) * 0 * 0) }

Tactic:
ext <;> dsimp <;> ring_nf

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)

Tactic:
have : (1 : ℤ√(d a1)) + ⟨a, 1⟩ * ⟨a, 1⟩ = ⟨a, 1⟩ * (2 * a) := by
  rw [Zsqrtd.natCast_val]
  change (⟨_, _⟩ : ℤ√(d a1)) = ⟨_, _⟩
  rw [dz_val]
  dsimp [az]
  ext <;> dsimp <;> ring_nf

Result:
a : ℕ
a1 : 1 < a
n : ℕ
this : 1 + { re := ↑a, im := 1 } * { re := ↑a, im := 1 } = { re := ↑a, im := 1 } * (2 * ↑a)
⊢ pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)