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

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

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

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