Theorem: Regex.NFA.eq_or_ge_of_step_pushRegex
Proof state before:
case inl
i j : ℕ
r : Data.Expr
ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      nfa.nodes.size ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
gt : nfa.nodes.size < i
lt : i < (↑compiled).nodes.size
this : (↑result)[i] = (↑compiled)[i]
step : (∃ c, j ∈ (↑compiled)[i].charStep c) ∨ j ∈ (↑compiled)[i].εStep
ih :
  (↑placeholder).nodes.size ≤ i →
    ∀ (h₂ : i < (↑compiled).nodes.size),
      (∃ c, j ∈ (↑compiled)[i].charStep c) ∨ j ∈ (↑compiled)[i].εStep →
        j = ↑⟨nfa.nodes.size, ⋯⟩ ∨ (↑placeholder).nodes.size ≤ j
⊢ j = ↑next ∨ nfa.nodes.size ≤ j
Tactic:
simp [eq₁] at ih
Proof state after:
case inl
i j : ℕ
r : Data.Expr
ih✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {result : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = result →
      nfa.nodes.size ≤ i →
        ∀ (h₂ : i < (↑result).nodes.size),
          (∃ c, j ∈ (↑result)[i].charStep c) ∨ j ∈ (↑result)[i].εStep → j = ↑next ∨ nfa.nodes.size ≤ j
nfa : NFA
next : Fin nfa.nodes.size
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
eq✝ : nfa.pushRegex next r.star = result
h₁ : nfa.nodes.size ≤ i
h₂ : i < (↑result).nodes.size
placeholder : { nfa' // nfa.nodes.size < nfa'.nodes.size }
compiled : { nfa' // (↑placeholder).nodes.size < nfa'.nodes.size }
patched : Array Node
nfa' : NFA
isLt : nfa.nodes.size < patched.size
inBounds : ∀ (i : Fin patched.size), patched[↑i].inBounds patched.size
property : nfa.nodes.size < nfa'.nodes.size
eq₁ : placeholder = nfa.pushNode Node.fail ⋯
eq₂ : compiled = (↑placeholder).pushRegex ⟨nfa.nodes.size, ⋯⟩ r
eq₃ : patched = (↑compiled).nodes.set ⟨nfa.nodes.size, ⋯⟩ (Node.split ↑(↑compiled).start ↑next)
eq₄ : nfa' = { nodes := patched, start := ⟨nfa.nodes.size, isLt⟩, inBounds := inBounds }
eq : result = ⟨nfa', property⟩
gt : nfa.nodes.size < i
lt : i < (↑compiled).nodes.size
this : (↑result)[i] = (↑compiled)[i]
step : (∃ c, j ∈ (↑compiled)[i].charStep c) ∨ j ∈ (↑compiled)[i].εStep
ih :
  nfa.nodes.size + 1 ≤ i →
    ∀ (h₂ : i < (↑compiled).nodes.size),
      (∃ c, j ∈ (↑compiled)[i].charStep c) ∨ j ∈ (↑compiled)[i].εStep → j = nfa.nodes.size ∨ nfa.nodes.size + 1 ≤ j
⊢ j = ↑next ∨ nfa.nodes.size ≤ j