Theorem: Regex.NFA.starLoop.intro'
Proof state before:
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih✝ :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        cs' = [] ∨
          ∃ cs₁ cs₂,
            cs' = cs₁ ++ cs₂ ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
      else
        ∃ cs₁ cs₂, cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
ih :
  if j = nfa.nodes.size then
    cs' = [] ∨
      ∃ cs₁ cs₂,
        cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
  else ∃ cs₁ cs₂, cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂
Tactic:
split at ih
Proof state after:
case inl
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih✝ :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        cs' = [] ∨
          ∃ cs₁ cs₂,
            cs' = cs₁ ++ cs₂ ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
      else
        ∃ cs₁ cs₂, cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
h✝ : j = nfa.nodes.size
ih :
  cs' = [] ∨
    ∃ cs₁ cs₂,
      cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂

case inr
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i✝ loopStart : ℕ
cs✝ : List Char
eq : nfa.pushRegex next r.star = result
i j k : ℕ
cs cs' : List Char
step : (↑result).stepIn nfa.nodes.size i j cs
path : (↑result).pathIn nfa.nodes.size j k cs'
ih✝ :
  j < (↑result).nodes.size →
    k = nfa.nodes.size →
      if j = nfa.nodes.size then
        cs' = [] ∨
          ∃ cs₁ cs₂,
            cs' = cs₁ ++ cs₂ ∧
              (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) (rStart_of eq) cs₁ ∧ starLoop eq cs₂
      else
        ∃ cs₁ cs₂, cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
assm₁ : i < (↑result).nodes.size
assm₂ : k = nfa.nodes.size
nei : ¬i = nfa.nodes.size
gti : nfa.nodes.size < i
h✝ : ¬j = nfa.nodes.size
ih : ∃ cs₁ cs₂, cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) j cs₁ ∧ starLoop eq cs₂
⊢ ∃ cs₁ cs₂, cs ++ cs' = cs₁ ++ cs₂ ∧ (↑result).pathToNext nfa.nodes.size (nfa.nodes.size + 1) i cs₁ ∧ starLoop eq cs₂