Theorem: symmDiff_union (Ray/Misc/Bounds.lean)

State before:
A B : Finset ℕ
⊢ A ∆ B = A \ B ∪ B \ A
Tactic:
rw [symmDiff_def, Finset.sup_eq_union]
State after:
no goals