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

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

State before:
case base
i j : ℕ
cs : List Char
nfa : NFA
start start' : ℕ
le : start' ≤ start
i✝ : ℕ
h : start ≤ i✝
⊢ nfa.pathIn start' i✝ i✝ []
Tactic:
exact .base (Nat.le_trans le h)
State after:
no goals

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