case a
α : Type u_1
β : Type ?u.373972
γ : Type ?u.373975
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ filter p (s ∩ t) ↔ a✝ ∈ filter p s ∩ filter p t
α : Type u_1
β : Type ?u.373972
γ : Type ?u.373975
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p (s ∩ t) = filter p s ∩ filter p t
ext
no goals
case a
α : Type u_1
β : Type ?u.373972
γ : Type ?u.373975
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ filter p (s ∩ t) ↔ a✝ ∈ filter p s ∩ filter p t
simp [mem_filter, mem_inter, and_assoc]