apply Exists.intro
case right
α 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)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ r', NFA.Run.last r' ∈ M.F
case right.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 : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run.last ?right.w ∈ M.F

case right.w
α 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)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run M qf w