mathlib3

41038bac - feat(data/set): add exists_maximal_wrt