case h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ εNFA.εClosure (toεNFA M) S ↔ a ∈ S
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a : α
M : NFA α σ
S : Set σ
⊢ εNFA.εClosure (toεNFA M) S = S
ext a
case h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ εNFA.εClosure (toεNFA M) S → a ∈ S
case h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ εNFA.εClosure (toεNFA M) S ↔ a ∈ S
refine' ⟨_, εNFA.εClosure.base _⟩
case h.base
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
h : a ∈ S
⊢ a ∈ S

case h.step
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝¹ : α
M : NFA α σ
S : Set σ
a s✝ : σ
a✝ : εNFA.εClosure (toεNFA M) S s✝
h : a ∈ εNFA.step (toεNFA M) s✝ none
⊢ a ∈ S
case h
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
⊢ a ∈ εNFA.εClosure (toεNFA M) S → a ∈ S
rintro (⟨_, h⟩ | ⟨_, _, h, _⟩)
no goals
case h.base
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝ : α
M : NFA α σ
S : Set σ
a : σ
h : a ∈ S
⊢ a ∈ S
exact h
no goals
case h.step
α : Type u
σ σ' : Type v
M✝ : εNFA α σ
S✝ : Set σ
x : List α
s : σ
a✝¹ : α
M : NFA α σ
S : Set σ
a s✝ : σ
a✝ : εNFA.εClosure (toεNFA M) S s✝
h : a ∈ εNFA.step (toεNFA M) s✝ none
⊢ a ∈ S
cases h