feat(data/finset/lattice): choice-free le_sup_iff and lt_sup_iff (#7584)
feat(data/finset/lattice): choice-free le_sup_iff and lt_sup_iff (#7584)

Propagate to `finset` the change to `le_sup_iff [is_total α (≤)]` and `lt_sup_iff [is_total α (≤)]` made in #7455.





leanprover-community/mathlib,leanprover-community/mathlib