case a
α : Type u_1
β : Type ?u.97519
γ : Type ?u.97522
s t : Set α
a : α
inst✝ : Fintype ↑{a}
a✝ : α
⊢ a✝ ∈ toFinset {a} ↔ a✝ ∈ {a}
α : Type u_1
β : Type ?u.97519
γ : Type ?u.97522
s t : Set α
a : α
inst✝ : Fintype ↑{a}
⊢ toFinset {a} = {a}
ext
no goals
case a
α : Type u_1
β : Type ?u.97519
γ : Type ?u.97522
s t : Set α
a : α
inst✝ : Fintype ↑{a}
a✝ : α
⊢ a✝ ∈ toFinset {a} ↔ a✝ ∈ {a}
simp