. simp [l, r]; exact l.symm
case h.mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
w' : Word { x // x ∈ (DFA.toTotalDFA M).Z } := w
w_cast : w = w'
x : { x // x ∈ M.Q }
l : ↑({ toFun := fun q => { val := some q, property := ⋯ }, inj' := ⋯ } x) = DFA.del_star M (M.q₀, w')
r : x ∈ M.F
⊢ x ∈ DFA.del_star M (M.q₀, w') ∧ x ∈ M.F
no goals