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

State before:
nfa : NFA
i j : ℕ
h : j ∈ nfa.εClosure i
⊢ nfa.εClosure j ⊆ nfa.εClosure i
Tactic:
intro k h'
State after:
nfa : NFA
i j : ℕ
h : j ∈ nfa.εClosure i
k : ℕ
h' : k ∈ nfa.εClosure j
⊢ k ∈ nfa.εClosure i

State before:
nfa : NFA
i j : ℕ
h : j ∈ nfa.εClosure i
k : ℕ
h' : k ∈ nfa.εClosure j
⊢ k ∈ nfa.εClosure i
Tactic:
exact εClosure_trans h h'
State after:
no goals