feat(Order/PartialSups): add exists_partialSups_eq#34029

lua-vr wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

lua-vr:exists_partialSups_eqlua-vr/mathlib4:exists_partialSups_eqCopy head branch name to clipboard