mathlib3

5ea225ec - feat(data/set/function): add `set.eq_on_union` (#16984)

feat(data/set/function): add `set.eq_on_union` (#16984) Also add `set.eq_on.union` and turn `set.comp_eq_of_eq_on_range` into an `iff` lemma `set.eq_on_range`.