feat(order/lattice, data/set): some helper lemmas (#14789)
This PR provides lemmas describing when `s ∪ a = t ∪ a`, in both necessary and iff forms, as well as intersection and lattice versions.
Co-authored-by: Peter Nelson <apnelson@uwaterloo.ca>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
