-- Lean 4 proof step from Mathlib.Computability.EpsilonNFA (goal)
Goal:
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l : List α
a : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l
s : σ
append_singleton :
  (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) →
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁ :
  (∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))) →
    ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₂ append_singleton₃ append_singleton₄ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₅ append_singleton₆ append_singleton₇ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₈ append_singleton₉ append_singleton₁₀ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁₁ append_singleton₁₂ append_singleton₁₃ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₁₄ append_singleton₁₅ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
append_singleton₁₆ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S ∧ ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
append_singleton₁₇ : (w : σ) → s ∈ M.εClosure (M.step w (some a)) → (w_1 : σ) → w_1 ∈ S → w ∈ M.evalFrom {w_1} l → σ
append_singleton₁₈ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S ∧ ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
append_singleton₁₉ : (w : σ) → s ∈ M.εClosure (M.step w (some a)) → (w_1 : σ) → w_1 ∈ S → w ∈ M.evalFrom {w_1} l → σ
append_singleton₂₀ : ∀ (w : σ), s ∈ M.εClosure (M.step w (some a)) → ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S
append_singleton₂₁ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
append_singleton₂₂ : (w : σ) → s ∈ M.εClosure (M.step w (some a)) → (w_1 : σ) → w_1 ∈ S → w ∈ M.evalFrom {w_1} l → σ
append_singleton₂₃ : ∀ (w : σ), s ∈ M.εClosure (M.step w (some a)) → ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → w_1 ∈ S
append_singleton₂₄ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
append_singleton₂₅ : (w : σ) → s ∈ M.εClosure (M.step w (some a)) → (w_1 : σ) → w_1 ∈ S → w ∈ M.evalFrom {w_1} l → σ
append_singleton₂₆ append_singleton₂₇ :
  ∀ (w : σ),
    s ∈ M.εClosure (M.step w (some a)) →
      ∀ w_1 ∈ S, w ∈ M.evalFrom {w_1} l → ∃ t ∈ M.evalFrom {w_1} l, s ∈ M.εClosure (M.step t (some a))
append_singleton₂₈ append_singleton₂₉ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) →
        ∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))
append_singleton₃₀ :
  ∀ w ∈ S,
    ∀ w_1 ∈ M.evalFrom {w} l,
      s ∈ M.εClosure (M.step w_1 (some a)) → (∃ t ∈ S, w_1 ∈ M.evalFrom {t} l) ∧ s ∈ M.εClosure (M.step w_1 (some a))
⊢ (∃ (t : σ), (∃ t_1 ∈ S, t ∈ M.evalFrom {t_1} l) ∧ s ∈ M.εClosure (M.step t (some a))) ↔
    ∃ t ∈ S, ∃ t_1 ∈ M.evalFrom {t} l, s ∈ M.εClosure (M.step t_1 (some a))
have append_singleton₃₁ : (w : σ) → w ∈ S → (w_1 : σ) → w_1 ∈ M.evalFrom {w} l → s ∈ M.εClosure (M.step w_1 (some a)) → σ
Tactic: tauto