Symmetric differences of intersections

The symmetric difference of an intersection with a set lies in the union of the symmetric differences: the intersection member of Mathlib's Set.union_symmDiff_subset family, obtained from the union member by complementation.

theorem Set.inter_symmDiff_subset {α : Type u_1} {s t u : Set α} : symmDiff (s ∩ t) u ⊆ symmDiff s u ∪ symmDiff t u

(s ∩ t) ∆ u ⊆ s ∆ u ∪ t ∆ u.