Theorem: Regex.NFA.pathToNext_of_matches.group
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₁ : (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs
Tactic:
have path₁ : pathToNext nfa''' nfa''.val.start nfa.nodes.size nfa'''.val.start [] := by
  apply path₁.castStart (Nat.le_of_lt ?_)
  exact Nat.lt_trans nfa'.property nfa''.property
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
i : ℕ
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (Data.Expr.group i r) = nfa'✝
ih :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs
nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }
nfa'' : { nfa'_1 // (↑nfa').nodes.size < nfa'_1.nodes.size }
nfa''' : { nfa'_1 // (↑nfa'').nodes.size < nfa'_1.nodes.size }
property : nfa.nodes.size < (↑nfa''').nodes.size
inBounds'✝ : (Node.save (2 * i + 1) ↑next).inBounds (nfa.nodes.size + 1)
inBounds'''✝ : (Node.save (2 * i) ↑(↑nfa'').start).inBounds ((↑nfa'').nodes.size + 1)
eq₁ : nfa' = nfa.pushNode (Node.save (2 * i + 1) ↑next) inBounds'✝
eq₂ : nfa'' = (↑nfa').pushRegex (↑nfa').start r
eq₃ : nfa''' = (↑nfa'').pushNode (Node.save (2 * i) ↑(↑nfa'').start) inBounds'''✝
eq : nfa'✝ = ⟨↑nfa''', property⟩
path₃✝ : (↑nfa').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₃ : (↑nfa'').pathToNext (↑next) nfa.nodes.size ↑(↑nfa').start []
path₂✝ : (↑nfa'').pathToNext (↑(↑nfa').start) (↑nfa').nodes.size (↑(↑nfa'').start) cs
path₂ : (↑nfa'').pathToNext (↑(↑nfa').start) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃✝ : (↑nfa'').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₂₃ : (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa'').start) cs
path₁✝ : (↑nfa''').pathToNext (↑(↑nfa'').start) (↑nfa'').nodes.size ↑(↑nfa''').start []
path₁ : (↑nfa''').pathToNext (↑(↑nfa'').start) nfa.nodes.size ↑(↑nfa''').start []
⊢ (↑nfa''').pathToNext (↑next) nfa.nodes.size (↑(↑nfa''').start) cs