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

State before:
nfa : NFA
next i : ℕ
cs : List Char
start : ℕ
path : nfa.pathToNext next start i cs
⊢ start ≤ i
Tactic:
obtain ⟨_, _, _, _, path, _⟩ := path
State after:
case intro.intro.intro.intro.intro
nfa : NFA
next i : ℕ
cs : List Char
start w✝² : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : nfa.pathIn start i w✝² w✝¹
right✝ : nfa.stepIn start w✝² next w✝
⊢ start ≤ i

State before:
case intro.intro.intro.intro.intro
nfa : NFA
next i : ℕ
cs : List Char
start w✝² : ℕ
w✝¹ w✝ : List Char
left✝ : cs = w✝¹ ++ w✝
path : nfa.pathIn start i w✝² w✝¹
right✝ : nfa.stepIn start w✝² next w✝
⊢ start ≤ i
Tactic:
exact le_of_pathIn_left path
State after:
no goals