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

State before:
i j : ℕ
cs : List Char
nfa nfa' : NFA
start : ℕ
step : nfa.stepIn start i j cs
h : i < nfa'.nodes.size
eq : nfa[i] = nfa'[i]
⊢ nfa'.stepIn start i j cs
Tactic:
cases step with
| charStep h₁ h₂ step =>
  exact .charStep h₁ h (eq ▸ step)
| εStep h₁ h₂ step =>
  exact .εStep h₁ h (eq ▸ step)
State after:
no goals

State before:
case charStep
i j : ℕ
nfa nfa' : NFA
start : ℕ
h : i < nfa'.nodes.size
c✝ : Char
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].charStep c✝
eq : nfa[i] = nfa'[i]
⊢ nfa'.stepIn start i j [c✝]
Tactic:
exact .charStep h₁ h (eq ▸ step)
State after:
no goals

State before:
case εStep
i j : ℕ
nfa nfa' : NFA
start : ℕ
h : i < nfa'.nodes.size
h₁ : start ≤ i
h₂ : i < nfa.nodes.size
step : j ∈ nfa[i].εStep
eq : nfa[i] = nfa'[i]
⊢ nfa'.stepIn start i j []
Tactic:
exact .εStep h₁ h (eq ▸ step)
State after:
no goals