Theorem: NFA.Run.fromDerivation_last_in_final (FormalSystems/Chomsky/Regular/NFA.lean)

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
⊢ last (fromDerivation G d) ∈ (toNFA G).F
Tactic:
match d with
| .eps (v:=v) _ _ =>
  simp [last, toNFA]
  exists .eps v
| .alpha _ _ _ =>
  simp [last, fromDerivation, Fintype.wrap, toNFA]
| .step _ _ _ _ _ =>
  simp [last]
  apply fromDerivation_last_in_final
State after:
no goals

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
v : { x // x ∈ G.V }
h_v✝ : RegularProduction.eps v ∈ G.productions
h_w✝ : w✝ = ε
⊢ last (fromDerivation G (RegularDerivation.eps v h_v✝ h_w✝)) ∈ (toNFA G).F
Tactic:
simp [last, toNFA]
State after:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
v : { x // x ∈ G.V }
h_v✝ : RegularProduction.eps v ∈ G.productions
h_w✝ : w✝ = ε
⊢ ∃ a,
    (a ∈ G.productions ∧ RegularProduction.isEps a) ∧
      Fintype.wrap (Sum.inl (RegularProduction.lhs a)) = { val := Sum.inl v, property := ⋯ }

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
v : { x // x ∈ G.V }
h_v✝ : RegularProduction.eps v ∈ G.productions
h_w✝ : w✝ = ε
⊢ ∃ a,
    (a ∈ G.productions ∧ RegularProduction.isEps a) ∧
      Fintype.wrap (Sum.inl (RegularProduction.lhs a)) = { val := Sum.inl v, property := ⋯ }
Tactic:
exists .eps v
State after:
no goals

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝ : { x // x ∈ G.Z }
h_v✝ : RegularProduction.alpha x✝ a✝ ∈ G.productions
h_w✝ : w✝ = [a✝]
⊢ last (fromDerivation G (RegularDerivation.alpha x✝ h_v✝ h_w✝)) ∈ (toNFA G).F
Tactic:
simp [last, fromDerivation, Fintype.wrap, toNFA]
State after:
no goals

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝¹ : { x // x ∈ G.Z }
w'✝ : List { x // x ∈ G.Z }
v'✝ : { x // x ∈ G.V }
h✝ : RegularProduction.cons x✝ (a✝¹, v'✝) ∈ G.productions
h_w✝ : w✝ = a✝¹ :: w'✝
a✝ : RegularDerivation G v'✝ w'✝
⊢ last (fromDerivation G (RegularDerivation.step x✝ v'✝ h✝ h_w✝ a✝)) ∈ (toNFA G).F
Tactic:
simp [last]
State after:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝¹ : { x // x ∈ G.Z }
w'✝ : List { x // x ∈ G.Z }
v'✝ : { x // x ∈ G.V }
h✝ : RegularProduction.cons x✝ (a✝¹, v'✝) ∈ G.productions
h_w✝ : w✝ = a✝¹ :: w'✝
a✝ : RegularDerivation G v'✝ w'✝
⊢ last (fromDerivation G a✝) ∈ (toNFA G).F

State before:
α nt : Type
Z : Finset α
inst✝¹ : DecidableEq α
V : Finset nt
inst✝ : DecidableEq nt
G : RegularGrammar α nt
v✝ : { x // x ∈ G.V }
w✝ : Word { x // x ∈ (toNFA G).Z }
d : RegularDerivation G v✝ w✝
x✝ : { x // x ∈ G.V }
a✝¹ : { x // x ∈ G.Z }
w'✝ : List { x // x ∈ G.Z }
v'✝ : { x // x ∈ G.V }
h✝ : RegularProduction.cons x✝ (a✝¹, v'✝) ∈ G.productions
h_w✝ : w✝ = a✝¹ :: w'✝
a✝ : RegularDerivation G v'✝ w'✝
⊢ last (fromDerivation G a✝) ∈ (toNFA G).F
Tactic:
apply fromDerivation_last_in_final
State after:
no goals