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

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

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

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