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

State before:
α✝ : Type ?u.47152
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
⊢ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA = L
Tactic:
apply Set.ext
State after:
case h
α✝ : Type ?u.47152
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
⊢ ∀ (x : Word { x // x ∈ (canonicalAutomaton nc).Z }), x ∈ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA ↔ x ∈ L

State before:
case h
α✝ : Type ?u.47152
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
⊢ ∀ (x : Word { x // x ∈ (canonicalAutomaton nc).Z }), x ∈ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA ↔ x ∈ L
Tactic:
intro w
State after:
case h
α✝ : Type ?u.47152
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 }
⊢ w ∈ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA ↔ w ∈ L

State before:
case h
α✝ : Type ?u.47152
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 }
⊢ w ∈ DFA.AcceptedLanguage (canonicalAutomaton nc).toDFA ↔ w ∈ L
Tactic:
rw [TotalDFA.in_language_iff_del_star_final, final_state_accepts_iff]
State after:
no goals