feat(Filter): add Filter.EventuallyEq.symmDiff (#15016)

Mathlib/Order/Filter/Basic.lean

@@ -78,7 +78,7 @@ we do *not* require. This gives `Filter X` better formal properties, in particul
 assert_not_exists OrderedSemiring
 
 open Function Set Order
-open scoped Classical
+open scoped Classical symmDiff
 
 universe u v w x y
 
@@ -1394,6 +1394,10 @@ theorem EventuallyEq.diff {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t)
     (s \ s' : Set α) =ᶠ[l] (t \ t' : Set α) :=
   h.inter h'.compl
 
+protected theorem EventuallyEq.symmDiff {s t s' t' : Set α} {l : Filter α}
+    (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') : (s ∆ s' : Set α) =ᶠ[l] (t ∆ t' : Set α) :=
+  (h.diff h').union (h'.diff h)
+
 theorem eventuallyEq_empty {s : Set α} {l : Filter α} : s =ᶠ[l] (∅ : Set α) ↔ ∀ᶠ x in l, x ∉ s :=
   eventuallyEq_set.trans <| by simp