mathlib3

136e0d68 - feat(data/fintype/basic): The cardinality of a set is at most the cardinality of the universe (#7823)

feat(data/fintype/basic): The cardinality of a set is at most the cardinality of the universe (#7823) I think that the hypothesis `[fintype ↥s]` can be avoided with the use of classical logic. E.g., `noncomputable instance set_fintype' {α : Type*} [fintype α] (s : set α) : fintype s :=by { classical, exact set_fintype s }` Would it make sense to add this? Co-authored-by: tb65536 <tb65536@users.noreply.github.com>