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

State before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
path : nfa.pathIn start i j cs
⊢ start ≤ i
Tactic:
cases path with
| base h => exact h
| step step _ => exact le_of_stepIn step
State after:
no goals

State before:
case base
nfa : NFA
i start : ℕ
h : start ≤ i
⊢ start ≤ i
Tactic:
exact h
State after:
no goals

State before:
case step
nfa : NFA
i j start j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j✝ cs₁✝
rest✝ : nfa.pathIn start j✝ j cs₂✝
⊢ start ≤ i
Tactic:
exact le_of_stepIn step
State after:
no goals