Theorem: Regex.NFA.pathToNext.cons (RegexCorrectness/NFA/Transition/Path/Basic.lean)

State before:
nfa : NFA
i j next start : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
path : nfa.pathToNext next start j cs₂
⊢ nfa.pathToNext next start i (cs₁ ++ cs₂)
Tactic:
obtain ⟨i', pcs, scs, eqs, path, step'⟩ := path
State after:
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
eqs : cs₂ = pcs ++ scs
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ cs₂)

State before:
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ cs₂ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
eqs : cs₂ = pcs ++ scs
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ cs₂)
Tactic:
subst eqs
State after:
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ (pcs ++ scs))

State before:
case intro.intro.intro.intro.intro
nfa : NFA
i j next start : ℕ
cs₁ : List Char
step : nfa.stepIn start i j cs₁
i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
⊢ nfa.pathToNext next start i (cs₁ ++ (pcs ++ scs))
Tactic:
cases step with
| charStep h₁ h₂ step =>
  exact ⟨i', _ :: pcs, scs, rfl, .step (.charStep h₁ h₂ step) path, step'⟩
| εStep h₁ h₂ step =>
  exact ⟨i', pcs, scs, rfl, .step (.εStep h₁ h₂ step) path, step'⟩
State after:
no goals

State before:
case intro.intro.intro.intro.intro.charStep
nfa : NFA
i j next start i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
c✝ : Char
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ nfa.pathToNext next start i ([c✝] ++ (pcs ++ scs))
Tactic:
exact ⟨i', _ :: pcs, scs, rfl, .step (.charStep h₁ h₂ step) path, step'⟩
State after:
no goals

State before:
case intro.intro.intro.intro.intro.εStep
nfa : NFA
i j next start i' : ℕ
pcs scs : List Char
path : nfa.pathIn start j i' pcs
step' : nfa.stepIn start i' next scs
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.pathToNext next start i ([] ++ (pcs ++ scs))
Tactic:
exact ⟨i', pcs, scs, rfl, .step (.εStep h₁ h₂ step) path, step'⟩
State after:
no goals