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