-- Mathlib/NumberTheory/Dioph.lean
theorem pell_dioph :
    Dioph fun v : Vector3 ℕ 4 => ∃ h : 1 < v &0, xn h (v &1) = v &2 ∧ yn h (v &1) = v &3

Proof state:
proof :
  Dioph
    ({v | const (Fin2 4 → ℕ) 1 v < v &0} ∩
      ({v | v &1 ≤ v &3} ∩
        (((fun v => v &2 = const (Fin2 4 → ℕ) 1 v) ∩ fun v => v &3 = const (Fin2 4 → ℕ) 0 v) ∪
          {v |
            ∃ x,
              (x :: v) ∈
                {v |
                  ∃ x,
                    (x :: v) ∈
                      {v |
                        ∃ x,
                          (x :: v) ∈
                            {v |
                              ∃ x,
                                (x :: v) ∈
                                  {v |
                                    ∃ x,
                                      (x :: v) ∈
                                        (fun v =>
                                            v &7 * v &7 - (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &8 * v &8 =
                                              const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                          ((fun v =>
                                              v &4 * v &4 -
                                                  (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &3 * v &3 =
                                                const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                            ((fun v =>
                                                v &2 * v &2 -
                                                    (v &0 * v &0 - const (Fin2 (succ 8) → ℕ) 1 v) * v &1 * v &1 =
                                                  const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                              ({v | const (Fin2 (succ 8) → ℕ) 1 v < v &0} ∩
                                                ((fun v =>
                                                    v &0 ≡ const (Fin2 (succ 8) → ℕ) 1 v [MOD
                                                      const (Fin2 (succ 8) → ℕ) 4 v * v &8]) ∩
                                                  ((fun v => v &0 ≡ v &5 [MOD v &4]) ∩
                                                    ({v | const (Fin2 (succ 8) → ℕ) 0 v < v &3} ∩
                                                      ((fun v => v &8 * v &8 ∣ v &3) ∩
                                                        ((fun v => v &2 ≡ v &7 [MOD v &4]) ∩ fun v =>
                                                          v &1 ≡ v &6 [MOD
                                                            const (Fin2 (succ 8) → ℕ) 4 v * v &8]))))))))}}}}})))
⊢ Dioph fun v => ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3

Tactic:
have : Dioph {v : Vector3 ℕ 4 |
  1 < v &0 ∧ v &1 ≤ v &3 ∧
  (v &2 = 1 ∧ v &3 = 0 ∨
  ∃ u w s t b : ℕ,
    v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
    u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
    s * s - (b * b - 1) * t * t = 1 ∧
    1 < b ∧ b ≡ 1 [MOD 4 * v &3] ∧ b ≡ v &0 [MOD u] ∧
    0 < w ∧ v &3 * v &3 ∣ w ∧
    s ≡ v &2 [MOD u] ∧
    t ≡ v &1 [MOD 4 * v &3])} := by
  exact proof

Result:
proof :
  Dioph
    ({v | const (Fin2 4 → ℕ) 1 v < v &0} ∩
      ({v | v &1 ≤ v &3} ∩
        (((fun v => v &2 = const (Fin2 4 → ℕ) 1 v) ∩ fun v => v &3 = const (Fin2 4 → ℕ) 0 v) ∪
          {v |
            ∃ x,
              (x :: v) ∈
                {v |
                  ∃ x,
                    (x :: v) ∈
                      {v |
                        ∃ x,
                          (x :: v) ∈
                            {v |
                              ∃ x,
                                (x :: v) ∈
                                  {v |
                                    ∃ x,
                                      (x :: v) ∈
                                        (fun v =>
                                            v &7 * v &7 - (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &8 * v &8 =
                                              const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                          ((fun v =>
                                              v &4 * v &4 -
                                                  (v &5 * v &5 - const (Fin2 (succ 8) → ℕ) 1 v) * v &3 * v &3 =
                                                const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                            ((fun v =>
                                                v &2 * v &2 -
                                                    (v &0 * v &0 - const (Fin2 (succ 8) → ℕ) 1 v) * v &1 * v &1 =
                                                  const (Fin2 (succ 8) → ℕ) 1 v) ∩
                                              ({v | const (Fin2 (succ 8) → ℕ) 1 v < v &0} ∩
                                                ((fun v =>
                                                    v &0 ≡ const (Fin2 (succ 8) → ℕ) 1 v [MOD
                                                      const (Fin2 (succ 8) → ℕ) 4 v * v &8]) ∩
                                                  ((fun v => v &0 ≡ v &5 [MOD v &4]) ∩
                                                    ({v | const (Fin2 (succ 8) → ℕ) 0 v < v &3} ∩
                                                      ((fun v => v &8 * v &8 ∣ v &3) ∩
                                                        ((fun v => v &2 ≡ v &7 [MOD v &4]) ∩ fun v =>
                                                          v &1 ≡ v &6 [MOD
                                                            const (Fin2 (succ 8) → ℕ) 4 v * v &8]))))))))}}}}})))
this :
  Dioph
    {v |
      1 < v &0 ∧
        v &1 ≤ v &3 ∧
          (v &2 = 1 ∧ v &3 = 0 ∨
            ∃ u w s t b,
              v &2 * v &2 - (v &0 * v &0 - 1) * v &3 * v &3 = 1 ∧
                u * u - (v &0 * v &0 - 1) * w * w = 1 ∧
                  s * s - (b * b - 1) * t * t = 1 ∧
                    1 < b ∧
                      b ≡ 1 [MOD 4 * v &3] ∧
                        b ≡ v &0 [MOD u] ∧ 0 < w ∧ v &3 * v &3 ∣ w ∧ s ≡ v &2 [MOD u] ∧ t ≡ v &1 [MOD 4 * v &3])}
⊢ Dioph fun v => ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3