assumption
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
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last (NFA.Run.step x right✝ r' h✝) ∈ M.F
no goals