Commit 2021-06-07 07:44 136e0d68
View on Github →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?