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

State before:
α qs : Type
M : DFA α qs
⊢ AcceptedLanguage M = NFA.AcceptedLanguage (toNFA M)
Tactic:
unfold AcceptedLanguage
State after:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = NFA.AcceptedLanguage (toNFA M)

State before:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = NFA.AcceptedLanguage (toNFA M)
Tactic:
unfold toNFA
State after:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) =
    NFA.AcceptedLanguage { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }

State before:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) =
    NFA.AcceptedLanguage { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }
Tactic:
unfold NFA.AcceptedLanguage
State after:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = fun w =>
    ∃ q₀ ∈ { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }.Q₀,
      ∃ run, NFA.Run.last run ∈ { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }.F

State before:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = fun w =>
    ∃ q₀ ∈ { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }.Q₀,
      ∃ run, NFA.Run.last run ∈ { Z := M.Z, Q := M.Q, δ := Option.toFinset ∘ M.δ, Q₀ := {M.q₀}, F := M.F }.F
Tactic:
simp
State after:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = fun w => ∃ run, NFA.Run.last run ∈ M.F

State before:
α qs : Type
M : DFA α qs
⊢ (fun w => ∃ run, NFA.Run.last run ∈ M.F) = fun w => ∃ run, NFA.Run.last run ∈ M.F
Tactic:
rfl
State after:
no goals