feat(logic/function/basic): add function.{in,sur,bi}jective.comp_left (#10406)

As far as I can tell we don't have these variations.

Note that the `surjective` and `bijective` versions do not appear next to the other composition statements, as they require `surj_inv` to concisely prove.

Author: eric-wieser

src/logic/function/basic.lean

@@ -92,6 +92,11 @@ lemma injective.of_comp_iff' (f : α → β) {g : γ → α} (hg : bijective g)
     hx ▸ hy ▸ λ hf, h hf ▸ rfl,
   λ h, h.comp hg.injective⟩
 
+/-- Composition by an injective function on the left is itself injective. -/
+lemma injective.comp_left {g : β → γ} (hg : function.injective g) :
+  function.injective ((∘) g : (α → β) → (α → γ)) :=
+λ f₁ f₂ hgf, funext $ λ i, hg $ (congr_fun hgf i : _)
+
 lemma injective_of_subsingleton [subsingleton α] (f : α → β) :
   injective f :=
 λ a b ab, subsingleton.elim _ _
@@ -345,7 +350,7 @@ lemma injective_iff_has_left_inverse : injective f ↔ has_left_inverse f :=
 end inv_fun
 
 section surj_inv
-variables {α : Sort u} {β : Sort v} {f : α → β}
+variables {α : Sort u} {β : Sort v} {γ : Sort w} {f : α → β}
 
 /-- The inverse of a surjective function. (Unlike `inv_fun`, this does not require
   `α` to be inhabited.) -/
@@ -376,6 +381,16 @@ lemma surjective_to_subsingleton [na : nonempty α] [subsingleton β] (f : α 
   surjective f :=
 λ y, let ⟨a⟩ := na in ⟨a, subsingleton.elim _ _⟩
 
+/-- Composition by an surjective function on the left is itself surjective. -/
+lemma surjective.comp_left {g : β → γ} (hg : function.surjective g) :
+  function.surjective ((∘) g : (α → β) → (α → γ)) :=
+λ f, ⟨surj_inv hg ∘ f, funext $ λ x, right_inverse_surj_inv _ _⟩
+
+/-- Composition by an bijective function on the left is itself bijective. -/
+lemma bijective.comp_left {g : β → γ} (hg : function.bijective g) :
+  function.bijective ((∘) g : (α → β) → (α → γ)) :=
+⟨hg.injective.comp_left, hg.surjective.comp_left⟩
+
 end surj_inv
 
 section update