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

State before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
step : nfa.stepIn start i j cs
⊢ j < nfa.nodes.size
Tactic:
match step.step with
| .inl ⟨_, step⟩ => exact lt_of_charStep step
| .inr step => exact lt_of_εStep step
State after:
no goals

State before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
step✝ : nfa.stepIn start i j cs
w✝ : Char
step : j ∈ nfa[i].charStep w✝
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_charStep step
State after:
no goals

State before:
nfa : NFA
i j : ℕ
cs : List Char
start : ℕ
step✝ : nfa.stepIn start i j cs
step : j ∈ nfa[i].εStep
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_εStep step
State after:
no goals