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

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
⊢ AcceptedLanguage M ⊆ Grammar.GeneratedLanguage (toGrammar M)
Tactic:
intro _ ⟨ run, h ⟩
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ M.Z }
run : Run M M.q₀ a✝
h : NFA.Run.last run ∈ M.F
⊢ a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ M.Z }
run : Run M M.q₀ a✝
h : NFA.Run.last run ∈ M.F
⊢ a✝ ∈ Grammar.GeneratedLanguage (toGrammar M)
Tactic:
constructor
State after:
case val
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ M.Z }
run : Run M M.q₀ a✝
h : NFA.Run.last run ∈ M.F
⊢ Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)

State before:
case val
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
a✝ : Word { x // x ∈ M.Z }
run : Run M M.q₀ a✝
h : NFA.Run.last run ∈ M.F
⊢ Grammar.Derivation (toGrammar M) [Sum.inl (toGrammar M).start] (Sum.inr <$> a✝)
Tactic:
exact run.toDerivation _ h
State after:
no goals