Theorem: DFA.Run.fromDerivation_result (FormalSystems/Chomsky/Regular/DFA.lean)

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
d : RegularGrammar.RegularDerivation (toGrammar M) s w
⊢ NFA.Run.last (fromDerivation M d) ∈ M.F
Tactic:
cases d
State after:
case eps
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w✝ : w = ε
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v✝ h_w✝)) ∈ M.F

case alpha
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝ : { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.alpha s a✝ ∈ (toGrammar M).productions
h_w✝ : w = [a✝]
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.alpha s h_v✝ h_w✝)) ∈ M.F

case step
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w✝ : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.step s v'✝ h✝ h_w✝ a✝)) ∈ M.F

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v h_w)) ∈ M.F
Tactic:
case eps h_v h_w =>
  simp [toGrammar, transitionToRule] at h_v
  simp [fromDerivation, NFA.Run.last]
  assumption
State after:
no goals

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝ : { x // x ∈ (toGrammar M).Z }
h_v : RegularProduction.alpha s a✝ ∈ (toGrammar M).productions
h_w✝ : w = [a✝]
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.alpha s h_v h_w✝)) ∈ M.F
Tactic:
case alpha h_v _ =>
  simp [toGrammar, transitionToRule] at h_v
State after:
no goals

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.step s v'✝ h✝ h_w a✝)) ∈ M.F
Tactic:
case step h_w =>
  simp [fromDerivation, NFA.Run.last]
  apply fromDerivation_result
State after:
no goals

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v h_w)) ∈ M.F
Tactic:
simp [toGrammar, transitionToRule] at h_v
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
h_v : s ∈ M.F
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v✝ h_w)) ∈ M.F

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
h_v : s ∈ M.F
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.eps s h_v✝ h_w)) ∈ M.F
Tactic:
simp [fromDerivation, NFA.Run.last]
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
h_v : s ∈ M.F
⊢ s ∈ M.F

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
h_v✝ : RegularProduction.eps s ∈ (toGrammar M).productions
h_w : w = ε
h_v : s ∈ M.F
⊢ s ∈ M.F
Tactic:
assumption
State after:
no goals

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝ : { x // x ∈ (toGrammar M).Z }
h_v : RegularProduction.alpha s a✝ ∈ (toGrammar M).productions
h_w✝ : w = [a✝]
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.alpha s h_v h_w✝)) ∈ M.F
Tactic:
simp [toGrammar, transitionToRule] at h_v
State after:
no goals

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M (RegularGrammar.RegularDerivation.step s v'✝ h✝ h_w a✝)) ∈ M.F
Tactic:
simp [fromDerivation, NFA.Run.last]
State after:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M a✝) ∈ M.F

State before:
α qs : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : DFA α qs
s : { x // x ∈ (toGrammar M).V }
w : Word { x // x ∈ (toGrammar M).Z }
a✝¹ : { x // x ∈ (toGrammar M).Z }
w'✝ : List { x // x ∈ (toGrammar M).Z }
v'✝ : { x // x ∈ (toGrammar M).V }
a✝ : RegularGrammar.RegularDerivation (toGrammar M) v'✝ w'✝
h✝ : RegularProduction.cons s (a✝¹, v'✝) ∈ (toGrammar M).productions
h_w : w = a✝¹ :: w'✝
⊢ NFA.Run.last (fromDerivation M a✝) ∈ M.F
Tactic:
apply fromDerivation_result
State after:
no goals