Theorem: Regex.VM.captureNext_spec.go (RegexCorrectness/VM/Basic.lean)

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
h : captureNext.go nfa saveSize it current next saveSlots lastMatch = matched
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
unfold captureNext.go at h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h :
  (if it.atEnd = true then lastMatch
    else
      if (current.isEmpty && lastMatch.isSome) = true then lastMatch
      else
        let currentAndSaveSlots :=
          if lastMatch.isNone = true then
            let explored :=
              exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
            explored.2
          else (current, saveSlots);
        let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
        captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
          (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h :
  (if it.atEnd = true then lastMatch
    else
      if (current.isEmpty && lastMatch.isSome) = true then lastMatch
      else
        let currentAndSaveSlots :=
          if lastMatch.isNone = true then
            let explored :=
              exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
            explored.2
          else (current, saveSlots);
        let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
        captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
          (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
split at h
State after:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
next =>
  subst h
  exact eqs ▸ inv.acceptOfLastMatch
State after:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
next atEnd =>
  split at h
  next h' =>
    subst h
    exact eqs ▸ inv.acceptOfLastMatch
  next =>
    if hm : lastMatch.isNone then
      generalize he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored at h
      let (_, current', saveSlots') := explored
      simp [hm] at h
      have mem_current'_iff := exploreεClosure_spec.mem_next_iff he inv.currentClosure
      generalize hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = stepped at h
      let (matched', next', saveSlots'') := stepped
      simp at h
      have currentPath'  (k : Fin nfa.nodes.size) (hk : k ∈ next') :
        ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
        have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
        have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
        cases (mem_current'_iff current'[i]).mp (SparseSet.mem_get isLt) with
        | inl mem_current =>
          have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current'[i] mem_current
          have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
          subst hr
          exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
        | inr cls' =>
          have ⟨l, r, iv⟩ := v.validFor
          have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
          subst hr
          let startPos : String.Pos := ⟨String.utf8Len l⟩
          refine ⟨⟨it.toString, startPos, startPos + it.curr⟩, l.reverse, [it.curr], r', ?_, ?_, ?_⟩
          . apply Substring.ValidFor.of_eq <;> simp [iv.toString, List.reverseAux_eq]
          . apply String.Iterator.ValidFor.of_eq <;> simp [iv.next.toString, iv.next.pos]
          . have prev : nfa.reaches current'[i] [] := .nil cls'
            exact prev.snoc step cls
      have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
        ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
        cases matched' with
        | none =>
          simp at h
          exact eqs ▸ inv.acceptOfLastMatch h
        | some =>
          have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
          have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
          have eqs' := iv.toString
          simp [String.Iterator.next, List.reverseAux_eq] at eqs'
          exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
      have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
        ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
      exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
    else
      simp [hm] at h
      generalize hs : eachStepChar nfa it.curr it.next.i current next saveSlots = stepped at h
      let (matched', next', saveSlots'') := stepped
      simp at h
      have currentPath' (k : Fin nfa.nodes.size) (hk : k ∈ next') :
        ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
        have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
        have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
        have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current[i] (SparseSet.mem_get isLt)
        have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
        subst hr
        exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
      have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
        ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
        cases matched' with
        | none =>
          simp at h
          exact eqs ▸ inv.acceptOfLastMatch h
        | some =>
          have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
          have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
          have eqs' := iv.toString
          simp [String.Iterator.next, List.reverseAux_eq] at eqs'
          exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
      have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
        ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
      exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
subst h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
⊢ lastMatch.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
h✝ : it.atEnd = true
⊢ lastMatch.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact eqs ▸ inv.acceptOfLastMatch
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h :
  (if (current.isEmpty && lastMatch.isSome) = true then lastMatch
    else
      let currentAndSaveSlots :=
        if lastMatch.isNone = true then
          let explored :=
            exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
          explored.2
        else (current, saveSlots);
      let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
      captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
        (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
split at h
State after:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : (current.isEmpty && lastMatch.isSome) = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : (current.isEmpty && lastMatch.isSome) = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
next h' =>
  subst h
  exact eqs ▸ inv.acceptOfLastMatch
State after:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
next =>
  if hm : lastMatch.isNone then
    generalize he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored at h
    let (_, current', saveSlots') := explored
    simp [hm] at h
    have mem_current'_iff := exploreεClosure_spec.mem_next_iff he inv.currentClosure
    generalize hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = stepped at h
    let (matched', next', saveSlots'') := stepped
    simp at h
    have currentPath'  (k : Fin nfa.nodes.size) (hk : k ∈ next') :
      ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
      have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
      have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
      cases (mem_current'_iff current'[i]).mp (SparseSet.mem_get isLt) with
      | inl mem_current =>
        have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current'[i] mem_current
        have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
        subst hr
        exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
      | inr cls' =>
        have ⟨l, r, iv⟩ := v.validFor
        have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
        subst hr
        let startPos : String.Pos := ⟨String.utf8Len l⟩
        refine ⟨⟨it.toString, startPos, startPos + it.curr⟩, l.reverse, [it.curr], r', ?_, ?_, ?_⟩
        . apply Substring.ValidFor.of_eq <;> simp [iv.toString, List.reverseAux_eq]
        . apply String.Iterator.ValidFor.of_eq <;> simp [iv.next.toString, iv.next.pos]
        . have prev : nfa.reaches current'[i] [] := .nil cls'
          exact prev.snoc step cls
    have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
      ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
      cases matched' with
      | none =>
        simp at h
        exact eqs ▸ inv.acceptOfLastMatch h
      | some =>
        have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
        have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
        have eqs' := iv.toString
        simp [String.Iterator.next, List.reverseAux_eq] at eqs'
        exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
    have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
      ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
    exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
  else
    simp [hm] at h
    generalize hs : eachStepChar nfa it.curr it.next.i current next saveSlots = stepped at h
    let (matched', next', saveSlots'') := stepped
    simp at h
    have currentPath' (k : Fin nfa.nodes.size) (hk : k ∈ next') :
      ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
      have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
      have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
      have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current[i] (SparseSet.mem_get isLt)
      have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
      subst hr
      exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
    have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
      ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
      cases matched' with
      | none =>
        simp at h
        exact eqs ▸ inv.acceptOfLastMatch h
      | some =>
        have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
        have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
        have eqs' := iv.toString
        simp [String.Iterator.next, List.reverseAux_eq] at eqs'
        exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
    have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
      ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
    exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h' : (current.isEmpty && lastMatch.isSome) = true
h : lastMatch = matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
subst h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h' : (current.isEmpty && lastMatch.isSome) = true
⊢ lastMatch.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h' : (current.isEmpty && lastMatch.isSome) = true
⊢ lastMatch.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact eqs ▸ inv.acceptOfLastMatch
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
if hm : lastMatch.isNone then
  generalize he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored at h
  let (_, current', saveSlots') := explored
  simp [hm] at h
  have mem_current'_iff := exploreεClosure_spec.mem_next_iff he inv.currentClosure
  generalize hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = stepped at h
  let (matched', next', saveSlots'') := stepped
  simp at h
  have currentPath'  (k : Fin nfa.nodes.size) (hk : k ∈ next') :
    ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
    have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
    have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
    cases (mem_current'_iff current'[i]).mp (SparseSet.mem_get isLt) with
    | inl mem_current =>
      have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current'[i] mem_current
      have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
      subst hr
      exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
    | inr cls' =>
      have ⟨l, r, iv⟩ := v.validFor
      have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
      subst hr
      let startPos : String.Pos := ⟨String.utf8Len l⟩
      refine ⟨⟨it.toString, startPos, startPos + it.curr⟩, l.reverse, [it.curr], r', ?_, ?_, ?_⟩
      . apply Substring.ValidFor.of_eq <;> simp [iv.toString, List.reverseAux_eq]
      . apply String.Iterator.ValidFor.of_eq <;> simp [iv.next.toString, iv.next.pos]
      . have prev : nfa.reaches current'[i] [] := .nil cls'
        exact prev.snoc step cls
  have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
    ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
    cases matched' with
    | none =>
      simp at h
      exact eqs ▸ inv.acceptOfLastMatch h
    | some =>
      have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
      have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
      have eqs' := iv.toString
      simp [String.Iterator.next, List.reverseAux_eq] at eqs'
      exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
  have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
    ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
  exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
else
  simp [hm] at h
  generalize hs : eachStepChar nfa it.curr it.next.i current next saveSlots = stepped at h
  let (matched', next', saveSlots'') := stepped
  simp at h
  have currentPath' (k : Fin nfa.nodes.size) (hk : k ∈ next') :
    ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
    have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
    have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
    have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current[i] (SparseSet.mem_get isLt)
    have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
    subst hr
    exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
  have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
    ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
    cases matched' with
    | none =>
      simp at h
      exact eqs ▸ inv.acceptOfLastMatch h
    | some =>
      have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
      have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
      have eqs' := iv.toString
      simp [String.Iterator.next, List.reverseAux_eq] at eqs'
      exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
  have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
    ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
  exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
hm : lastMatch.isNone = true
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
generalize he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored at h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := explored;
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
he : exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] = explored
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := explored;
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
let (_, current', saveSlots') := explored
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := (fst✝, current', saveSlots');
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := (fst✝, current', saveSlots');
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp [hm] at h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current' next saveSlots').1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current' next saveSlots').1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have mem_current'_iff := exploreεClosure_spec.mem_next_iff he inv.currentClosure
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current' next saveSlots').1 fun x => lastMatch) =
    matched
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current' next saveSlots').2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current' next saveSlots').1 fun x => lastMatch) =
    matched
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
generalize hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = stepped at h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = stepped
h :
  captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = stepped
h :
  captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
let (matched', next', saveSlots'') := stepped
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next (matched', next', saveSlots'').2.1 current.clear
      (matched', next', saveSlots'').2.2 (HOrElse.hOrElse (matched', next', saveSlots'').1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next (matched', next', saveSlots'').2.1 current.clear
      (matched', next', saveSlots'').2.2 (HOrElse.hOrElse (matched', next', saveSlots'').1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp at h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have currentPath'  (k : Fin nfa.nodes.size) (hk : k ∈ next') :
  ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
  have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
  have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
  cases (mem_current'_iff current'[i]).mp (SparseSet.mem_get isLt) with
  | inl mem_current =>
    have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current'[i] mem_current
    have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
    subst hr
    exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
  | inr cls' =>
    have ⟨l, r, iv⟩ := v.validFor
    have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
    subst hr
    let startPos : String.Pos := ⟨String.utf8Len l⟩
    refine ⟨⟨it.toString, startPos, startPos + it.curr⟩, l.reverse, [it.curr], r', ?_, ?_, ?_⟩
    . apply Substring.ValidFor.of_eq <;> simp [iv.toString, List.reverseAux_eq]
    . apply String.Iterator.ValidFor.of_eq <;> simp [iv.next.toString, iv.next.pos]
    . have prev : nfa.reaches current'[i] [] := .nil cls'
      exact prev.snoc step cls
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
  ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
  cases matched' with
  | none =>
    simp at h
    exact eqs ▸ inv.acceptOfLastMatch h
  | some =>
    have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
    have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
    have eqs' := iv.toString
    simp [String.Iterator.next, List.reverseAux_eq] at eqs'
    exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have inv' : captureNext.go.Inv nfa it.next haystack next' (matched' <|> lastMatch) :=
  ⟨eachStepChar_spec.preserve_cls hs hemp, currentPath', acceptOfLastMatch'⟩
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
inv' : captureNext.go.Inv nfa it.next haystack next' (HOrElse.hOrElse matched' fun x => lastMatch)
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
inv' : captureNext.go.Inv nfa it.next haystack next' (HOrElse.hOrElse matched' fun x => lastMatch)
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact captureNext_spec.go h inv' (v.next' atEnd) (by simp [eqs, String.Iterator.next]) (by simp)
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
cases (mem_current'_iff current'[i]).mp (SparseSet.mem_get isLt) with
| inl mem_current =>
  have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current'[i] mem_current
  have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
  subst hr
  exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
| inr cls' =>
  have ⟨l, r, iv⟩ := v.validFor
  have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
  subst hr
  let startPos : String.Pos := ⟨String.utf8Len l⟩
  refine ⟨⟨it.toString, startPos, startPos + it.curr⟩, l.reverse, [it.curr], r', ?_, ?_, ?_⟩
  . apply Substring.ValidFor.of_eq <;> simp [iv.toString, List.reverseAux_eq]
  . apply String.Iterator.ValidFor.of_eq <;> simp [iv.next.toString, iv.next.pos]
  . have prev : nfa.reaches current'[i] [] := .nil cls'
    exact prev.snoc step cls
State after:
no goals

State before:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
mem_current : current'[i] ∈ current
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current'[i] mem_current
State after:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
mem_current : current'[i] ∈ current
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it
prev : nfa.reaches current'[i] m
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

State before:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
mem_current : current'[i] ∈ current
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it
prev : nfa.reaches current'[i] m
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
State after:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
mem_current : current'[i] ∈ current
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it
prev : nfa.reaches current'[i] m
r' : List Char
hr : r = it.curr :: r'
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

State before:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
mem_current : current'[i] ∈ current
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it
prev : nfa.reaches current'[i] m
r' : List Char
hr : r = it.curr :: r'
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
subst hr
State after:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
mem_current : current'[i] ∈ current
s : Substring
l m : List Char
prev : nfa.reaches current'[i] m
r' : List Char
sv : Substring.ValidFor l m (it.curr :: r') s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) (it.curr :: r') it
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

State before:
case inl
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
mem_current : current'[i] ∈ current
s : Substring
l m : List Char
prev : nfa.reaches current'[i] m
r' : List Char
sv : Substring.ValidFor l m (it.curr :: r') s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) (it.curr :: r') it
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
mem_current : current'[i] ∈ current
s : Substring
l m : List Char
prev : nfa.reaches current'[i] m
r' : List Char
sv : Substring.ValidFor l m (it.curr :: r') s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) (it.curr :: r') it
⊢ String.Iterator.ValidFor ((m ++ [it.curr]).reverse ++ l.reverse) r' it.next
Tactic:
simp [iv.next]
State after:
no goals

State before:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
have ⟨l, r, iv⟩ := v.validFor
State after:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r : List Char
iv : String.Iterator.ValidFor l r it
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

State before:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r : List Char
iv : String.Iterator.ValidFor l r it
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
State after:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r : List Char
iv : String.Iterator.ValidFor l r it
r' : List Char
hr : r = it.curr :: r'
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

State before:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r : List Char
iv : String.Iterator.ValidFor l r it
r' : List Char
hr : r = it.curr :: r'
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
subst hr
State after:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

State before:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
let startPos : String.Pos := ⟨String.utf8Len l⟩
State after:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m

State before:
case inr
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
Tactic:
refine ⟨⟨it.toString, startPos, startPos + it.curr⟩, l.reverse, [it.curr], r', ?_, ?_, ?_⟩
State after:
case inr.refine_1
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ Substring.ValidFor l.reverse [it.curr] r' { str := it.toString, startPos := startPos, stopPos := startPos + it.curr }

case inr.refine_2
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ String.Iterator.ValidFor ([it.curr].reverse ++ l.reverse.reverse) r' it.next

case inr.refine_3
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ nfa.reaches k [it.curr]

State before:
case inr.refine_1
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ Substring.ValidFor l.reverse [it.curr] r' { str := it.toString, startPos := startPos, stopPos := startPos + it.curr }

case inr.refine_2
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ String.Iterator.ValidFor ([it.curr].reverse ++ l.reverse.reverse) r' it.next

case inr.refine_3
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ nfa.reaches k [it.curr]
Tactic:
. apply Substring.ValidFor.of_eq <;> simp [iv.toString, List.reverseAux_eq]
State after:
case inr.refine_2
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ String.Iterator.ValidFor ([it.curr].reverse ++ l.reverse.reverse) r' it.next

case inr.refine_3
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ nfa.reaches k [it.curr]

State before:
case inr.refine_2
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ String.Iterator.ValidFor ([it.curr].reverse ++ l.reverse.reverse) r' it.next

case inr.refine_3
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ nfa.reaches k [it.curr]
Tactic:
. apply String.Iterator.ValidFor.of_eq <;> simp [iv.next.toString, iv.next.pos]
State after:
case inr.refine_3
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ nfa.reaches k [it.curr]

State before:
case inr.refine_3
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ nfa.reaches k [it.curr]
Tactic:
. have prev : nfa.reaches current'[i] [] := .nil cls'
  exact prev.snoc step cls
State after:
no goals

State before:
case inr.refine_1
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ Substring.ValidFor l.reverse [it.curr] r' { str := it.toString, startPos := startPos, stopPos := startPos + it.curr }
Tactic:
apply Substring.ValidFor.of_eq <;> simp [iv.toString, List.reverseAux_eq]
State after:
no goals

State before:
case inr.refine_2
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ String.Iterator.ValidFor ([it.curr].reverse ++ l.reverse.reverse) r' it.next
Tactic:
apply String.Iterator.ValidFor.of_eq <;> simp [iv.next.toString, iv.next.pos]
State after:
no goals

State before:
case inr.refine_3
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
⊢ nfa.reaches k [it.curr]
Tactic:
have prev : nfa.reaches current'[i] [] := .nil cls'
State after:
case inr.refine_3
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
prev : nfa.reaches current'[i] []
⊢ nfa.reaches k [it.curr]

State before:
case inr.refine_3
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
k : Fin nfa.nodes.size
hk : k ∈ next'
w✝ : ℕ
mem_next_iff :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next' ↔
      ∃ i', ∃ (x : i' < current'.count), i' < w✝ ∧ ∃ i'' ∈ nfa.charStep (↑current'[i']) it.curr, ↑j ∈ nfa.εClosure i''
i : ℕ
isLt : i < current'.count
left✝ : i < w✝
j : ℕ
step : j ∈ nfa.charStep (↑current'[i]) it.curr
cls : ↑k ∈ nfa.εClosure j
cls' : ↑current'[i] ∈ nfa.εClosure ↑nfa.start
l r' : List Char
iv : String.Iterator.ValidFor l (it.curr :: r') it
startPos : String.Pos := { byteIdx := String.utf8Len l }
prev : nfa.reaches current'[i] []
⊢ nfa.reaches k [it.curr]
Tactic:
exact prev.snoc step cls
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
h : (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
cases matched' with
| none =>
  simp at h
  exact eqs ▸ inv.acceptOfLastMatch h
| some =>
  have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
  have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
  have eqs' := iv.toString
  simp [String.Iterator.next, List.reverseAux_eq] at eqs'
  exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
State after:
no goals

State before:
case none
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (none, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse none fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse none fun x => lastMatch).isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp at h
State after:
case none
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (none, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse none fun x => lastMatch) =
    matched
h : lastMatch.isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case none
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (none, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse none fun x => lastMatch) =
    matched
h : lastMatch.isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact eqs ▸ inv.acceptOfLastMatch h
State after:
no goals

State before:
case some
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
State after:
case some
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case some
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
State after:
case some
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case some
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have eqs' := iv.toString
State after:
case some
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.next.s = { data := (m.reverse ++ l.reverse).reverseAux r }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case some
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.next.s = { data := (m.reverse ++ l.reverse).reverseAux r }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp [String.Iterator.next, List.reverseAux_eq] at eqs'
State after:
case some
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.s = { data := l ++ (m ++ r) }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
case some
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.s = { data := l ++ (m ++ r) }
⊢ ∃ s l m r, Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝¹ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
val✝ : Array (Option String.Pos)
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (some val✝, next', saveSlots'')
h✝ :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse (some val✝) fun x => lastMatch) =
    matched
h : (HOrElse.hOrElse (some val✝) fun x => lastMatch).isSome = true
i : Fin nfa.nodes.size
hi : i ∈ next'
hdone : nfa[i] = Node.done
s : Substring
l m r : List Char
sv : Substring.ValidFor l m r s
iv : String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next
reaches : nfa.reaches i m
eqs' : it.s = { data := l ++ (m ++ r) }
⊢ haystack = { data := l ++ m ++ r }
Tactic:
simp [eqs, eqs']
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
inv' : captureNext.go.Inv nfa it.next haystack next' (HOrElse.hOrElse matched' fun x => lastMatch)
⊢ haystack = it.next.toString
Tactic:
simp [eqs, String.Iterator.next]
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : lastMatch.isNone = true
explored :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
fst✝ : Option (Array (Option String.Pos))
current' : SparseSet nfa.nodes.size
saveSlots' : Vec (Array (Option String.Pos)) nfa.nodes.size
he :
  exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[] =
    (fst✝, current', saveSlots')
mem_current'_iff : ∀ (i : Fin nfa.nodes.size), i ∈ current' ↔ i ∈ current ∨ ↑i ∈ nfa.εClosure ↑nfa.start
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current' next saveSlots' = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
inv' : captureNext.go.Inv nfa it.next haystack next' (HOrElse.hOrElse matched' fun x => lastMatch)
⊢ current.clear.isEmpty = true
Tactic:
simp
State after:
no goals

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
h :
  (let currentAndSaveSlots :=
      if lastMatch.isNone = true then
        let explored := exploreεClosure nfa it.pos current (captureNext.initSave saveSize) none saveSlots nfa.start #[];
        explored.2
      else (current, saveSlots);
    let stepped := eachStepChar nfa it.curr it.next.pos currentAndSaveSlots.1 next currentAndSaveSlots.2;
    captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch)) =
    matched
hm : ¬lastMatch.isNone = true
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp [hm] at h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current next saveSlots).2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current next saveSlots).2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current next saveSlots).1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
h :
  captureNext.go nfa saveSize it.next (eachStepChar nfa it.curr it.next.i current next saveSlots).2.1 current.clear
      (eachStepChar nfa it.curr it.next.i current next saveSlots).2.2
      (HOrElse.hOrElse (eachStepChar nfa it.curr it.next.i current next saveSlots).1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
generalize hs : eachStepChar nfa it.curr it.next.i current next saveSlots = stepped at h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = stepped
h :
  captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = stepped
h :
  captureNext.go nfa saveSize it.next stepped.2.1 current.clear stepped.2.2
      (HOrElse.hOrElse stepped.1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
let (matched', next', saveSlots'') := stepped
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next (matched', next', saveSlots'').2.1 current.clear
      (matched', next', saveSlots'').2.2 (HOrElse.hOrElse (matched', next', saveSlots'').1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next (matched', next', saveSlots'').2.1 current.clear
      (matched', next', saveSlots'').2.2 (HOrElse.hOrElse (matched', next', saveSlots'').1 fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
simp at h
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have currentPath' (k : Fin nfa.nodes.size) (hk : k ∈ next') :
  ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ it.next.ValidFor (m.reverse ++ l.reverse) r ∧ nfa.reaches k m := by
  have ⟨_, mem_next_iff⟩ := eachStepChar_spec.mem_next_iff hs hemp
  have ⟨i, isLt, _, ⟨j, step, cls⟩⟩ := (mem_next_iff k).mp hk
  have ⟨s, l, m, r, sv, iv, prev⟩ := inv.currentPath current[i] (SparseSet.mem_get isLt)
  have ⟨r', hr⟩ := iv.exists_cons_of_not_atEnd atEnd
  subst hr
  exact ⟨s.expand, l, m ++ [it.curr], r', sv.expand, by simp [iv.next], prev.snoc step cls⟩
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done

State before:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
Tactic:
have acceptOfLastMatch' (h : (matched' <|> lastMatch).isSome) :
  ∃ (s : Substring) (l m r : List Char), s.ValidFor l m r ∧ haystack = ⟨l ++ m ++ r⟩ ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = .done := by
  cases matched' with
  | none =>
    simp at h
    exact eqs ▸ inv.acceptOfLastMatch h
  | some =>
    have ⟨i, hi, hdone⟩ := (eachStepChar_spec.mem_done_iff hs hemp).mpr rfl
    have ⟨s, l, m, r, sv, iv, reaches⟩ := currentPath' i hi
    have eqs' := iv.toString
    simp [String.Iterator.next, List.reverseAux_eq] at eqs'
    exact ⟨s, l, m, r, sv, by simp [eqs, eqs'], ⟨i, reaches, hdone⟩⟩
State after:
nfa : NFA
saveSize : ℕ
it : String.Iterator
current next : SparseSet nfa.nodes.size
saveSlots : Vec (Array (Option String.Pos)) nfa.nodes.size
lastMatch matched : Option (Array (Option String.Pos))
haystack : String
inv : captureNext.go.Inv nfa it haystack current lastMatch
v : it.Valid
eqs : haystack = it.toString
hemp : next.isEmpty = true
atEnd : ¬it.atEnd = true
h✝ : ¬(current.isEmpty && lastMatch.isSome) = true
hm : ¬lastMatch.isNone = true
stepped : Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots'' : Vec (Array (Option String.Pos)) nfa.nodes.size
hs : eachStepChar nfa it.curr it.next.i current next saveSlots = (matched', next', saveSlots'')
h :
  captureNext.go nfa saveSize it.next next' current.clear saveSlots'' (HOrElse.hOrElse matched' fun x => lastMatch) =
    matched
currentPath' :
  ∀ k ∈ next',
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ String.Iterator.ValidFor (m.reverse ++ l.reverse) r it.next ∧ nfa.reaches k m
acceptOfLastMatch' :
  (HOrElse.hOrElse matched' fun x => lastMatch).isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done
⊢ matched.isSome = true →
    ∃ s l m r,
      Substring.ValidFor l m r s ∧ haystack = { data := l ++ m ++ r } ∧ ∃ i, nfa.reaches i m ∧ nfa[i] = Node.done