no goals
α : Type u_1
β : Type ?u.372476
γ : Type ?u.372479
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
s t : Finset α
inst✝ : (i : α) → Decidable (i ∈ t)
i : α
⊢ i ∈ filter (fun i => i ∈ t) s ↔ i ∈ s ∩ t
simp [mem_filter, mem_inter]