Theorem: DFA.toGrammar_lang_eq_lang (FormalSystems/Chomsky/Regular/DFA.lean)

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ Grammar.GeneratedLanguage (toGrammar M) = AcceptedLanguage M
Tactic:
apply Set.ext
State after:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ ∀ (x : Word { x // x ∈ (toGrammar M).Z }), x ∈ Grammar.GeneratedLanguage (toGrammar M) ↔ x ∈ AcceptedLanguage M

State before:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ ∀ (x : Word { x // x ∈ (toGrammar M).Z }), x ∈ Grammar.GeneratedLanguage (toGrammar M) ↔ x ∈ AcceptedLanguage M
Tactic:
intros
State after:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage (toGrammar M) ↔ x✝ ∈ AcceptedLanguage M

State before:
case h
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage (toGrammar M) ↔ x✝ ∈ AcceptedLanguage M
Tactic:
constructor
State after:
case h.mp
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage (toGrammar M) → x✝ ∈ AcceptedLanguage M

case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)

State before:
case h.mp
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage (toGrammar M) → x✝ ∈ AcceptedLanguage M

case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
Tactic:
apply toGrammar_lang_subs_lang
State after:
case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)

State before:
case h.mpr
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
x✝ : Word { x // x ∈ (toGrammar M).Z }
⊢ x✝ ∈ AcceptedLanguage M → x✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
Tactic:
apply lang_subs_toGrammar_lang
State after:
no goals