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

State before:
j i k : ℕ
nfa : NFA
cls : j ∈ nfa.εClosure i
step : k ∈ nfa.εStep j
⊢ k ∈ nfa.εClosure i
Tactic:
induction cls with
| base => exact .step step .base
| step step' _ ih => exact εClosure.step step' (ih step)
State after:
no goals

State before:
case base
j i k : ℕ
nfa : NFA
i✝ : ℕ
step : k ∈ nfa.εStep i✝
⊢ k ∈ nfa.εClosure i✝
Tactic:
exact .step step .base
State after:
no goals

State before:
case step
j i k : ℕ
nfa : NFA
i✝ j✝ k✝ : ℕ
step' : j✝ ∈ nfa.εStep i✝
rest✝ : nfa.εClosure j✝ k✝
ih : k ∈ nfa.εStep k✝ → k ∈ nfa.εClosure j✝
step : k ∈ nfa.εStep k✝
⊢ k ∈ nfa.εClosure i✝
Tactic:
exact εClosure.step step' (ih step)
State after:
no goals