feat(data/finset): remove uses of choice for infima (#2699)
This PR removes the dependence of many lemmas about inf of finset sets on the axiom of choice. The motivation for this is to make `category_theory.limits.has_finite_limits_of_semilattice_inf_top` not depend on choice, which I would like so that I can prove independence results about topos models of set theory from the axiom of choice.
This does make the decidable_classical linter fail.
