Theorem: final_state_eq (FormalSystems/Chomsky/Regular/Nerode.lean)

State before:
α✝ : Type ?u.29550
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
w : Word { x // x ∈ (canonicalAutomaton nc).Z }
⊢ ↑(TotalDFA.del_star' (canonicalAutomaton nc) ({ val := ⟦ε⟧, property := ⋯ }, w)) = ↑{ val := ⟦w⟧, property := ⋯ }
Tactic:
simp [del_star_eq]
State after:
no goals