. dsimp [toNFA] at h_q₀
  simp at h_q₀
  have := congrArg Subtype.val h_q₀
  simp at this
  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₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ ↑?val.d.q = Sum.inl G.start

case val.d.hlast
α 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₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run.last ?val.d.run ∈ (toNFA G).F

case val.d.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₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ { x // x ∈ (toNFA G).Q }

case val.d.run
α 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₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run (toNFA G) ?val.d.q w
case val.d.hlast
α 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₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run.last ?val.d.run ∈ (toNFA G).F

case val.d.run
α 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₀ ∈ (toNFA G).Q₀
r : NFA.Run (toNFA G) q₀ w
hr : NFA.Run.last r ∈ (toNFA G).F
⊢ NFA.Run (toNFA G) q₀ w