Theorem: DFA.fromNFA.NFARunToRun_final_imp_final (FormalSystems/Chomsky/Regular/PowersetConstruction.lean)

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
r : NFA.Run M q w
h : NFA.Run.last r ∈ M.F
⊢ NFA.Run.last (NFARunToRun r) ∈ (fromNFA M).F
Tactic:
cases r
State after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ (fromNFA M).F

case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F

State before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ (fromNFA M).F

case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F
Tactic:
. dsimp [fromNFA]
  apply Eq.subst (propext $ Finset.mem_filter.symm) (motive := id); simp
  constructor
  dsimp [Finset.univ]
  apply Fintype.complete
  exists q; simp
  dsimp [NFA.Run.last] at h
  simp [NFARunToRun, NFA.Run.last]
  assumption
State after:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F

State before:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F
Tactic:
. dsimp [NFARunToRun, NFA.Run.last]
  apply RunFromRestricted_final
  apply NFARunToRun_final_imp_final
  dsimp [NFA.Run.last] at h
  assumption
State after:
no goals

State before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ (fromNFA M).F
Tactic:
dsimp [fromNFA]
State after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈
    Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)

State before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈
    Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
Tactic:
apply Eq.subst (propext $ Finset.mem_filter.symm) (motive := id)
State after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ id
    (NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ ∧
      ∃ q_1 ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))), q_1 ∈ M.F)

State before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ id
    (NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ ∧
      ∃ q_1 ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))), q_1 ∈ M.F)
Tactic:
simp
State after:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ ∧
    ∃ a,
      ∃ (b : a ∈ M.Q),
        { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
          { val := a, property := b } ∈ M.F

State before:
case final
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ ∧
    ∃ a,
      ∃ (b : a ∈ M.Q),
        { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
          { val := a, property := b } ∈ M.F
Tactic:
constructor
State after:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F

State before:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Finset.univ

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F
Tactic:
dsimp [Finset.univ]
State after:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Fintype.elems

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F

State before:
case final.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.final q h✝)) ∈ Finset.attach Fintype.elems

case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F
Tactic:
apply Fintype.complete
State after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F

State before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ a,
    ∃ (b : a ∈ M.Q),
      { val := a, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
        { val := a, property := b } ∈ M.F
Tactic:
exists q
State after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ (b : ↑q ∈ M.Q),
    { val := ↑q, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
      { val := ↑q, property := b } ∈ M.F

State before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ ∃ (b : ↑q ∈ M.Q),
    { val := ↑q, property := b } ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧
      { val := ↑q, property := b } ∈ M.F
Tactic:
simp
State after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ q ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧ q ∈ M.F

State before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : NFA.Run.last (NFA.Run.final q h✝) ∈ M.F
⊢ q ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧ q ∈ M.F
Tactic:
dsimp [NFA.Run.last] at h
State after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : q ∈ M.F
⊢ q ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧ q ∈ M.F

State before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : q ∈ M.F
⊢ q ∈ ↑(NFA.Run.last (NFARunToRun (NFA.Run.final q h✝))) ∧ q ∈ M.F
Tactic:
simp [NFARunToRun, NFA.Run.last]
State after:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : q ∈ M.F
⊢ q ∈ M.F

State before:
case final.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
h✝ : w = ε
h : q ∈ M.F
⊢ q ∈ M.F
Tactic:
assumption
State after:
no goals

State before:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun (NFA.Run.step q x✝ r✝ h✝)) ∈ (fromNFA M).F
Tactic:
dsimp [NFARunToRun, NFA.Run.last]
State after:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (RunFromRestricted (NFARunToRun r✝) ⋯) ∈ (fromNFA M).F

State before:
case step
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (RunFromRestricted (NFARunToRun r✝) ⋯) ∈ (fromNFA M).F
Tactic:
apply RunFromRestricted_final
State after:
case step.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun r✝) ∈ (fromNFA M).F

State before:
case step.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last (NFARunToRun r✝) ∈ (fromNFA M).F
Tactic:
apply NFARunToRun_final_imp_final
State after:
case step.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last r✝ ∈ M.F

State before:
case step.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last (NFA.Run.step q x✝ r✝ h✝) ∈ M.F
⊢ NFA.Run.last r✝ ∈ M.F
Tactic:
dsimp [NFA.Run.last] at h
State after:
case step.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last r✝ ∈ M.F
⊢ NFA.Run.last r✝ ∈ M.F

State before:
case step.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
q : { x // x ∈ M.Q }
w : Word { x // x ∈ M.Z }
q₂✝ : { x // x ∈ M.Q }
a✝ : { x // x ∈ M.Z }
w✝ : Word { x // x ∈ M.Z }
r✝ : NFA.Run M q₂✝ w✝
x✝ : q₂✝ ∈ M.δ (q, a✝)
h✝ : w = a✝ :: w✝
h : NFA.Run.last r✝ ∈ M.F
⊢ NFA.Run.last r✝ ∈ M.F
Tactic:
assumption
State after:
no goals