Theorem: RegularGrammar.lang_eq_toNFA_lang (FormalSystems/Chomsky/Regular/NFA.lean)

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
⊢ Grammar.GeneratedLanguage G = NFA.AcceptedLanguage (toNFA G)
Tactic:
apply Set.ext
State after:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
⊢ ∀ (x : Word { x // x ∈ G.Z }), x ∈ Grammar.GeneratedLanguage G ↔ x ∈ NFA.AcceptedLanguage (toNFA G)

State before:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
⊢ ∀ (x : Word { x // x ∈ G.Z }), x ∈ Grammar.GeneratedLanguage G ↔ x ∈ NFA.AcceptedLanguage (toNFA G)
Tactic:
intro
State after:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage G ↔ x✝ ∈ NFA.AcceptedLanguage (toNFA G)

State before:
case h
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage G ↔ x✝ ∈ NFA.AcceptedLanguage (toNFA G)
Tactic:
constructor
State after:
case h.mp
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage G → x✝ ∈ NFA.AcceptedLanguage (toNFA G)

case h.mpr
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ NFA.AcceptedLanguage (toNFA G) → x✝ ∈ Grammar.GeneratedLanguage G

State before:
case h.mp
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ Grammar.GeneratedLanguage G → x✝ ∈ NFA.AcceptedLanguage (toNFA G)

case h.mpr
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ NFA.AcceptedLanguage (toNFA G) → x✝ ∈ Grammar.GeneratedLanguage G
Tactic:
apply RegularGrammar.lang_subs_toNFA_lang
State after:
case h.mpr
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ NFA.AcceptedLanguage (toNFA G) → x✝ ∈ Grammar.GeneratedLanguage G

State before:
case h.mpr
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
x✝ : Word { x // x ∈ G.Z }
⊢ x✝ ∈ NFA.AcceptedLanguage (toNFA G) → x✝ ∈ Grammar.GeneratedLanguage G
Tactic:
apply RegularGrammar.toNFA_lang_subs_lang
State after:
no goals