case a
α : Type u_1
β : Type ?u.91847
γ : Type ?u.91850
s t : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
a✝ : α
⊢ a✝ ∈ toFinset univ ↔ a✝ ∈ Finset.univ
α : Type u_1
β : Type ?u.91847
γ : Type ?u.91850
s t : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
⊢ toFinset univ = Finset.univ
ext
no goals
case a
α : Type u_1
β : Type ?u.91847
γ : Type ?u.91850
s t : Set α
inst✝¹ : Fintype α
inst✝ : Fintype ↑univ
a✝ : α
⊢ a✝ ∈ toFinset univ ↔ a✝ ∈ Finset.univ
simp