Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.go (RegexCorrectness/VM/Auxiliary.lean)

State before:
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
h : eachStepChar.go nfa c pos current i hle next saveSlots = (matched', next', saveSlots')
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
⊢ ∃ 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''
Tactic:
unfold eachStepChar.go at h
State after:
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 :
  (if h : i = current.count then (none, next, saveSlots)
    else
      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''

State before:
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 :
  (if h : i = current.count then (none, next, saveSlots)
    else
      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''
Tactic:
split at h
State after:
case inl
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 : (none, next, saveSlots) = (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''

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''

State before:
case inl
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 : (none, next, saveSlots) = (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''

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''
Tactic:
next hi =>
  subst hi
  simp at h
  simp only [←h]
  exact ⟨current.count, inv₁⟩
State after:
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''

State before:
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''
Tactic:
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₁'⟩
State after:
no goals

State before:
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
hi : i = current.count
h : (none, next, saveSlots) = (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''
Tactic:
subst hi
State after:
nfa : NFA
c : Char
pos : String.Pos
current 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₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
h : (none, next, saveSlots) = (matched', next', saveSlots')
hle : current.count ≤ current.count
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔
      ∃ i',
        ∃ (x : i' < current.count), i' < current.count ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ ∃ 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''

State before:
nfa : NFA
c : Char
pos : String.Pos
current 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₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
h : (none, next, saveSlots) = (matched', next', saveSlots')
hle : current.count ≤ current.count
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔
      ∃ i',
        ∃ (x : i' < current.count), i' < current.count ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ ∃ 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''
Tactic:
simp at h
State after:
nfa : NFA
c : Char
pos : String.Pos
current 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₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hle : current.count ≤ current.count
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔
      ∃ i',
        ∃ (x : i' < current.count), i' < current.count ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
h : none = matched' ∧ next = next' ∧ saveSlots = 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''

State before:
nfa : NFA
c : Char
pos : String.Pos
current 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₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hle : current.count ≤ current.count
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔
      ∃ i',
        ∃ (x : i' < current.count), i' < current.count ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
h : none = matched' ∧ next = next' ∧ saveSlots = 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''
Tactic:
simp only [←h]
State after:
nfa : NFA
c : Char
pos : String.Pos
current 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₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hle : current.count ≤ current.count
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔
      ∃ i',
        ∃ (x : i' < current.count), i' < current.count ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
h : none = matched' ∧ next = next' ∧ saveSlots = 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''

State before:
nfa : NFA
c : Char
pos : String.Pos
current 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₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hle : current.count ≤ current.count
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔
      ∃ i',
        ∃ (x : i' < current.count), i' < current.count ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
h : none = matched' ∧ next = next' ∧ saveSlots = 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''
Tactic:
exact ⟨current.count, inv₁⟩
State after:
no goals

State before:
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
hi : ¬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''
Tactic:
have hlt : i < current.count := Nat.lt_of_le_of_ne hle hi
State after:
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
hi : ¬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')
hlt : i < current.count
⊢ ∃ 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''

State before:
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
hi : ¬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')
hlt : i < current.count
⊢ ∃ 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''
Tactic:
simp at h
State after:
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
hi : ¬i = current.count
h :
  (match (stepChar nfa c pos next saveSlots current[i]).1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (stepChar nfa c pos next saveSlots current[i]).2.1
        (stepChar nfa c pos next saveSlots current[i]).2.2
    | some val => stepChar nfa c pos next saveSlots current[i]) =
    (matched', next', saveSlots')
hlt : i < current.count
⊢ ∃ 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''

State before:
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
hi : ¬i = current.count
h :
  (match (stepChar nfa c pos next saveSlots current[i]).1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (stepChar nfa c pos next saveSlots current[i]).2.1
        (stepChar nfa c pos next saveSlots current[i]).2.2
    | some val => stepChar nfa c pos next saveSlots current[i]) =
    (matched', next', saveSlots')
hlt : i < current.count
⊢ ∃ 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''
Tactic:
generalize hres : stepChar nfa c pos next saveSlots current[i] = result at h
State after:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = result
h :
  (match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) ⋯ 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''

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hres : stepChar nfa c pos next saveSlots current[i] = result
h :
  (match result.1 with
    | none => eachStepChar.go nfa c pos current (i + 1) ⋯ 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''
Tactic:
let (matched'', next'', saveSlots'') := result
State after:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (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''

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (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''
Tactic:
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
State after:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ ∃ 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''

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ ∃ 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''
Tactic:
have inv₂' : ∀ i j : Fin nfa.nodes.size, i ∈ next'' → j.val ∈ nfa.εStep i → j ∈ next'' :=
  stepChar_spec.preserve_cls hres inv₂
State after:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
⊢ ∃ 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''

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
⊢ ∃ 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''
Tactic:
split at h
State after:
case h_1
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
heq✝ : (matched'', next'', saveSlots'').1 = none
h :
  eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
      (matched'', next'', saveSlots'').2.2 =
    (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''

case h_2
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : (matched'', next'', saveSlots'') = (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''

State before:
case h_1
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
heq✝ : (matched'', next'', saveSlots'').1 = none
h :
  eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
      (matched'', next'', saveSlots'').2.2 =
    (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''

case h_2
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : (matched'', next'', saveSlots'') = (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''
Tactic:
next =>
  exact go h inv₁' inv₂'
State after:
case h_2
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : (matched'', next'', saveSlots'') = (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''

State before:
case h_2
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : (matched'', next'', saveSlots'') = (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''
Tactic:
next =>
  simp at h
  simp only [←h]
  exact ⟨i + 1, inv₁'⟩
State after:
no goals

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
⊢ ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
intro j
State after:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
⊢ j ∈ next'' ↔
    ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
⊢ j ∈ next'' ↔
    ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
have := stepChar_spec.mem_next_iff hres inv₂
State after:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ j ∈ next'' ↔
    ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ j ∈ next'' ↔
    ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
rw [this j, inv₁ j]
State after:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ((∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1) ↔
    ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ((∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1) ↔
    ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
apply Iff.intro
State after:
case mp
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ((∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1) →
    ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

case mpr
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ (∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') →
    (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1

State before:
case mp
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ((∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1) →
    ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

case mpr
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ (∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') →
    (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
. 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⟩
State after:
case mpr
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ (∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') →
    (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1

State before:
case mpr
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ (∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') →
    (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
. 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
State after:
no goals

State before:
case mp
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ((∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1) →
    ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
intro h
State after:
case mp
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h :
  (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

State before:
case mp
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h :
  (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
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⟩
State after:
no goals

State before:
case mp.inl
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
have ⟨i', hlt', hlt'', hmem⟩ := h
State after:
case mp.inl
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i
hmem : ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

State before:
case mp.inl
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i
hmem : ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
exact ⟨i', hlt', Nat.le.step hlt'', hmem⟩
State after:
no goals

State before:
case mp.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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
hmem : ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
exact ⟨i, hlt, Nat.lt_succ_self _, hmem⟩
State after:
no goals

State before:
case mpr
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
⊢ (∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') →
    (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
      ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
intro h
State after:
case mpr
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1

State before:
case mpr
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
have ⟨i', hlt', hlt'', hmem⟩ := h
State after:
case mpr
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i + 1
hmem : ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1

State before:
case mpr
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i + 1
hmem : ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
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
State after:
no goals

State before:
case mpr.inl
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt''✝ : i' < i + 1
hmem : ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
hlt'' : i' < i
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
exact .inl ⟨i', hlt', hlt'', hmem⟩
State after:
no goals

State before:
case mpr.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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i + 1
hmem : ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
heq : i' = i
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
simp [heq] at hmem
State after:
case mpr.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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i + 1
heq : i' = i
hmem : ∃ i'' ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i''
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1

State before:
case mpr.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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
h✝ :
  (match (matched'', next'', saveSlots'').1 with
    | none =>
      eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
        (matched'', next'', saveSlots'').2.2
    | some val => (matched'', next'', saveSlots'')) =
    (matched', next', saveSlots')
j : Fin nfa.nodes.size
this : ∀ (j : Fin nfa.nodes.size), j ∈ next'' ↔ j ∈ next ∨ ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
h : ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
i' : ℕ
hlt' : i' < current.count
hlt'' : i' < i + 1
heq : i' = i
hmem : ∃ i'' ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i''
⊢ (∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i'') ∨
    ∃ i_1 ∈ nfa.charStep (↑current[i]) c, ↑j ∈ nfa.εClosure i_1
Tactic:
exact .inr hmem
State after:
no goals

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
heq✝ : (matched'', next'', saveSlots'').1 = none
h :
  eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
      (matched'', next'', saveSlots'').2.2 =
    (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''
Tactic:
exact go h inv₁' inv₂'
State after:
no goals

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : (matched'', next'', saveSlots'') = (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''
Tactic:
simp at h
State after:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : matched'' = matched' ∧ next'' = next' ∧ saveSlots'' = 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''

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : matched'' = matched' ∧ next'' = next' ∧ saveSlots'' = 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''
Tactic:
simp only [←h]
State after:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : matched'' = matched' ∧ next'' = next' ∧ saveSlots'' = 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''

State before:
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
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ 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''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : matched'' = matched' ∧ next'' = next' ∧ saveSlots'' = 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''
Tactic:
exact ⟨i + 1, inv₁'⟩
State after:
no goals