dsimp [NFA.Run.last, fromNFA] at h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q₀ h✝) ∈ (fromNFA M).F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F