Theorem: Regex.NFA.stepIn.h₂ (RegexCorrectness/NFA/Transition/Path/Basic.lean)

State before:
nfa : NFA
start i j : ℕ
cs : List Char
step : nfa.stepIn start i j cs
⊢ i < nfa.nodes.size
Tactic:
cases step with
| charStep _ h₂ _ => exact h₂
| εStep _ h₂ _ => exact h₂
State after:
no goals

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

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