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

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

State before:
case intro.intro.intro.intro.intro
next i : ℕ
cs : List Char
nfa : NFA
start i' : ℕ
pcs scs : List Char
eqs : cs = pcs ++ scs
path : nfa.pathIn start i i' pcs
step : nfa.stepIn start i' next scs
⊢ nfa.pathIn (min start next) i next cs
Tactic:
cases step with
| charStep h₁ h₂ step => exact eqs ▸ path.snoc_char h₂ step
| εStep h₁ h₂ step => simp [eqs, path.snoc_ε h₂ step]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.charStep
next i : ℕ
cs : List Char
nfa : NFA
start i' : ℕ
pcs : List Char
path : nfa.pathIn start i i' pcs
c✝ : Char
h₁ : start ≤ i'
h₂ : i' < nfa.nodes.size
step : next ∈ nfa[i'].charStep c✝
eqs : cs = pcs ++ [c✝]
⊢ nfa.pathIn (min start next) i next cs
Tactic:
exact eqs ▸ path.snoc_char h₂ step
State after:
no goals

State before:
case intro.intro.intro.intro.intro.εStep
next i : ℕ
cs : List Char
nfa : NFA
start i' : ℕ
pcs : List Char
path : nfa.pathIn start i i' pcs
h₁ : start ≤ i'
h₂ : i' < nfa.nodes.size
step : next ∈ nfa[i'].εStep
eqs : cs = pcs ++ []
⊢ nfa.pathIn (min start next) i next cs
Tactic:
simp [eqs, path.snoc_ε h₂ step]
State after:
no goals