-- Mathlib/NumberTheory/Dioph.lean
theorem pow_dioph {f g : (α → ℕ) → ℕ} (df : DiophFn f) (dg : DiophFn g) :
    DiophFn fun v => f v ^ g v

Proof state:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
proof :
  Dioph
    (((fun v => v &2 = const (Fin2 3 → ℕ) 0 v) ∩ fun v => v &0 = const (Fin2 3 → ℕ) 1 v) ∪
      {v | const (Fin2 3 → ℕ) 0 v < v &2} ∩
        (((fun v => v &1 = const (Fin2 3 → ℕ) 0 v) ∩ fun v => v &0 = const (Fin2 3 → ℕ) 0 v) ∪
          {v | const (Fin2 3 → ℕ) 0 v < v &1} ∩
            {v |
              ∃ x,
                (x :: v) ∈
                  {v |
                    ∃ x,
                      (x :: v) ∈
                        {v |
                          ∃ x,
                            (x :: v) ∈
                              {v |
                                ∃ x,
                                  (x :: v) ∈
                                    {v |
                                      ∃ x,
                                        (x :: v) ∈
                                          {v |
                                            ∃ x,
                                              (x :: v) ∈
                                                {v |
                                                    (v ∘ &4 :: &8 :: &1 :: &0 :: []) ∈ fun v =>
                                                      ∃ (h : 1 < v &0), xn h (v &1) = v &2 ∧ yn h (v &1) = v &3} ∩
                                                  ((fun v => v &1 ≡ v &0 * (v &4 - v &7) + v &6 [MOD v &3]) ∩
                                                    ((fun v =>
                                                        const (Fin2 (succ 8) → ℕ) 2 v * v &4 * v &7 =
                                                          v &3 + (v &7 * v &7 + const (Fin2 (succ 8) → ℕ) 1 v)) ∩
                                                      ({v | v &6 < v &3} ∩
                                                        ({v | v &7 ≤ v &5} ∩
                                                          ({v | v &8 ≤ v &5} ∩ fun v =>
                                                            v &4 * v &4 -
                                                                ((v &5 + const (Fin2 (succ 8) → ℕ) 1 v) *
                                                                        (v &5 + const (Fin2 (succ 8) → ℕ) 1 v) -
                                                                      const (Fin2 (succ 8) → ℕ) 1 v) *
                                                                    (v &5 * v &2) *
                                                                  (v &5 * v &2) =
                                                              const (Fin2 (succ 8) → ℕ) 1 v)))))}}}}}}))
this :
  Dioph
    {v |
      v &2 = 0 ∧ v &0 = 1 ∨
        0 < v &2 ∧
          (v &1 = 0 ∧ v &0 = 0 ∨
            0 < v &1 ∧
              ∃ w a t z x y,
                (∃ (a1 : 1 < a), xn a1 (v &2) = x ∧ yn a1 (v &2) = y) ∧
                  x ≡ y * (a - v &1) + v &0 [MOD t] ∧
                    2 * a * v &1 = t + (v &1 * v &1 + 1) ∧
                      v &0 < t ∧ v &1 ≤ w ∧ v &2 ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)}
⊢ DiophFn fun v => f v ^ g v

Tactic:
exact diophFn_comp2 df dg <| (diophFn_vec _).2 <| Dioph.ext this fun v => Iff.symm <|
  eq_pow_of_pell.trans <| or_congr Iff.rfl <| and_congr Iff.rfl <| or_congr Iff.rfl <|
     and_congr Iff.rfl <|
      ⟨fun ⟨w, a, t, z, a1, h⟩ => ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩,
      fun ⟨w, a, t, z, _, _, ⟨a1, rfl, rfl⟩, h⟩ => ⟨w, a, t, z, a1, h⟩⟩

Result:
no goals