Theorem: Regex.NFA.pathToNext_of_matches.alternateRight
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
a✝¹ : nfa₁ = nfa.pushRegex next r₁
a✝ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
⊢ nfa.nodes.size ≤ ↑(↑nfa').start

nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
a✝¹ : nfa₁ = nfa.pushRegex next r₁
a✝ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
⊢ ↑(↑nfa₂).start ∈ (↑nfa')[↑(↑nfa').start].εStep
Tactic:
. rw [eq₅]
  simp
  exact Nat.le_of_lt (Nat.lt_trans nfa₁.property nfa₂.property)
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r₁ r₂ : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs : List Char
eq✝ : nfa.pushRegex next (r₁.alternate 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 }
start₁ : Fin (↑nfa₁).nodes.size
nfa₂ : { nfa' // (↑nfa₁).nodes.size < nfa'.nodes.size }
start₂ : Fin (↑nfa₂).nodes.size
inBounds✝ : (Node.split ↑start₁ ↑start₂).inBounds ((↑nfa₂).nodes.size + 1)
nfa' : { nfa' // (↑nfa₂).nodes.size < nfa'.nodes.size }
property : nfa.nodes.size < (↑nfa').nodes.size
a✝¹ : nfa₁ = nfa.pushRegex next r₁
a✝ : start₁ = (↑nfa₁).start
eq₃ : nfa₂ = (↑nfa₁).pushRegex ⟨↑next, ⋯⟩ r₂
eq₄ : start₂ = (↑nfa₂).start
eq₅ : nfa' = (↑nfa₂).pushNode (Node.split ↑start₁ ↑start₂) inBounds✝
eq : nfa'✝ = ⟨↑nfa', property⟩
this✝ : (↑nfa₂).pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
this : (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa₂).start) cs
⊢ ↑(↑nfa₂).start ∈ (↑nfa')[↑(↑nfa').start].εStep