have := mem_εStep_iff_εClosure_sub.mp this
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next
nfa : NFA
next : SparseSet nfa.nodes.size
inv : LowerInvεClosure nfa next #[]
S : Set ℕ := {j | ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next}
this✝ : ∀ i ∈ S, ∀ (x : i < nfa.nodes.size), ∀ j ∈ nfa[i].εStep, j ∈ S
this : ∀ i ∈ S, nfa.εClosure i ⊆ S
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next