have : j ∈ S := this hj
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 : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this : nfa.εClosure ↑i ⊆ S
⊢ ∃ (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 : Fin nfa.nodes.size
hi : i ∈ next
j : ℕ
hj : j ∈ nfa.εClosure ↑i
this✝ : nfa.εClosure ↑i ⊆ S
this : j ∈ S
⊢ ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next