next hi =>
  have hlt : i < current.count := Nat.lt_of_le_of_ne hle hi
  simp at h
  generalize hres : stepChar nfa c pos next saveSlots current[i] = result at h
  let (matched'', next'', saveSlots'') := result
  have inv₁' : ∀ j, j ∈ next'' ↔ ∃ i', ∃ _ : i' < current.count, i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep current[i'] c, j.val ∈ nfa.εClosure i'' := by
    intro j
    have := stepChar_spec.mem_next_iff hres inv₂
    rw [this j, inv₁ j]
    apply Iff.intro
    . intro h
      cases h with
      | inl h =>
        have ⟨i', hlt', hlt'', hmem⟩ := h
        exact ⟨i', hlt', Nat.le.step hlt'', hmem⟩
      | inr hmem => exact ⟨i, hlt, Nat.lt_succ_self _, hmem⟩
    . intro h
      have ⟨i', hlt', hlt'', hmem⟩ := h
      cases Nat.lt_succ_iff_lt_or_eq.mp hlt'' with
      | inl hlt'' => exact .inl ⟨i', hlt', hlt'', hmem⟩
      | inr heq =>
        simp [heq] at hmem
        exact .inr hmem
  have inv₂' : ∀ i j : Fin nfa.nodes.size, i ∈ next'' → j.val ∈ nfa.εStep i → j ∈ next'' :=
    stepChar_spec.preserve_cls hres inv₂
  split at h
  next =>
    exact go h inv₁' inv₂'
  next =>
    simp at h
    simp only [←h]
    exact ⟨i + 1, inv₁'⟩
case inr
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
inv₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
h✝ : ¬i = current.count
h :
  (let_fun hlt := ⋯;
    let result := stepChar nfa c pos next saveSlots current[i];
    match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) hlt result.2.1 result.2.2
    | some val => result) =
    (matched', next', saveSlots')
⊢ ∃ istop,
    ∀ (j : Fin nfa.nodes.size),
      j ∈ next' ↔
        ∃ i', ∃ (x : i' < current.count), i' < istop ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
no goals