Theorem: Regex.NFA.pathToNext_of_matches.starConcat
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
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 : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)
Tactic:
have ih₁ : pathToNext nfa' nfa.nodes.size placeholder.val.nodes.size compiled.val.start cs₁ := by
  apply ih₁.cast
  intro i h₁ h₂
  rw [eq₄]
  simp [eq₃]
  exists h₂
  simp [get_eq_nodes_get, eq₃]
  rw [Array.get_set_ne (hj := h₂)]
  simp
  apply Nat.ne_of_lt (Nat.lt_of_lt_of_le placeholder.property h₁)
Proof state after:
nfa : NFA
next : Fin nfa.nodes.size
r : Data.Expr
nfa'✝ : { nfa' // nfa.nodes.size < nfa'.nodes.size }
cs₁ cs₂ : List Char
eq✝ : nfa.pushRegex next r.star = 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₁
ih₂✝ :
  ∀ {nfa : NFA} {next : Fin nfa.nodes.size} {nfa' : { nfa' // nfa.nodes.size < nfa'.nodes.size }},
    nfa.pushRegex next r.star = nfa' → (↑nfa').pathToNext (↑next) nfa.nodes.size (↑(↑nfa').start) cs₂
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
ih₂ : nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) cs₂
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 : nfa'✝ = ⟨nfa', property⟩
eqStart : ↑nfa'.start = nfa.nodes.size
ih₁✝ : (↑compiled).pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
ih₁ : nfa'.pathToNext nfa.nodes.size (↑placeholder).nodes.size (↑(↑compiled).start) cs₁
⊢ nfa'.pathToNext (↑next) nfa.nodes.size (↑nfa'.start) (cs₁ ++ cs₂)