case h
α : Type u_1
β : Type ?u.1081
γ : Type ?u.1084
inst✝ : Fintype α
s t : Finset α
x✝ : α
⊢ x✝ ∈ ↑univ ↔ x✝ ∈ Set.univ
α : Type u_1
β : Type ?u.1081
γ : Type ?u.1084
inst✝ : Fintype α
s t : Finset α
⊢ ↑univ = Set.univ
ext
no goals
case h
α : Type u_1
β : Type ?u.1081
γ : Type ?u.1084
inst✝ : Fintype α
s t : Finset α
x✝ : α
⊢ x✝ ∈ ↑univ ↔ x✝ ∈ Set.univ
simp