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

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

State before:
case base
nfa : NFA
i j : ℕ
cs : List Char
start i✝ : ℕ
h : start ≤ i✝
⊢ start ≤ i✝
Tactic:
exact h
State after:
no goals

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