simp at this
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
this : ⟨j, jLt⟩ ∈ next ∨ StackEntry.explore ⟨j, jLt⟩ ∈ #[]
⊢ j ∈ S
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
i : ℕ
hi✝ : i ∈ S
iLt : i < nfa.nodes.size
j : ℕ
hj✝ : j ∈ nfa[i].εStep
w✝ : i < nfa.nodes.size
hi : ⟨i, w✝⟩ ∈ next
jLt : j < nfa.nodes.size
hj : j ∈ nfa.εStep i
this : next.mem ⟨j, jLt⟩ = true
⊢ j ∈ S