Universe transfer for finite-type existentials

∃ (σ : Type) (_ : Fintype σ), P σ is the canonical shape of machine-computability classes: states exist at Type 0, and a finite type is equivalent to ULift (Fin n) in any universe. exists_fintype_congr moves such an existential across universes along any equivalence-stable predicate transport, giving each class its universe-polymorphic characterization from a single lemma; exists_fintype₂_congr is the two-type version for machines with a pair of state spaces.

[UPSTREAM] candidate: Mathlib.Computability.DFA, as the shared form of its private Language.isRegular_iff.helper once a second machine-computability class needs it — the two-predicate statement (a universe-polymorphic predicate cannot be abstracted, so each call site passes the same transport at two universe instantiations) makes it pattern infrastructure rather than a Data/Fintype lemma.

theorem exists_fintype_congr {P : Type u → Prop} {Q : Type v → Prop} (hPQ : ∀ {σ : Type u} {τ : Type v} (a : σ ≃ τ), P σ → Q τ) (hQP : ∀ {σ : Type v} {τ : Type u} (a : σ ≃ τ), Q σ → P τ) : (∃ (σ : Type u) (x : Fintype σ), P σ) ↔ ∃ (σ : Type v) (x : Fintype σ), Q σ

Transports a finite-type existential across universes: any finite type is equivalent to a ULift (Fin n) in the target universe, so an equivalence-stable predicate can follow it there.

theorem exists_fintype₂_congr {P : Type u₁ → Type u₂ → Prop} {Q : Type v₁ → Type v₂ → Prop} (hPQ : ∀ {σ₁ : Type u₁} {τ₁ : Type v₁} {σ₂ : Type u₂} {τ₂ : Type v₂} (a : σ₁ ≃ τ₁) (a : σ₂ ≃ τ₂), P σ₁ σ₂ → Q τ₁ τ₂) (hQP : ∀ {σ₁ : Type v₁} {τ₁ : Type u₁} {σ₂ : Type v₂} {τ₂ : Type u₂} (a : σ₁ ≃ τ₁) (a : σ₂ ≃ τ₂), Q σ₁ σ₂ → P τ₁ τ₂) : (∃ (σ₁ : Type u₁) (x : Fintype σ₁) (σ₂ : Type u₂) (x : Fintype σ₂), P σ₁ σ₂) ↔ ∃ (σ₁ : Type v₁) (x : Fintype σ₁) (σ₂ : Type v₂) (x : Fintype σ₂), Q σ₁ σ₂

The two-type version of exists_fintype_congr, for machines with a pair of state spaces.