-- Module: Mathlib.Computability.EpsilonNFA
Goal:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
s₂ : σ
left : s₂ ∈ M.accept
s₁ : σ
left_1 : s₁ ∈ M.start
h : ∃ (x' : List (Option α)), x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)),
          s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₁ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₂ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
w₁ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₃ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₄ w₂ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₅ :
  ∀ (w : List (Option α)),
    w.reduceOption = x →
      M.IsPath s₁ s₂ w →
        ∃ (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
h₆ w₃ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₇ :
  ∀ (w : List (Option α)),
    w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₈ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₉ w₄ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₁₀ :
  ∀ (w : List (Option α)),
    w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₁₁ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₁₂ w₅ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₁₃ : ∀ (w : List (Option α)), w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start
h₁₄ :
  ∀ (w : List (Option α)), w.reduceOption = x → M.IsPath s₁ s₂ w → s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₁₅ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₁₆ w₆ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₁₇ : ∀ (w : List (Option α)), w.reduceOption = x → M.IsPath s₁ s₂ w → s₁ ∈ M.start
h₁₈ :
  ∀ (w : List (Option α)), w.reduceOption = x → M.IsPath s₁ s₂ w → s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₁₉ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₂₀ w₇ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₂₁ :
  ∀ (w : List (Option α)), w.reduceOption = x → M.IsPath s₁ s₂ w → s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₂₂ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₂₃ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
h₂₄ :
  ∀ (w : List (Option α)), w.reduceOption = x → M.IsPath s₁ s₂ w → s₂ ∈ M.accept ∧ w.reduceOption = x ∧ M.IsPath s₁ s₂ w
h₂₅ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → List (Option α)
h₂₆ : (w : List (Option α)) → w.reduceOption = x → M.IsPath s₁ s₂ w → σ
⊢ ∃ (s₁ : σ) (s₂ : σ) (x' : List (Option α)), s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'

Tactic:
tauto