case a
α : Type u_1
β : Type ?u.320628
γ : Type ?u.320631
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x => True) s ↔ a✝ ∈ s
α : Type u_1
β : Type ?u.320628
γ : Type ?u.320631
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter (fun x => True) s = s
ext
no goals
case a
α : Type u_1
β : Type ?u.320628
γ : Type ?u.320631
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x => True) s ↔ a✝ ∈ s
simp