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

src/logic/function/basic.lean

@@ -92,6 +92,10 @@ lemma injective.of_comp_iff' (f : α → β) {g : γ → α} (hg : bijective g)
     hx ▸ hy ▸ λ hf, h hf ▸ rfl,
   λ h, h.comp hg.injective⟩
 
+lemma injective_of_subsingleton [subsingleton α] (f : α → β) :
+  injective f :=
+λ a b ab, subsingleton.elim _ _
+
 lemma injective.dite (p : α → Prop) [decidable_pred p]
   {f : {a : α // p a} → β} {f' : {a : α // ¬ p a} → β}
   (hf : injective f) (hf' : injective f')
@@ -350,6 +354,10 @@ lemma bijective_iff_has_inverse : bijective f ↔ ∃ g, left_inverse g f ∧ ri
 lemma injective_surj_inv (h : surjective f) : injective (surj_inv h) :=
 (right_inverse_surj_inv h).injective
 
+lemma surjective_to_subsingleton [na : nonempty α] [subsingleton β] (f : α → β) :
+  surjective f :=
+λ y, let ⟨a⟩ := na in ⟨a, subsingleton.elim _ _⟩
+
 end surj_inv
 
 section update