Theorem: Regex.VM.eachStepChar_spec.mem_done_iff.go
Proof state before:
case h_1
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
heq : stepChar nfa c pos next saveSlots current[i] = (none, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ none.isSome = true
h : eachStepChar.go nfa c pos current (i + 1) ⋯ next'' saveSlots'' = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true

case h_2
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq : stepChar nfa c pos next saveSlots current[i] = (some val✝, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ (some val✝).isSome = true
h : (some val✝, next'', saveSlots'') = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
Tactic:
next =>
  simp at this
  exact eachStepChar_spec.mem_done_iff.go h this
Proof state after:
case h_2
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × Data.Vec (Array (Option String.Pos)) nfa.nodes.size
next'' : SparseSet nfa.nodes.size
saveSlots'' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq : stepChar nfa c pos next saveSlots current[i] = (some val✝, next'', saveSlots'')
this : (∃ i ∈ next'', nfa[i] = Node.done) ↔ (some val✝).isSome = true
h : (some val✝, next'', saveSlots'') = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true