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
⊢ start ≤ i
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✝
⊢ start ≤ i
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
⊢ start ≤ i
Tactic:
exact h₁
State after:
no goals