mathlib3

b8414e78 - feat(logic/function/basic): add injectivity/surjectivity of functions from/to subsingletons (#7060)

feat(logic/function/basic): add injectivity/surjectivity of functions from/to subsingletons (#7060) In the surjective lemma (`function.surjective.to_subsingleton`), ~~I had to assume `Type*`, instead of `Sort*`, since I was not able to make the proof work in the more general case.~~ [Edit: Eric fixed the proof so that now they work in full generality.] 🎉 Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/lemmas.20on.20int.20and.20subsingleton