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

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h : NFA.Run.last r ∈ (fromNFA M).F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
match r with
| .final _ _ =>
  dsimp [NFA.Run.last, fromNFA] at h
  have ⟨_, qf, _, _⟩ := Finset.mem_filter.mp h
  exists qf; constructor; assumption
  apply Exists.intro; swap
  apply NFA.Run.final _
  assumption
  dsimp [NFA.Run.last]
  assumption
| .step _ h_step _ _ =>
  dsimp [NFA.Run.last] at h
  dsimp [fromNFA, toNFA] at h_step; simp at h_step
  have ⟨_, h_q₂, r', hr'⟩ := fromNFA_run_imp_run h
  rw [h_step, Finset.mem_fold_union_iff] at h_q₂
  have ⟨x, _, _⟩ := h_q₂
  exists x; constructor; assumption
  apply Exists.intro; swap
  apply NFA.Run.step
  repeat { assumption }
State after:
no goals

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

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
have ⟨_, qf, _, _⟩ := Finset.mem_filter.mp h
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
exists qf
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ qf ∈ ↑q₀ ∧ ∃ r', NFA.Run.last r' ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ qf ∈ ↑q₀ ∧ ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
constructor
State after:
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ qf ∈ ↑q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ r', NFA.Run.last r' ∈ M.F

State before:
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ qf ∈ ↑q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
assumption
State after:
case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ r', NFA.Run.last r' ∈ M.F

State before:
case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
apply Exists.intro
State after:
case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run.last ?right.w ∈ M.F

case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run M qf w

State before:
case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run.last ?right.w ∈ M.F

case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run M qf w
Tactic:
swap
State after:
case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run M qf w

case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run.last ?right.w ∈ M.F

State before:
case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run M qf w

case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run.last ?right.w ∈ M.F
Tactic:
apply NFA.Run.final _
State after:
case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ w = ε

case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run.last (NFA.Run.final qf ?right.w) ∈ M.F

State before:
case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ w = ε

case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run.last (NFA.Run.final qf ?right.w) ∈ M.F
Tactic:
assumption
State after:
case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ NFA.Run.last (NFA.Run.final qf h✝) ∈ M.F

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

State before:
case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
h✝ : w = ε
h : q₀ ∈ Finset.filter (fun s => ∃ q ∈ ↑s, q ∈ M.F) (Finset.attach Finset.univ)
left✝¹ : q₀ ∈ Finset.attach Finset.univ
qf : { x // x ∈ M.Q }
left✝ : qf ∈ ↑q₀
right✝ : qf ∈ M.F
⊢ qf ∈ M.F
Tactic:
assumption
State after:
no goals

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

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
h_step : q₂✝ ∈ (toNFA (fromNFA M)).δ (q₀, a✝)
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
h✝ : w = a✝ :: w✝
h : NFA.Run.last r✝ ∈ (fromNFA M).F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
dsimp [fromNFA, toNFA] at h_step
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
h_step : q₂✝ ∈ {{ val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }}
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
h✝ : w = a✝ :: w✝
h : NFA.Run.last r✝ ∈ (fromNFA M).F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
h_step : q₂✝ ∈ {{ val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }}
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
h✝ : w = a✝ :: w✝
h : NFA.Run.last r✝ ∈ (fromNFA M).F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
simp at h_step
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
h✝ : w = a✝ :: w✝
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝
h✝ : w = a✝ :: w✝
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
have ⟨_, h_q₂, r', hr'⟩ := fromNFA_run_imp_run h
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : w✝ ∈ ↑q₂✝
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : w✝ ∈ ↑q₂✝
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
rw [h_step, Finset.mem_fold_union_iff] at h_q₂
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
have ⟨x, _, _⟩ := h_q₂
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ∃ q ∈ ↑q₀, ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
exists x
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ x ∈ ↑q₀ ∧ ∃ r', NFA.Run.last r' ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ x ∈ ↑q₀ ∧ ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
constructor
State after:
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ x ∈ ↑q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ∃ r', NFA.Run.last r' ∈ M.F

State before:
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ x ∈ ↑q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
assumption
State after:
case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ∃ r', NFA.Run.last r' ∈ M.F

State before:
case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ∃ r', NFA.Run.last r' ∈ M.F
Tactic:
apply Exists.intro
State after:
case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last ?right.w ∈ M.F

case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M x w

State before:
case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last ?right.w ∈ M.F

case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M x w
Tactic:
swap
State after:
case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M x w

case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last ?right.w ∈ M.F

State before:
case right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M x w

case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last ?right.w ∈ M.F
Tactic:
apply NFA.Run.step
State after:
case right.w.x
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ?right.w.q₂ ∈ M.δ (x, ?right.w.a)

case right.w.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M ?right.w.q₂ ?right.w.w

case right.w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ w = ?right.w.a :: ?right.w.w

case right.w.q₂
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ { x // x ∈ M.Q }

case right.w.a
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ { x // x ∈ M.Z }

case right.w.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ Word { x // x ∈ M.Z }

case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last (NFA.Run.step x ?right.w.x ?right.w.r ?right.w.h) ∈ M.F

State before:
case right.w.x
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ ?right.w.q₂ ∈ M.δ (x, ?right.w.a)

case right.w.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run M ?right.w.q₂ ?right.w.w

case right.w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ w = ?right.w.a :: ?right.w.w

case right.w.q₂
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ { x // x ∈ M.Q }

case right.w.a
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ { x // x ∈ M.Z }

case right.w.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ Word { x // x ∈ M.Z }

case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last (NFA.Run.step x ?right.w.x ?right.w.r ?right.w.h) ∈ M.F
Tactic:
repeat { assumption }
State after:
no goals

State before:
case right.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (toNFA (fromNFA M)).Z }
q₀ : { x // x ∈ (fromNFA M).Q }
r : Run (fromNFA M) q₀ w
q₂✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : { x // x ∈ (toNFA (fromNFA M)).Z }
w✝¹ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
r✝ : NFA.Run (toNFA (fromNFA M)) q₂✝ w✝¹
h✝ : w = a✝ :: w✝¹
h : NFA.Run.last r✝ ∈ (fromNFA M).F
h_step : q₂✝ = { val := Finset.fold (fun x x_1 => x ∪ x_1) ∅ (fun q => M.δ (q, a✝)) ↑q₀, property := ⋯ }
w✝ : { x // x ∈ M.Q }
h_q₂ : ∃ x ∈ ↑q₀, w✝ ∈ M.δ (x, a✝)
r' : NFA.Run M w✝ w✝¹
hr' : NFA.Run.last r' ∈ M.F
x : { x // x ∈ M.Q }
left✝ : x ∈ ↑q₀
right✝ : w✝ ∈ M.δ (x, a✝)
⊢ NFA.Run.last (NFA.Run.step x right✝ r' h✝) ∈ M.F
Tactic:
assumption
State after:
no goals