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

State before:
nfa : NFA
start i j : ℕ
cs : List Char
step : nfa.stepIn start i j cs
⊢ (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep
Tactic:
cases step with
| charStep _ _ step => exact .inl ⟨_, step⟩
| εStep _ _ step => exact .inr step
State after:
no goals

State before:
case charStep
nfa : NFA
start i j : ℕ
c✝ : Char
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
⊢ (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep
Tactic:
exact .inl ⟨_, step⟩
State after:
no goals

State before:
case εStep
nfa : NFA
start i j : ℕ
h₁✝ : start ≤ i
h₂✝ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
⊢ (∃ c, j ∈ nfa[i].charStep c) ∨ j ∈ nfa[i].εStep
Tactic:
exact .inr step
State after:
no goals