have : ∀ i ∈ S, (_ : i < nfa.nodes.size) → ∀ j ∈ nfa[i].εStep, j ∈ S := by
  intro i hi iLt j hj
  have ⟨_, hi⟩ := hi
  have jLt : j < nfa.nodes.size := lt_of_εStep hj
  have hj : j ∈ nfa.εStep i := by
    simp [εStep, iLt, hj]
  have := inv ⟨i, iLt⟩ ⟨j, jLt⟩ hi hj
  simp at this
  refine ⟨jLt, 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 ∈ 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
⊢ ∀ i ∈ next, ∀ j ∈ nfa.εClosure ↑i, ∃ (isLt : j < nfa.nodes.size), ⟨j, isLt⟩ ∈ next