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

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

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

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