no goals
α : Type u_1
β : Type ?u.285746
γ : Type ?u.285749
inst✝ : DecidableEq α
s t : Finset α
a b : α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ ¬a ∈ t ∨ a ∈ t ∧ ¬a ∈ s
simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]