-- Module: Mathlib.Computability.NFA
Goal:
α : Type u
σ : Type v
M : NFA α σ
x : List α
mp : (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr : (∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x) → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₁ mp₂ mp₃ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₁ mpr₂ mpr₃ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₄ mp₅ mp₆ :
  ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mpr₄ mpr₅ mpr₆ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mp₇ mp₈ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x
mp₉ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₀ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₁ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start ∧ ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₂ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₃ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
mp₁₄ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₅ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₆ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → w_1 ∈ M.start
mp₁₇ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mp₁₈ : (w : σ) → w ∈ M.accept → (w_1 : σ) → w_1 ∈ M.start → w ∈ M.evalFrom {w_1} x → σ
mp₁₉ mp₂₀ : ∀ w ∈ M.accept, ∀ w_1 ∈ M.start, w ∈ M.evalFrom {w_1} x → ∃ t ∈ M.accept, t ∈ M.evalFrom {w_1} x
mpr₇ mpr₈ :
  ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x
mpr₉ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept ∧ ∃ t ∈ M.start, w_1 ∈ M.evalFrom {t} x
mpr₁₀ : (w : σ) → w ∈ M.start → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom {w} x → σ
mpr₁₁ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept ∧ ∃ t ∈ M.start, w_1 ∈ M.evalFrom {t} x
mpr₁₂ : (w : σ) → w ∈ M.start → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom {w} x → σ
mpr₁₃ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept
mpr₁₄ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ t ∈ M.start, w_1 ∈ M.evalFrom {t} x
mpr₁₅ : (w : σ) → w ∈ M.start → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom {w} x → σ
mpr₁₆ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → w_1 ∈ M.accept
mpr₁₇ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ t ∈ M.start, w_1 ∈ M.evalFrom {t} x
mpr₁₈ : (w : σ) → w ∈ M.start → (w_1 : σ) → w_1 ∈ M.accept → w_1 ∈ M.evalFrom {w} x → σ
mpr₁₉ mpr₂₀ : ∀ w ∈ M.start, ∀ w_1 ∈ M.accept, w_1 ∈ M.evalFrom {w} x → ∃ t ∈ M.start, w_1 ∈ M.evalFrom {t} x
⊢ (∃ S ∈ M.accept, ∃ t ∈ M.start, S ∈ M.evalFrom {t} x) ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, t ∈ M.evalFrom {s} x

Tactic:
tauto