-- 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:
⊢ Dioph fun v => ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3

Tactic:
have proof := D.1 D< D&0 D∧ D&1 D≤ D&3 D∧
    ((D&2 D= D.1 D∧ D&3 D= D.0) D∨
    ((D∃) 4 <| (D∃) 5 <| (D∃) 6 <| (D∃) 7 <| (D∃) 8 <|
    D&7 D* D&7 D- (D&5 D* D&5 D- D.1) D* D&8 D* D&8 D= D.1 D∧
    D&4 D* D&4 D- (D&5 D* D&5 D- D.1) D* D&3 D* D&3 D= D.1 D∧
    D&2 D* D&2 D- (D&0 D* D&0 D- D.1) D* D&1 D* D&1 D= D.1 D∧
    D.1 D< D&0 D∧ (D≡ (D&0) (D.1) (D.4 D* D&8)) D∧ (D≡ (D&0) (D&5) (D&4)) D∧
    D.0 D< D&3 D∧ D&8 D* D&8 D∣ D&3 D∧
    (D≡ (D&2) (D&7) (D&4)) D∧
    (D≡ (D&1) (D&6) (D.4 D* (D&8)))))

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]))))))))}}}}})))
⊢ Dioph fun v => ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3