feat(Finset/SymmDiff): add additional api lemmas (#25553)

Fill in simple lemmas as convenient special cases with the right syntactic equalities for rewrites.

Author: b-mehta

Mathlib/Data/Finset/SymmDiff.lean

@@ -52,6 +52,18 @@ theorem image_symmDiff [DecidableEq β] {f : α → β} (s t : Finset α) (hf :
     (s ∆ t).image f = s.image f ∆ t.image f :=
   mod_cast Set.image_symmDiff hf s t
 
+/-- See `symmDiff_subset_sdiff'` for the swapped version of this. -/
+lemma symmDiff_subset_sdiff : s \ t ⊆ s ∆ t := subset_union_left
+
+/-- See `symmDiff_subset_sdiff` for the swapped version of this. -/
+lemma symmDiff_subset_sdiff' : t \ s ⊆ s ∆ t := subset_union_right
+
+lemma symmDiff_subset_union : s ∆ t ⊆ s ∪ t := symmDiff_le_sup (α := Finset α)
+
+lemma symmDiff_eq_union_iff (s t : Finset α) : s ∆ t = s ∪ t ↔ Disjoint s t := symmDiff_eq_sup s t
+
+lemma symmDiff_eq_union (h : Disjoint s t) : s ∆ t = s ∪ t := Disjoint.symmDiff_eq_sup h
+
 end SymmDiff
 
 end Finset