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

State before:
cs : List Char
nfa : NFA
start i i' : ℕ
assm : i < nfa.nodes.size
path : nfa.pathIn start i i' cs
⊢ i' < nfa.nodes.size
Tactic:
induction path with
| base _ => exact assm
| @step i j _ _ _ step _ ih =>
  have : j < nfa.nodes.size := by
    cases step with
    | charStep _ _ step => exact lt_of_charStep step
    | εStep _ _ step => exact lt_of_εStep step
  exact ih this
State after:
no goals

State before:
case base
cs : List Char
nfa : NFA
start i i' i✝ : ℕ
h✝ : start ≤ i✝
assm : i✝ < nfa.nodes.size
⊢ i✝ < nfa.nodes.size
Tactic:
exact assm
State after:
no goals

State before:
case step
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j cs₁✝
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Tactic:
have : j < nfa.nodes.size := by
  cases step with
  | charStep _ _ step => exact lt_of_charStep step
  | εStep _ _ step => exact lt_of_εStep step
State after:
case step
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j cs₁✝
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size

State before:
case step
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j cs₁✝
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Tactic:
exact ih this
State after:
no goals

State before:
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₁✝ cs₂✝ : List Char
step : nfa.stepIn start i j cs₁✝
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
cases step with
| charStep _ _ step => exact lt_of_charStep step
| εStep _ _ step => exact lt_of_εStep step
State after:
no goals

State before:
case charStep
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₂✝ : List Char
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_charStep step
State after:
no goals

State before:
case εStep
cs : List Char
nfa : NFA
start i✝ i' i j k✝ : ℕ
cs₂✝ : List Char
rest✝ : nfa.pathIn start j k✝ cs₂✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
assm : i < nfa.nodes.size
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ j < nfa.nodes.size
Tactic:
exact lt_of_εStep step
State after:
no goals