feat(category_theory/isomorphism): two lemmas is_iso.of_iso_comp_left…

…/right on isomorphisms (#12056)

src/category_theory/isomorphism.lean

@@ -266,6 +266,22 @@ lemma comp_inv_eq (α : X ⟶ Y) [is_iso α] {f : Z ⟶ Y} {g : Z ⟶ X} : f ≫
 lemma eq_comp_inv (α : X ⟶ Y) [is_iso α] {f : Z ⟶ Y} {g : Z ⟶ X} : g = f ≫ inv α ↔ g ≫ α = f :=
 (as_iso α).eq_comp_inv
 
+lemma of_is_iso_comp_left {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
+  [is_iso f] [is_iso (f ≫ g)] : is_iso g :=
+by { rw [← id_comp g, ← inv_hom_id f, assoc], apply_instance, }
+
+lemma of_is_iso_comp_right {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
+  [is_iso g] [is_iso (f ≫ g)] : is_iso f :=
+by { rw [← comp_id f, ← hom_inv_id g, ← assoc], apply_instance, }
+
+lemma of_is_iso_fac_left {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z}
+  [is_iso f] [hh : is_iso h] (w : f ≫ g = h) : is_iso g :=
+by { rw ← w at hh, haveI := hh, exact of_is_iso_comp_left f g, }
+
+lemma of_is_iso_fac_right {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z}
+  [is_iso g] [hh : is_iso h] (w : f ≫ g = h) : is_iso f :=
+by { rw ← w at hh, haveI := hh, exact of_is_iso_comp_right f g, }
+
 end is_iso
 
 open is_iso