Theorem: Regex.NFA.lt_of_εClosure_right (RegexCorrectness/NFA/Transition/Closure/Basic.lean)

State before:
nfa : NFA
i j : ℕ
lt : i < nfa.nodes.size
h : j ∈ nfa.εClosure i
⊢ j < nfa.nodes.size
Tactic:
induction h with
| base => exact lt
| @step i j _ step _ ih =>
  have : j < nfa.nodes.size := by
    simp [εStep] at step
    split at step <;> exact lt_of_εStep step
  exact ih this
State after:
no goals

State before:
case base
nfa : NFA
i j i✝ : ℕ
lt : i✝ < nfa.nodes.size
⊢ i✝ < nfa.nodes.size
Tactic:
exact lt
State after:
no goals

State before:
case step
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Tactic:
have : j < nfa.nodes.size := by
  simp [εStep] at step
  split at step <;> exact lt_of_εStep step
State after:
case step
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size

State before:
case step
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
this : j < nfa.nodes.size
⊢ k✝ < nfa.nodes.size
Tactic:
exact ih this
State after:
no goals

State before:
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ nfa.εStep i
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
simp [εStep] at step
State after:
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ if h : i < nfa.nodes.size then nfa[i].εStep else ∅
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
⊢ j < nfa.nodes.size

State before:
nfa : NFA
i✝ j✝ i j k✝ : ℕ
step : j ∈ if h : i < nfa.nodes.size then nfa[i].εStep else ∅
rest✝ : nfa.εClosure j k✝
ih : j < nfa.nodes.size → k✝ < nfa.nodes.size
lt : i < nfa.nodes.size
⊢ j < nfa.nodes.size
Tactic:
split at step <;> exact lt_of_εStep step
State after:
no goals