feat(category_theory/isomorphism): lemmas for manipulating isomorphisms

Author: rwbarton

category_theory/equivalence.lean

@@ -239,14 +239,7 @@ section
 { obj  := λ X, F.obj_preimage X,
   map := λ X Y f, F.preimage ((F.fun_obj_preimage_iso X).hom ≫ f ≫ (F.fun_obj_preimage_iso Y).inv),
   map_id' := λ X, begin apply F.injectivity, tidy, end,
-  map_comp' := λ X Y Z f g,
-  begin
-    apply F.injectivity,
-    /- obviously can finish from here... -/
-    simp,
-    slice_rhs 2 3 { erw [is_iso.hom_inv_id] },
-    simp,
-  end }.
+  map_comp' := λ X Y Z f g, by apply F.injectivity; simp }.
 
 def equivalence_of_fully_faithfully_ess_surj
   (F : C ⥤ D) [full F] [faithful : faithful F] [ess_surj F] : is_equivalence F :=
@@ -261,4 +254,4 @@ end
 
 end category_theory.equivalence
 
-end category_theory
+end category_theory

category_theory/isomorphism.lean

@@ -26,6 +26,12 @@ variables {X Y Z : C}
 
 namespace iso
 
+@[simp] lemma hom_inv_id_assoc (α : X ≅ Y) (f : X ⟶ Z) : α.hom ≫ α.inv ≫ f = f :=
+by rw [←category.assoc, α.hom_inv_id, category.id_comp]
+
+@[simp] lemma inv_hom_id_assoc (α : X ≅ Y) (f : Y ⟶ Z) : α.inv ≫ α.hom ≫ f = f :=
+by rw [←category.assoc, α.inv_hom_id, category.id_comp]
+
 @[extensionality] lemma ext
   (α β : X ≅ Y)
   (w : α.hom = β.hom) : α = β :=
@@ -82,6 +88,18 @@ infixr ` ≪≫ `:80 := iso.trans -- type as `\ll \gg`.
 @[simp] lemma refl_symm (X : C) : (iso.refl X).hom = 𝟙 X := rfl
 @[simp] lemma trans_symm (α : X ≅ Y) (β : Y ≅ Z) : (α ≪≫ β).inv = β.inv ≫ α.inv := rfl
 
+lemma inv_comp_eq (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : α.inv ≫ f = g ↔ f = α.hom ≫ g :=
+⟨λ H, by simp [H.symm], λ H, by simp [H]⟩
+
+lemma eq_inv_comp (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z} : g = α.inv ≫ f ↔ α.hom ≫ g = f :=
+(inv_comp_eq α.symm).symm
+
+lemma comp_inv_eq (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : f ≫ α.inv = g ↔ f = g ≫ α.hom :=
+⟨λ H, by simp [H.symm], λ H, by simp [H]⟩
+
+lemma eq_comp_inv (α : X ≅ Y) {f : Z ⟶ Y} {g : Z ⟶ X} : g = f ≫ α.inv ↔ g ≫ α.hom = f :=
+(comp_inv_eq α.symm).symm
+
 end iso
 
 /-- `is_iso` typeclass expressing that a morphism is invertible.

category_theory/natural_isomorphism.lean

@@ -78,12 +78,7 @@ def of_components (app : ∀ X : C, (F.obj X) ≅ (G.obj X))
   inv  :=
   { app := λ X, ((app X).inv),
     naturality' := λ X Y f,
-    begin
-      let p := congr_arg (λ f, (app X).inv ≫ (f ≫ (app Y).inv)) (eq.symm (naturality f)),
-      dsimp at *,
-      simp at *,
-      erw [←p, ←category.assoc, is_iso.hom_inv_id, category.id_comp],
-    end } }.
+    by simpa using congr_arg (λ f, (app X).inv ≫ (f ≫ (app Y).inv)) (eq.symm (naturality f)) } }
 
 @[simp] def of_components.app (app' : ∀ X : C, (F.obj X) ≅ (G.obj X)) (naturality) (X) :
   app (of_components app' naturality) X = app' X :=