Theorem: IMOSL.IMO2009C1.filter_symmDiff (IMOSLLean4/IMO2009/C1/C1.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
A B : Finset α
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ x ∈ filter p (symmDiff A B) ↔ x ∈ symmDiff (filter p A) (filter p B)
Tactic:
rw [mem_filter, mem_symmDiff, mem_symmDiff,
mem_filter, mem_filter, not_and_or, not_and_or,
and_and_or_not_iff, and_and_or_not_iff, ← or_and_right]
State after:
no goals