diff --git a/src/category_theory/closed/cartesian.lean b/src/category_theory/closed/cartesian.lean
index e99ad286c72bc..eed6ddc1b4933 100644
--- a/src/category_theory/closed/cartesian.lean
+++ b/src/category_theory/closed/cartesian.lean
@@ -341,7 +341,7 @@ def cartesian_closed_of_equiv (e : C ≌ D) [h : cartesian_closed C] : cartesian
         { rw [assoc, prod.lift_fst, prod.lift_fst, ←functor.map_comp,
             limits.prod.map_fst, comp_id], },
         { rw [assoc, prod.lift_snd, prod.lift_snd, ←functor.map_comp_assoc, limits.prod.map_snd],
-          simp only [nat_iso.hom_inv_id_app, assoc, equivalence.inv_fun_map,
+          simp only [iso.hom_inv_id_app, assoc, equivalence.inv_fun_map,
             functor.map_comp, comp_id],
           erw comp_id, }, },
       { have : is_left_adjoint (e.functor ⋙ prod_functor.obj X ⋙ e.inverse) :=
diff --git a/src/category_theory/equivalence.lean b/src/category_theory/equivalence.lean
index 220952d2d4fbc..f1d6e05698d15 100644
--- a/src/category_theory/equivalence.lean
+++ b/src/category_theory/equivalence.lean
@@ -177,8 +177,8 @@ variables {E : Type u₃} [category.{v₃} E]
   begin
     dsimp,
     rw [← f.functor.map_comp_assoc, e.functor.map_comp, functor_unit, fun_inv_map,
-        inv_hom_id_app_assoc, assoc, inv_hom_id_app, counit_functor, ← functor.map_comp],
-    erw [comp_id, hom_inv_id_app, functor.map_id],
+        iso.inv_hom_id_app_assoc, assoc, iso.inv_hom_id_app, counit_functor, ← functor.map_comp],
+    erw [comp_id, iso.hom_inv_id_app, functor.map_id],
   end }
 
 def fun_inv_id_assoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F ≅ F :=
@@ -370,7 +370,7 @@ instance faithful_of_equivalence (F : C ⥤ D) [is_equivalence F] : faithful F :
 instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F :=
 { preimage := λ X Y f, F.fun_inv_id.inv.app X ≫ F.inv.map f ≫ F.fun_inv_id.hom.app Y,
   witness' := λ X Y f, F.inv.map_injective
-  (by simpa only [is_equivalence.inv_fun_map, assoc, hom_inv_id_app_assoc, hom_inv_id_app] using comp_id _) }
+  (by simpa only [is_equivalence.inv_fun_map, assoc, iso.hom_inv_id_app_assoc, iso.hom_inv_id_app] using comp_id _) }
 
 @[simp] private def equivalence_inverse (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : D ⥤ C :=
 { obj  := λ X, F.obj_preimage X,
diff --git a/src/category_theory/limits/cones.lean b/src/category_theory/limits/cones.lean
index f1e283db5a8ef..781de54f6bfae 100644
--- a/src/category_theory/limits/cones.lean
+++ b/src/category_theory/limits/cones.lean
@@ -429,8 +429,8 @@ begin
   { dsimp,
     erw [comp_id, ← H.inv_fun_id.hom.naturality (c.π.app j), comp_map, H.map_comp],
     congr' 1,
-    erw [← cancel_epi (H.inv_fun_id.inv.app (H.obj (F.obj j))), nat_iso.inv_hom_id_app,
-         ← (functor.as_equivalence H).functor_unit _, ← H.map_comp, nat_iso.hom_inv_id_app,
+    erw [← cancel_epi (H.inv_fun_id.inv.app (H.obj (F.obj j))), iso.inv_hom_id_app,
+         ← (functor.as_equivalence H).functor_unit _, ← H.map_comp, iso.hom_inv_id_app,
          H.map_id],
     refl }
 end
diff --git a/src/category_theory/limits/limits.lean b/src/category_theory/limits/limits.lean
index 8269e77690536..3f5a8803e2b65 100644
--- a/src/category_theory/limits/limits.lean
+++ b/src/category_theory/limits/limits.lean
@@ -222,7 +222,7 @@ def map_cone_equiv {D : Type u'} [category.{v} D] {K : J ⥤ C} {F G : C ⥤ D}
     slice_lhs 2 3 {erw ← h.hom.naturality (c.π.app j)},
     slice_lhs 1 2 {erw t.fac ((cones.postcompose (iso_whisker_left K h).inv).obj s) j},
     dsimp,
-    slice_lhs 2 3 {rw nat_iso.inv_hom_id_app},
+    slice_lhs 2 3 {rw iso.inv_hom_id_app},
     rw category.comp_id,
   end,
   uniq' := λ s m J,
@@ -233,7 +233,7 @@ def map_cone_equiv {D : Type u'} [category.{v} D] {K : J ⥤ C} {F G : C ⥤ D}
     dsimp,
     slice_lhs 2 3 {erw ← h.inv.naturality (c.π.app j)},
     slice_lhs 1 2 {erw J j},
-    conv_rhs {congr, rw [category.assoc, nat_iso.hom_inv_id_app, comp_id]},
+    conv_rhs {congr, rw [category.assoc, iso.hom_inv_id_app, comp_id]},
     apply (t.fac ((cones.postcompose (iso_whisker_left K h).inv).obj s) j).symm
   end }
 
diff --git a/src/category_theory/natural_isomorphism.lean b/src/category_theory/natural_isomorphism.lean
index a67bc0122ca1b..210660ea453dc 100644
--- a/src/category_theory/natural_isomorphism.lean
+++ b/src/category_theory/natural_isomorphism.lean
@@ -14,39 +14,41 @@ universes v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
 namespace category_theory
 open nat_trans
 
+variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
+  {E : Type u₃} [category.{v₃} E]
+
+namespace iso
+
 /-- The application of a natural isomorphism to an object. We put this definition in a different
 namespace, so that we can use `α.app` -/
-@[simp, reducible] def iso.app {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
-  {F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X :=
+@[simp, reducible] def app {F G : C ⥤ D} (α : F ≅ G) (X : C) : F.obj X ≅ G.obj X :=
 { hom := α.hom.app X,
   inv := α.inv.app X,
   hom_inv_id' := begin rw [← comp_app, iso.hom_inv_id], refl end,
   inv_hom_id' := begin rw [← comp_app, iso.inv_hom_id], refl end }
 
+@[simp, reassoc]
+lemma hom_inv_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
+  α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) :=
+congr_fun (congr_arg nat_trans.app α.hom_inv_id) X
+
+@[simp, reassoc]
+lemma inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
+  α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
+congr_fun (congr_arg nat_trans.app α.inv_hom_id) X
+
+end iso
 
 namespace nat_iso
 
 open category_theory.category category_theory.functor
 
-variables {C : Type u₁} [category.{v₁} C] {D : Type u₂} [category.{v₂} D]
-  {E : Type u₃} [category.{v₃} E]
-
 @[simp] lemma trans_app {F G H : C ⥤ D} (α : F ≅ G) (β : G ≅ H) (X : C) :
   (α ≪≫ β).app X = α.app X ≪≫ β.app X := rfl
 
 lemma app_hom {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).hom = α.hom.app X := rfl
 lemma app_inv {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).inv = α.inv.app X := rfl
 
-@[simp, reassoc]
-lemma hom_inv_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
-  α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) :=
-congr_fun (congr_arg app α.hom_inv_id) X
-
-@[simp, reassoc]
-lemma inv_hom_id_app {F G : C ⥤ D} (α : F ≅ G) (X : C) :
-  α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X) :=
-congr_fun (congr_arg app α.inv_hom_id) X
-
 variables {F G : C ⥤ D}
 
 instance hom_app_is_iso (α : F ≅ G) (X : C) : is_iso (α.hom.app X) :=
@@ -58,11 +60,6 @@ instance inv_app_is_iso (α : F ≅ G) (X : C) : is_iso (α.inv.app X) :=
   hom_inv_id' := begin rw [←comp_app, iso.inv_hom_id, ←id_app] end,
   inv_hom_id' := begin rw [←comp_app, iso.hom_inv_id, ←id_app] end }
 
-lemma hom_app_inv_app_id (α : F ≅ G) (X : C) : α.hom.app X ≫ α.inv.app X = 𝟙 _ :=
-hom_inv_id_app _ _
-lemma inv_app_hom_app_id (α : F ≅ G) (X : C) : α.inv.app X ≫ α.hom.app X = 𝟙 _ :=
-inv_hom_id_app _ _
-
 variables {X Y : C}
 lemma naturality_1 (α : F ≅ G) (f : X ⟶ Y) :
   (α.inv.app X) ≫ (F.map f) ≫ (α.hom.app Y) = G.map f :=
diff --git a/src/category_theory/opposites.lean b/src/category_theory/opposites.lean
index 1d7d209a2b066..390ad9bca29a5 100644
--- a/src/category_theory/opposites.lean
+++ b/src/category_theory/opposites.lean
@@ -259,8 +259,8 @@ isomorphism between the original functors `F ≅ G`. -/
 protected definition op (α : F ≅ G) : G.op ≅ F.op :=
 { hom := nat_trans.op α.hom,
   inv := nat_trans.op α.inv,
-  hom_inv_id' := begin ext, dsimp, rw ←op_comp, rw inv_hom_id_app, refl, end,
-  inv_hom_id' := begin ext, dsimp, rw ←op_comp, rw hom_inv_id_app, refl, end }
+  hom_inv_id' := begin ext, dsimp, rw ←op_comp, rw α.inv_hom_id_app, refl, end,
+  inv_hom_id' := begin ext, dsimp, rw ←op_comp, rw α.hom_inv_id_app, refl, end }
 
 @[simp] lemma op_hom (α : F ≅ G) : (nat_iso.op α).hom = nat_trans.op α.hom := rfl
 @[simp] lemma op_inv (α : F ≅ G) : (nat_iso.op α).inv = nat_trans.op α.inv := rfl
@@ -270,8 +270,8 @@ between the opposite functors `F.op ≅ G.op`. -/
 protected definition unop (α : F.op ≅ G.op) : G ≅ F :=
 { hom := nat_trans.unop α.hom,
   inv := nat_trans.unop α.inv,
-  hom_inv_id' := begin ext, dsimp, rw ←unop_comp, rw inv_hom_id_app, refl, end,
-  inv_hom_id' := begin ext, dsimp, rw ←unop_comp, rw hom_inv_id_app, refl, end }
+  hom_inv_id' := begin ext, dsimp, rw ←unop_comp, rw α.inv_hom_id_app, refl, end,
+  inv_hom_id' := begin ext, dsimp, rw ←unop_comp, rw α.hom_inv_id_app, refl, end }
 
 @[simp] lemma unop_hom (α : F.op ≅ G.op) : (nat_iso.unop α).hom = nat_trans.unop α.hom := rfl
 @[simp] lemma unop_inv (α : F.op ≅ G.op) : (nat_iso.unop α).inv = nat_trans.unop α.inv := rfl
diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean
index c0bdd91e9c9ad..498ece5a12fbc 100644
--- a/src/category_theory/types.lean
+++ b/src/category_theory/types.lean
@@ -100,6 +100,11 @@ congr_fun (F.map_iso f).hom_inv_id x
 @[simp] lemma map_hom_map_inv_apply (f : X ≅ Y) (y : F.obj Y) : F.map f.hom (F.map f.inv y) = y :=
 congr_fun (F.map_iso f).inv_hom_id y
 
+@[simp] lemma hom_inv_id_app_apply (α : F ≅ G) (X) (x) : α.inv.app X (α.hom.app X x) = x :=
+congr_fun (α.hom_inv_id_app X) x
+@[simp] lemma inv_hom_id_app_apply (α : F ≅ G) (X) (x) : α.hom.app X (α.inv.app X x) = x :=
+congr_fun (α.inv_hom_id_app X) x
+
 end functor_to_types
 
 /--