Theorem: DFA.fromNFA.RunFromRestricted_final
Proof state before:
case final.right.h.left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ ↑self✝

case final.right.h.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ M.F

case final.right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ↑q ∈ M.Q
Tactic:
apply Finset.mem_of_subset
Proof state after:
case final.right.h.left.a
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ?final.right.h.left.s₁ ⊆ ↑self✝

case final.right.h.left.a
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ ?final.right.h.left.s₁

case final.right.h.left.s₁
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ Finset { x // x ∈ M.Q }

case final.right.h.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ?final.right.w } ∈ M.F

case final.right.w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ ↑q ∈ M.Q