Theorem: Regex.NFA.stepIn.castStart' (RegexCorrectness/NFA/Transition/Path/Basic.lean)

State before:
i j : ℕ
cs : List Char
nfa : NFA
start start' : ℕ
le : start' ≤ i
step : nfa.stepIn start i j cs
⊢ nfa.stepIn start' i j cs
Tactic:
cases step with
| charStep h₁ h₂ step => exact .charStep le h₂ step
| εStep h₁ h₂ step => exact .εStep le h₂ step
State after:
no goals

State before:
case charStep
i j : ℕ
nfa : NFA
start start' : ℕ
le : start' ≤ i
c✝ : Char
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ nfa.stepIn start' i j [c✝]
Tactic:
exact .charStep le h₂ step
State after:
no goals

State before:
case εStep
i j : ℕ
nfa : NFA
start start' : ℕ
le : start' ≤ i
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ nfa.stepIn start' i j []
Tactic:
exact .εStep le h₂ step
State after:
no goals