assumption
case val.d.h_q
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
w : Word { x // x ∈ (toNFA G).Z }
q₀ : { x // x ∈ (toNFA G).Q }
h_q₀✝ : q₀ ∈ {{ val := Sum.inl G.start, property := ⋯ }}
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
h_q₀ : q₀ = { val := Sum.inl G.start, property := ⋯ }
this : ↑q₀ = Sum.inl G.start
⊢ ↑?val.d.q = Sum.inl G.start
no goals