diff --git a/src/algebra/category/Algebra/basic.lean b/src/algebra/category/Algebra/basic.lean
index cf9fa700c34da..2a292ee789845 100644
--- a/src/algebra/category/Algebra/basic.lean
+++ b/src/algebra/category/Algebra/basic.lean
@@ -145,5 +145,5 @@ instance Algebra.forget_reflects_isos : reflects_isomorphisms (forget (Algebra.{
     resetI,
     let i := as_iso ((forget (Algebra.{u} R)).map f),
     let e : X ≃ₐ[R] Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Algebra_iso },
+    exact is_iso.of_iso e.to_Algebra_iso,
   end }
diff --git a/src/algebra/category/CommRing/basic.lean b/src/algebra/category/CommRing/basic.lean
index 433bc0b002ab6..ab4d4fb74305a 100644
--- a/src/algebra/category/CommRing/basic.lean
+++ b/src/algebra/category/CommRing/basic.lean
@@ -202,7 +202,7 @@ instance Ring.forget_reflects_isos : reflects_isomorphisms (forget Ring.{u}) :=
     resetI,
     let i := as_iso ((forget Ring).map f),
     let e : X ≃+* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Ring_iso },
+    exact is_iso.of_iso e.to_Ring_iso,
   end }
 
 instance CommRing.forget_reflects_isos : reflects_isomorphisms (forget CommRing.{u}) :=
@@ -211,7 +211,7 @@ instance CommRing.forget_reflects_isos : reflects_isomorphisms (forget CommRing.
     resetI,
     let i := as_iso ((forget CommRing).map f),
     let e : X ≃+* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_CommRing_iso },
+    exact is_iso.of_iso e.to_CommRing_iso,
   end }
 
 example : reflects_isomorphisms (forget₂ Ring AddCommGroup) := by apply_instance
diff --git a/src/algebra/category/Group/basic.lean b/src/algebra/category/Group/basic.lean
index 95088d35ea577..0d101c788ba68 100644
--- a/src/algebra/category/Group/basic.lean
+++ b/src/algebra/category/Group/basic.lean
@@ -250,7 +250,7 @@ instance Group.forget_reflects_isos : reflects_isomorphisms (forget Group.{u}) :
     resetI,
     let i := as_iso ((forget Group).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Group_iso },
+    exact is_iso.of_iso e.to_Group_iso,
   end }
 
 @[to_additive]
@@ -260,5 +260,5 @@ instance CommGroup.forget_reflects_isos : reflects_isomorphisms (forget CommGrou
     resetI,
     let i := as_iso ((forget CommGroup).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_CommGroup_iso },
+    exact is_iso.of_iso e.to_CommGroup_iso,
   end }
diff --git a/src/algebra/category/Mon/basic.lean b/src/algebra/category/Mon/basic.lean
index 9b0f911822863..559012232dfbf 100644
--- a/src/algebra/category/Mon/basic.lean
+++ b/src/algebra/category/Mon/basic.lean
@@ -179,7 +179,7 @@ instance Mon.forget_reflects_isos : reflects_isomorphisms (forget Mon.{u}) :=
     resetI,
     let i := as_iso ((forget Mon).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Mon_iso },
+    exact is_iso.of_iso e.to_Mon_iso,
   end }
 
 @[to_additive]
@@ -189,7 +189,7 @@ instance CommMon.forget_reflects_isos : reflects_isomorphisms (forget CommMon.{u
     resetI,
     let i := as_iso ((forget CommMon).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_CommMon_iso },
+    exact is_iso.of_iso e.to_CommMon_iso,
   end }
 
 /-!
diff --git a/src/algebra/category/Semigroup/basic.lean b/src/algebra/category/Semigroup/basic.lean
index ac52d3dc5ee64..94ffe60cb45a2 100644
--- a/src/algebra/category/Semigroup/basic.lean
+++ b/src/algebra/category/Semigroup/basic.lean
@@ -168,7 +168,7 @@ instance Magma.forget_reflects_isos : reflects_isomorphisms (forget Magma.{u}) :
     resetI,
     let i := as_iso ((forget Magma).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Magma_iso },
+    exact is_iso.of_iso e.to_Magma_iso,
   end }
 
 @[to_additive]
@@ -178,7 +178,7 @@ instance Semigroup.forget_reflects_isos : reflects_isomorphisms (forget Semigrou
     resetI,
     let i := as_iso ((forget Semigroup).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Semigroup_iso },
+    exact is_iso.of_iso e.to_Semigroup_iso,
   end }
 
 /-!
diff --git a/src/algebra/homology/exact.lean b/src/algebra/homology/exact.lean
index 25ab1bcecaa35..3ab8cc8ff86ef 100644
--- a/src/algebra/homology/exact.lean
+++ b/src/algebra/homology/exact.lean
@@ -86,7 +86,7 @@ lemma exact_comp_mono [exact f g] [mono h] : exact f (g ≫ h) :=
 begin
   refine ⟨by simp, _⟩,
   letI : is_iso (kernel.lift (g ≫ h) (kernel.ι g) (by simp)) :=
-  { inv := kernel.lift g (kernel.ι (g ≫ h)) (by simp [←cancel_mono h]) },
+    ⟨kernel.lift g (kernel.ι (g ≫ h)) (by simp [←cancel_mono h]), by tidy⟩,
   rw image_to_kernel_map_comp_right f g h exact.w,
   exact epi_comp _ _
 end
@@ -95,8 +95,8 @@ lemma exact_kernel : exact (kernel.ι f) f :=
 begin
   refine ⟨kernel.condition _, _⟩,
   letI : is_iso (image_to_kernel_map (kernel.ι f) f (kernel.condition f)) :=
-  { inv := factor_thru_image (kernel.ι f),
-    hom_inv_id' := by simp [←cancel_mono (image.ι (kernel.ι f))] },
+    ⟨factor_thru_image (kernel.ι f),
+      ⟨by simp [←cancel_mono (image.ι (kernel.ι f))], by tidy⟩⟩,
   apply_instance
 end
 
diff --git a/src/algebraic_geometry/presheafed_space.lean b/src/algebraic_geometry/presheafed_space.lean
index 0e8e4cf2996db..2a922611555fe 100644
--- a/src/algebraic_geometry/presheafed_space.lean
+++ b/src/algebraic_geometry/presheafed_space.lean
@@ -107,9 +107,9 @@ instance category_of_PresheafedSpaces : category (PresheafedSpace C) :=
     { dsimp, simp only [id_comp] },  -- See note [dsimp, simp].
     { ext U, op_induction, cases U,
       dsimp,
-      simp only [comp_id, id_comp, map_id, presheaf.pushforward.comp_inv_app],
+      simp only [presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
       dsimp,
-      simp only [comp_id], },
+      simp only [comp_id, comp_id, map_id], },
   end,
   comp_id' := λ X Y f,
   begin
@@ -117,9 +117,9 @@ instance category_of_PresheafedSpaces : category (PresheafedSpace C) :=
     { dsimp, simp only [comp_id] },
     { ext U, op_induction, cases U,
       dsimp,
-      simp only [comp_id, id_comp, map_id, presheaf.pushforward.comp_inv_app],
+      simp only [presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
       dsimp,
-      simp only [comp_id], }
+      simp only [id_comp, comp_id, map_id], }
   end,
   assoc' := λ W X Y Z f g h,
   begin
@@ -127,9 +127,9 @@ instance category_of_PresheafedSpaces : category (PresheafedSpace C) :=
      refl,
      { ext U, op_induction, cases U,
        dsimp,
-       simp only [assoc, map_id, comp_id, presheaf.pushforward.comp_inv_app],
+       simp only [assoc, presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
        dsimp,
-       simp only [comp_id, id_comp], }
+       simp only [comp_id, id_comp, map_id], }
   end }
 
 end
diff --git a/src/algebraic_geometry/presheafed_space/has_colimits.lean b/src/algebraic_geometry/presheafed_space/has_colimits.lean
index 9039b49433eae..36b55b3d5a0f1 100644
--- a/src/algebraic_geometry/presheafed_space/has_colimits.lean
+++ b/src/algebraic_geometry/presheafed_space/has_colimits.lean
@@ -75,7 +75,7 @@ begin
   cases U,
   dsimp,
   simp only [PresheafedSpace.congr_app (F.map_comp f g)],
-  dsimp, simp,
+  dsimp, simp, dsimp, simp, -- See note [dsimp, simp]
 end
 
 /--
diff --git a/src/category_theory/abelian/basic.lean b/src/category_theory/abelian/basic.lean
index ae3bd602a04b0..7b3c32128285a 100644
--- a/src/category_theory/abelian/basic.lean
+++ b/src/category_theory/abelian/basic.lean
@@ -144,7 +144,7 @@ variables {X Y : C} (f : X ⟶ Y)
 local attribute [instance] strong_epi_of_epi
 
 /-- In an abelian category, a monomorphism which is also an epimorphism is an isomorphism. -/
-def is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
+lemma is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
 is_iso_of_mono_of_strong_epi _
 
 end mono_epi_iso
diff --git a/src/category_theory/abelian/non_preadditive.lean b/src/category_theory/abelian/non_preadditive.lean
index 7776df48b38e9..0a88735100cf9 100644
--- a/src/category_theory/abelian/non_preadditive.lean
+++ b/src/category_theory/abelian/non_preadditive.lean
@@ -109,7 +109,7 @@ local attribute [instance] strong_epi_of_epi
 
 /-- In a `non_preadditive_abelian` category, a monomorphism which is also an epimorphism is an
     isomorphism. -/
-def is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
+lemma is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
 is_iso_of_mono_of_strong_epi _
 
 end mono_epi_iso
@@ -556,7 +556,7 @@ is_iso_of_mono_of_epi _
     followed by the inverse of `r`. In the category of modules, using the normal kernels and
     cokernels, this map is equal to the map `(a, b) ↦ a - b`, hence the name `σ` for
     "subtraction". -/
-abbreviation σ {A : C} : A ⨯ A ⟶ A := cokernel.π (diag A) ≫ is_iso.inv (r A)
+abbreviation σ {A : C} : A ⨯ A ⟶ A := cokernel.π (diag A) ≫ inv (r A)
 
 end
 
diff --git a/src/category_theory/action.lean b/src/category_theory/action.lean
index 2bf3bb2616f49..adb99c81d2c84 100644
--- a/src/category_theory/action.lean
+++ b/src/category_theory/action.lean
@@ -42,6 +42,7 @@ def action_category := (action_as_functor M X).elements
 
 namespace action_category
 
+noncomputable
 instance (G : Type*) [group G] [mul_action G X] : groupoid (action_category G X) :=
 category_theory.groupoid_of_elements _
 
diff --git a/src/category_theory/adjunction/basic.lean b/src/category_theory/adjunction/basic.lean
index 2fd45f409ec4f..af4a1777aed11 100644
--- a/src/category_theory/adjunction/basic.lean
+++ b/src/category_theory/adjunction/basic.lean
@@ -412,6 +412,7 @@ If the unit and counit of a given adjunction are (pointwise) isomorphisms, then
 adjunction to an equivalence.
 -/
 @[simps]
+noncomputable
 def to_equivalence (adj : F ⊣ G) [∀ X, is_iso (adj.unit.app X)] [∀ Y, is_iso (adj.counit.app Y)] :
   C ≌ D :=
 { functor := F,
@@ -424,6 +425,7 @@ If the unit and counit for the adjunction corresponding to a right adjoint funct
 isomorphisms, then the functor is an equivalence of categories.
 -/
 @[simps]
+noncomputable
 def is_right_adjoint_to_is_equivalence [is_right_adjoint G]
   [∀ X, is_iso ((adjunction.of_right_adjoint G).unit.app X)]
   [∀ Y, is_iso ((adjunction.of_right_adjoint G).counit.app Y)] :
diff --git a/src/category_theory/adjunction/fully_faithful.lean b/src/category_theory/adjunction/fully_faithful.lean
index c972a5edba297..a1572f5701a6f 100644
--- a/src/category_theory/adjunction/fully_faithful.lean
+++ b/src/category_theory/adjunction/fully_faithful.lean
@@ -30,20 +30,17 @@ See
 instance unit_is_iso_of_L_fully_faithful [full L] [faithful L] : is_iso (adjunction.unit h) :=
 @nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.unit h) $ λ X,
 @yoneda.is_iso _ _ _ _ ((adjunction.unit h).app X)
-{ inv := { app := λ Y f, L.preimage ((h.hom_equiv (unop Y) (L.obj X)).symm f) },
-  inv_hom_id' :=
-  begin
-    ext, dsimp,
+⟨{ app := λ Y f, L.preimage ((h.hom_equiv (unop Y) (L.obj X)).symm f) },
+  ⟨begin
+    ext x f, dsimp,
+    apply L.map_injective,
+    simp,
+  end, begin
+    ext x f, dsimp,
     simp only [adjunction.hom_equiv_counit, preimage_comp, preimage_map, category.assoc],
     rw ←h.unit_naturality,
     simp,
-  end,
-  hom_inv_id' :=
-  begin
-    ext, dsimp,
-    apply L.map_injective,
-    simp,
-  end }.
+  end⟩⟩
 
 /--
 If the right adjoint is fully faithful, then the counit is an isomorphism.
@@ -54,20 +51,17 @@ instance counit_is_iso_of_R_fully_faithful [full R] [faithful R] : is_iso (adjun
 @nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.counit h) $ λ X,
 @is_iso_of_op _ _ _ _ _ $
 @coyoneda.is_iso _ _ _ _ ((adjunction.counit h).app X).op
-{ inv := { app := λ Y f, R.preimage ((h.hom_equiv (R.obj X) Y) f) },
-  inv_hom_id' :=
-  begin
-    ext, dsimp,
+⟨{ app := λ Y f, R.preimage ((h.hom_equiv (R.obj X) Y) f) },
+  ⟨begin
+    ext x f, dsimp,
+    apply R.map_injective,
+    simp,
+  end, begin
+    ext x f, dsimp,
     simp only [adjunction.hom_equiv_unit, preimage_comp, preimage_map],
     rw ←h.counit_naturality,
     simp,
-  end,
-  hom_inv_id' :=
-  begin
-    ext, dsimp,
-    apply R.map_injective,
-    simp,
-  end }
+  end⟩⟩
 
 -- TODO also prove the converses?
 -- def L_full_of_unit_is_iso [is_iso (adjunction.unit h)] : full L := sorry
diff --git a/src/category_theory/adjunction/mates.lean b/src/category_theory/adjunction/mates.lean
index a9a13c71ec0f3..4edaeb4f8aede 100644
--- a/src/category_theory/adjunction/mates.lean
+++ b/src/category_theory/adjunction/mates.lean
@@ -213,9 +213,8 @@ The converse is given in `transfer_nat_trans_self_of_iso`.
 -/
 instance transfer_nat_trans_self_iso (f : L₂ ⟶ L₁) [is_iso f] :
   is_iso (transfer_nat_trans_self adj₁ adj₂ f) :=
-{ inv := transfer_nat_trans_self adj₂ adj₁ (inv f),
-  hom_inv_id' := transfer_nat_trans_self_comm _ _ (by simp),
-  inv_hom_id' := transfer_nat_trans_self_comm _ _ (by simp) }
+⟨transfer_nat_trans_self adj₂ adj₁ (inv f),
+  ⟨transfer_nat_trans_self_comm _ _ (by simp), transfer_nat_trans_self_comm _ _ (by simp)⟩⟩
 
 /--
 If `f` is an isomorphism, then the un-transferred natural transformation is an isomorphism.
@@ -223,16 +222,16 @@ The converse is given in `transfer_nat_trans_self_symm_of_iso`.
 -/
 instance transfer_nat_trans_self_symm_iso (f : R₁ ⟶ R₂) [is_iso f] :
   is_iso ((transfer_nat_trans_self adj₁ adj₂).symm f) :=
-{ inv := (transfer_nat_trans_self adj₂ adj₁).symm (inv f),
-  hom_inv_id' := transfer_nat_trans_self_symm_comm _ _ (by simp),
-  inv_hom_id' := transfer_nat_trans_self_symm_comm _ _ (by simp) }
+⟨(transfer_nat_trans_self adj₂ adj₁).symm (inv f),
+  ⟨transfer_nat_trans_self_symm_comm _ _ (by simp),
+   transfer_nat_trans_self_symm_comm _ _ (by simp)⟩⟩
 
 /--
 If `f` is a natural transformation whose transferred natural transformation is an isomorphism,
 then `f` is an isomorphism.
 The converse is given in `transfer_nat_trans_self_iso`.
 -/
-def transfer_nat_trans_self_of_iso (f : L₂ ⟶ L₁) [is_iso (transfer_nat_trans_self adj₁ adj₂ f)] :
+lemma transfer_nat_trans_self_of_iso (f : L₂ ⟶ L₁) [is_iso (transfer_nat_trans_self adj₁ adj₂ f)] :
   is_iso f :=
 begin
   suffices :
@@ -246,7 +245,7 @@ If `f` is a natural transformation whose un-transferred natural transformation i
 then `f` is an isomorphism.
 The converse is given in `transfer_nat_trans_self_symm_iso`.
 -/
-def transfer_nat_trans_self_symm_of_iso (f : R₁ ⟶ R₂)
+lemma transfer_nat_trans_self_symm_of_iso (f : R₁ ⟶ R₂)
   [is_iso ((transfer_nat_trans_self adj₁ adj₂).symm f)] :
   is_iso f :=
 begin
diff --git a/src/category_theory/adjunction/opposites.lean b/src/category_theory/adjunction/opposites.lean
index 0955c01ffafe3..0a1be0633ea85 100644
--- a/src/category_theory/adjunction/opposites.lean
+++ b/src/category_theory/adjunction/opposites.lean
@@ -19,6 +19,7 @@ These constructions are used to show uniqueness of adjoints (up to natural isomo
 adjunction, opposite, uniqueness
 -/
 
+
 open category_theory
 
 universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation
diff --git a/src/category_theory/adjunction/reflective.lean b/src/category_theory/adjunction/reflective.lean
index f2d01f82e680a..ce0622537d1ad 100644
--- a/src/category_theory/adjunction/reflective.lean
+++ b/src/category_theory/adjunction/reflective.lean
@@ -70,7 +70,7 @@ reflection of `A`, with the isomorphism as `η_A`.
 
 (For any `B` in the reflective subcategory, we automatically have that `ε_B` is an iso.)
 -/
-def functor.ess_image.unit_is_iso [reflective i] {A : C} (h : A ∈ i.ess_image) :
+lemma functor.ess_image.unit_is_iso [reflective i] {A : C} (h : A ∈ i.ess_image) :
   is_iso ((adjunction.of_right_adjoint i).unit.app A) :=
 begin
   suffices : (adjunction.of_right_adjoint i).unit.app A =
diff --git a/src/category_theory/closed/cartesian.lean b/src/category_theory/closed/cartesian.lean
index e8d4c9a85fa3c..3cbf0119436cf 100644
--- a/src/category_theory/closed/cartesian.lean
+++ b/src/category_theory/closed/cartesian.lean
@@ -316,7 +316,7 @@ i.e. any morphism to `I` is an iso.
 This actually shows a slightly stronger version: any morphism to an initial object from an
 exponentiable object is an isomorphism.
 -/
-def strict_initial {I : C} (t : is_initial I) (f : A ⟶ I) : is_iso f :=
+lemma strict_initial {I : C} (t : is_initial I) (f : A ⟶ I) : is_iso f :=
 begin
   haveI : mono (limits.prod.lift (𝟙 A) f ≫ (zero_mul t).hom) := mono_comp _ _,
   rw [zero_mul_hom, prod.lift_snd] at _inst,
diff --git a/src/category_theory/closed/functor.lean b/src/category_theory/closed/functor.lean
index 33c4e63e9fafc..bb3f509a0ca07 100644
--- a/src/category_theory/closed/functor.lean
+++ b/src/category_theory/closed/functor.lean
@@ -87,12 +87,21 @@ transfer_nat_trans (exp.adjunction A) (exp.adjunction (F.obj A)) (prod_compariso
 lemma exp_comparison_ev (A B : C) :
   limits.prod.map (𝟙 (F.obj A)) ((exp_comparison F A).app B) ≫ (ev (F.obj A)).app (F.obj B) =
     inv (prod_comparison F _ _) ≫ F.map ((ev _).app _) :=
-by convert transfer_nat_trans_counit _ _ (prod_comparison_nat_iso F A).inv B
+begin
+  convert transfer_nat_trans_counit _ _ (prod_comparison_nat_iso F A).inv B,
+  ext,
+  simp,
+end
 
 lemma coev_exp_comparison (A B : C) :
   F.map ((coev A).app B) ≫ (exp_comparison F A).app (A ⨯ B) =
       (coev _).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prod_comparison F A B)) :=
-by convert unit_transfer_nat_trans _ _ (prod_comparison_nat_iso F A).inv B
+begin
+  convert unit_transfer_nat_trans _ _ (prod_comparison_nat_iso F A).inv B,
+  ext,
+  dsimp,
+  simp,
+end
 
 lemma uncurry_exp_comparison (A B : C) :
   uncurry ((exp_comparison F A).app B) = inv (prod_comparison F _ _) ≫ F.map ((ev _).app _) :=
@@ -147,7 +156,7 @@ lemma frobenius_morphism_mate (h : L ⊣ F) (A : C) :
 If the exponential comparison transformation (at `A`) is an isomorphism, then the Frobenius morphism
 at `A` is an isomorphism.
 -/
-def frobenius_morphism_iso_of_exp_comparison_iso (h : L ⊣ F) (A : C)
+lemma frobenius_morphism_iso_of_exp_comparison_iso (h : L ⊣ F) (A : C)
   [i : is_iso (exp_comparison F A)] :
   is_iso (frobenius_morphism F h A) :=
 begin
@@ -159,7 +168,7 @@ end
 If the Frobenius morphism at `A` is an isomorphism, then the exponential comparison transformation
 (at `A`) is an isomorphism.
 -/
-def exp_comparison_iso_of_frobenius_morphism_iso (h : L ⊣ F) (A : C)
+lemma exp_comparison_iso_of_frobenius_morphism_iso (h : L ⊣ F) (A : C)
   [i : is_iso (frobenius_morphism F h A)] :
   is_iso (exp_comparison F A) :=
 by { rw ← frobenius_morphism_mate F h, apply_instance }
diff --git a/src/category_theory/comma.lean b/src/category_theory/comma.lean
index 353c2675b75fe..476c1c7b87219 100644
--- a/src/category_theory/comma.lean
+++ b/src/category_theory/comma.lean
@@ -141,7 +141,10 @@ def iso_mk {X Y : comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.ri
   inv :=
   { left := l.inv,
     right := r.inv,
-    w' := by { erw [L₁.map_inv l.hom, iso.inv_comp_eq, reassoc_of h, ← R₁.map_comp], simp } } }
+    w' := begin
+      rw [←L₁.map_iso_inv l, iso.inv_comp_eq, L₁.map_iso_hom, reassoc_of h, ← R₁.map_comp],
+      simp
+    end, } }
 
 /-- A natural transformation `L₁ ⟶ L₂` induces a functor `comma L₂ R ⥤ comma L₁ R`. -/
 @[simps]
diff --git a/src/category_theory/core.lean b/src/category_theory/core.lean
index 2f7f4b9d56169..9e01e6d2a3ac8 100644
--- a/src/category_theory/core.lean
+++ b/src/category_theory/core.lean
@@ -39,6 +39,7 @@ variables {G : Type u₂} [groupoid.{v₂} G]
 /-- A functor from a groupoid to a category C factors through the core of C. -/
 -- Note that this function is not functorial
 -- (consider the two functors from [0] to [1], and the natural transformation between them).
+noncomputable
 def functor_to_core (F : G ⥤ C) : G ⥤ core C :=
 { obj := λ X, F.obj X,
   map := λ X Y f, ⟨F.map f, F.map (inv f)⟩ }
diff --git a/src/category_theory/currying.lean b/src/category_theory/currying.lean
index dd8b2426069d1..d8d5393b89ee0 100644
--- a/src/category_theory/currying.lean
+++ b/src/category_theory/currying.lean
@@ -93,7 +93,7 @@ The equivalence of functor categories given by currying/uncurrying.
 def currying : (C ⥤ (D ⥤ E)) ≌ ((C × D) ⥤ E) :=
 equivalence.mk uncurry curry
   (nat_iso.of_components (λ F, nat_iso.of_components
-    (λ X, nat_iso.of_components (λ Y, as_iso (𝟙 _)) (by tidy)) (by tidy)) (by tidy))
+    (λ X, nat_iso.of_components (λ Y, iso.refl _) (by tidy)) (by tidy)) (by tidy))
   (nat_iso.of_components (λ F, nat_iso.of_components
     (λ X, eq_to_iso (by simp)) (by tidy)) (by tidy))
 
diff --git a/src/category_theory/discrete_category.lean b/src/category_theory/discrete_category.lean
index 71c68a25a2bae..f246653059dfd 100644
--- a/src/category_theory/discrete_category.lean
+++ b/src/category_theory/discrete_category.lean
@@ -46,7 +46,7 @@ lemma eq_of_hom {X Y : discrete α} (i : X ⟶ Y) : X = Y := i.down.down
 variables {C : Type u₂} [category.{v₂} C]
 
 instance {I : Type u₁} {i j : discrete I} (f : i ⟶ j) : is_iso f :=
-{ inv := eq_to_hom (eq_of_hom f).symm, }
+⟨eq_to_hom (eq_of_hom f).symm, by tidy⟩
 
 /--
 Any function `I → C` gives a functor `discrete I ⥤ C`.
diff --git a/src/category_theory/elements.lean b/src/category_theory/elements.lean
index b73e5d4ef434a..7129cfdba7daa 100644
--- a/src/category_theory/elements.lean
+++ b/src/category_theory/elements.lean
@@ -64,6 +64,7 @@ subtype.ext_val w
 
 end category_of_elements
 
+noncomputable
 instance groupoid_of_elements {G : Type u} [groupoid.{v} G] (F : G ⥤ Type w) :
   groupoid F.elements :=
 { inv := λ p q f, ⟨inv f.val,
diff --git a/src/category_theory/epi_mono.lean b/src/category_theory/epi_mono.lean
index a99725e79cb87..84c73d7f7a9a7 100644
--- a/src/category_theory/epi_mono.lean
+++ b/src/category_theory/epi_mono.lean
@@ -82,9 +82,8 @@ instance retraction_split_epi {X Y : C} (f : X ⟶ Y) [split_mono f] : split_epi
 { section_ := f }
 
 /-- A split mono which is epi is an iso. -/
-def is_iso_of_epi_of_split_mono {X Y : C} (f : X ⟶ Y) [split_mono f] [epi f] : is_iso f :=
-{ inv := retraction f,
-  inv_hom_id' := by simp [← cancel_epi f] }
+lemma is_iso_of_epi_of_split_mono {X Y : C} (f : X ⟶ Y) [split_mono f] [epi f] : is_iso f :=
+⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩
 
 /--
 The chosen section of a split epimorphism.
@@ -99,17 +98,18 @@ instance section_split_mono {X Y : C} (f : X ⟶ Y) [split_epi f] : split_mono (
 { retraction := f }
 
 /-- A split epi which is mono is an iso. -/
-def is_iso_of_mono_of_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [split_epi f] : is_iso f :=
-{ inv := section_ f,
-  hom_inv_id' := by simp [← cancel_mono f] }
+lemma is_iso_of_mono_of_split_epi {X Y : C} (f : X ⟶ Y) [mono f] [split_epi f] : is_iso f :=
+⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩
 
 /-- Every iso is a split mono. -/
 @[priority 100]
+noncomputable
 instance split_mono.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_mono f :=
 { retraction := inv f }
 
 /-- Every iso is a split epi. -/
 @[priority 100]
+noncomputable
 instance split_epi.of_iso {X Y : C} (f : X ⟶ Y) [is_iso f] : split_epi f :=
 { section_ := inv f }
 
@@ -124,16 +124,14 @@ instance split_epi.epi {X Y : C} (f : X ⟶ Y) [split_epi f] : epi f :=
 { left_cancellation := λ Z g h w, begin replace w := section_ f ≫= w, simpa using w, end }
 
 /-- Every split mono whose retraction is mono is an iso. -/
-def is_iso.of_mono_retraction {X Y : C} {f : X ⟶ Y} [split_mono f] [mono $ retraction f]
+lemma is_iso.of_mono_retraction {X Y : C} {f : X ⟶ Y} [split_mono f] [mono $ retraction f]
   : is_iso f :=
-{ inv := retraction f,
-  inv_hom_id' := (cancel_mono_id $ retraction f).mp (by simp) }
+⟨retraction f, ⟨by simp, (cancel_mono_id $ retraction f).mp (by simp)⟩⟩
 
 /-- Every split epi whose section is epi is an iso. -/
-def is_iso.of_epi_section {X Y : C} {f : X ⟶ Y} [split_epi f] [epi $ section_ f]
+lemma is_iso.of_epi_section {X Y : C} {f : X ⟶ Y} [split_epi f] [epi $ section_ f]
   : is_iso f :=
-{ inv := section_ f,
-  hom_inv_id' := (cancel_epi_id $ section_ f).mp (by simp) }
+⟨section_ f, ⟨(cancel_epi_id $ section_ f).mp (by simp), by simp⟩⟩
 
 instance unop_mono_of_epi {A B : Cᵒᵖ} (f : A ⟶ B) [epi f] : mono f.unop :=
 ⟨λ Z g h eq, has_hom.hom.op_inj ((cancel_epi f).1 (has_hom.hom.unop_inj eq))⟩
diff --git a/src/category_theory/eq_to_hom.lean b/src/category_theory/eq_to_hom.lean
index 11c830fc7e065..ee2ab301a6839 100644
--- a/src/category_theory/eq_to_hom.lean
+++ b/src/category_theory/eq_to_hom.lean
@@ -78,9 +78,10 @@ by { cases h, refl, }
   (eq_to_hom h).unop = eq_to_hom (congr_arg unop h.symm) :=
 by { cases h, refl, }
 
-instance {X Y : C} (h : X = Y) : is_iso (eq_to_hom h) := { .. eq_to_iso h }
+instance {X Y : C} (h : X = Y) : is_iso (eq_to_hom h) := is_iso.of_iso (eq_to_iso h)
 
-@[simp] lemma inv_eq_to_hom {X Y : C} (h : X = Y) : inv (eq_to_hom h) = eq_to_hom h.symm := rfl
+@[simp] lemma inv_eq_to_hom {X Y : C} (h : X = Y) : inv (eq_to_hom h) = eq_to_hom h.symm :=
+by { ext, simp, }
 
 variables {D : Type u₂} [category.{v₂} D]
 
diff --git a/src/category_theory/fully_faithful.lean b/src/category_theory/fully_faithful.lean
index dce33a05cf210..14df26f2b959a 100644
--- a/src/category_theory/fully_faithful.lean
+++ b/src/category_theory/fully_faithful.lean
@@ -81,10 +81,9 @@ variables (F)
 If the image of a morphism under a fully faithful functor in an isomorphism,
 then the original morphisms is also an isomorphism.
 -/
-def is_iso_of_fully_faithful (f : X ⟶ Y) [is_iso (F.map f)] : is_iso f :=
-{ inv := F.preimage (inv (F.map f)),
-  hom_inv_id' := F.map_injective (by simp),
-  inv_hom_id' := F.map_injective (by simp) }
+lemma is_iso_of_fully_faithful (f : X ⟶ Y) [is_iso (F.map f)] : is_iso f :=
+⟨F.preimage (inv (F.map f)),
+  ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩
 
 /-- If `F` is fully faithful, we have an equivalence of hom-sets `X ⟶ Y` and `F X ⟶ F Y`. -/
 def equiv_of_fully_faithful {X Y} : (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y) :=
@@ -217,6 +216,7 @@ lemma fully_faithful_cancel_right_hom_app {F G : C ⥤ D} {H : D ⥤ E}
   [full H] [faithful H] (comp_iso: F ⋙ H ≅ G ⋙ H) (X : C) :
   (fully_faithful_cancel_right H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X) :=
 rfl
+
 @[simp]
 lemma fully_faithful_cancel_right_inv_app {F G : C ⥤ D} {H : D ⥤ E}
   [full H] [faithful H] (comp_iso: F ⋙ H ≅ G ⋙ H) (X : C) :
diff --git a/src/category_theory/groupoid.lean b/src/category_theory/groupoid.lean
index 94784ea5cbd5f..421b61ce6c6a8 100644
--- a/src/category_theory/groupoid.lean
+++ b/src/category_theory/groupoid.lean
@@ -36,14 +36,15 @@ section
 variables {C : Type u} [groupoid.{v} C] {X Y : C}
 
 @[priority 100] -- see Note [lower instance priority]
-instance is_iso.of_groupoid (f : X ⟶ Y) : is_iso f := { inv := groupoid.inv f }
+instance is_iso.of_groupoid (f : X ⟶ Y) : is_iso f :=
+⟨groupoid.inv f, by simp⟩
 
 variables (X Y)
 
 /-- In a groupoid, isomorphisms are equivalent to morphisms. -/
 def groupoid.iso_equiv_hom : (X ≅ Y) ≃ (X ⟶ Y) :=
 { to_fun := iso.hom,
-  inv_fun := λ f, as_iso f,
+  inv_fun := λ f, ⟨f, groupoid.inv f⟩,
   left_inv := λ i, iso.ext rfl,
   right_inv := λ f, rfl }
 
@@ -54,10 +55,13 @@ section
 variables {C : Type u} [category.{v} C]
 
 /-- A category where every morphism `is_iso` is a groupoid. -/
+noncomputable
 def groupoid.of_is_iso (all_is_iso : ∀ {X Y : C} (f : X ⟶ Y), is_iso f) : groupoid.{v} C :=
-{ inv := λ X Y f, (all_is_iso f).inv }
+{ inv := λ X Y f, inv f }
 
 /-- A category where every morphism has a `trunc` retraction is computably a groupoid. -/
+-- FIXME this has unnecessarily become noncomputable!
+noncomputable
 def groupoid.of_trunc_split_mono
   (all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), trunc (split_mono f)) :
   groupoid.{v} C :=
diff --git a/src/category_theory/isomorphism.lean b/src/category_theory/isomorphism.lean
index 4d73c78010cd5..916b8cd2ca7bc 100644
--- a/src/category_theory/isomorphism.lean
+++ b/src/category_theory/isomorphism.lean
@@ -13,9 +13,11 @@ This file defines isomorphisms between objects of a category.
 ## Main definitions
 
 - `structure iso` : a bundled isomorphism between two objects of a category;
-- `class is_iso` : an unbundled version of `iso`; note that `is_iso f` is usually *not* a `Prop`,
-  because it holds the inverse morphism;
-- `as_iso` : convert from `is_iso` to `iso`;
+- `class is_iso` : an unbundled version of `iso`;
+  note that `is_iso f` is a `Prop`, and only asserts the existence of an inverse.
+  Of course, this inverse is unique, so it doesn't cost us much to use choice to retrieve it.
+- `inv f`, for the inverse of a morphism with `[is_iso f]`
+- `as_iso` : convert from `is_iso` to `iso` (noncomputable);
 - `of_iso` : convert from `iso` to `is_iso`;
 - standard operations on isomorphisms (composition, inverse etc)
 
@@ -157,41 +159,75 @@ by { erw [inv_eq_inv α.symm β, eq_comm], refl }
 
 end iso
 
-/-- `is_iso` typeclass expressing that a morphism is invertible.
-    This contains the data of the inverse, but is a subsingleton type. -/
-class is_iso (f : X ⟶ Y) :=
-(inv : Y ⟶ X)
-(hom_inv_id' : f ≫ inv = 𝟙 X . obviously)
-(inv_hom_id' : inv ≫ f = 𝟙 Y . obviously)
+/-- `is_iso` typeclass expressing that a morphism is invertible. -/
+def is_iso (f : X ⟶ Y) : Prop := ∃ inv : Y ⟶ X, f ≫ inv = 𝟙 X ∧ inv ≫ f = 𝟙 Y
+
+attribute [class] is_iso
+
+/--
+The inverse of a morphism `f` when we have `[is_iso f]`.
+-/
+noncomputable def inv (f : X ⟶ Y) [I : is_iso f] := classical.some I
+
+namespace is_iso
+
+@[simp, reassoc] lemma hom_inv_id (f : X ⟶ Y) [I : is_iso f] : f ≫ inv f = 𝟙 X :=
+(classical.some_spec I).left
+@[simp, reassoc] lemma inv_hom_id (f : X ⟶ Y) [I : is_iso f] : inv f ≫ f = 𝟙 Y :=
+(classical.some_spec I).right
+
+end is_iso
 
-export is_iso (inv)
+open is_iso
 
 /-- Reinterpret a morphism `f` with an `is_iso f` instance as an `iso`. -/
-def as_iso (f : X ⟶ Y) [h : is_iso f] : X ≅ Y := { hom := f, ..h }
+noncomputable
+def as_iso (f : X ⟶ Y) [h : is_iso f] : X ≅ Y := ⟨f, inv f, hom_inv_id f, inv_hom_id f⟩
 
 @[simp] lemma as_iso_hom (f : X ⟶ Y) [is_iso f] : (as_iso f).hom = f := rfl
 @[simp] lemma as_iso_inv (f : X ⟶ Y) [is_iso f] : (as_iso f).inv = inv f := rfl
 
 namespace is_iso
 
-@[simp] lemma hom_inv_id (f : X ⟶ Y) [is_iso f] : f ≫ inv f = 𝟙 X :=
-is_iso.hom_inv_id'
-@[simp] lemma inv_hom_id (f : X ⟶ Y) [is_iso f] : inv f ≫ f = 𝟙 Y :=
-is_iso.inv_hom_id'
+@[priority 100] -- see Note [lower instance priority]
+instance epi_of_iso (f : X ⟶ Y) [is_iso f] : epi f  :=
+{ left_cancellation := λ Z g h w,
+  -- This is an interesting test case for better rewrite automation.
+  by rw [← is_iso.inv_hom_id_assoc f g, w, is_iso.inv_hom_id_assoc f h] }
+@[priority 100] -- see Note [lower instance priority]
+instance mono_of_iso (f : X ⟶ Y) [is_iso f] : mono f :=
+{ right_cancellation := λ Z g h w,
+  by rw [← category.comp_id g, ← category.comp_id h, ← is_iso.hom_inv_id f, ← category.assoc, w,
+    ← category.assoc] }
+
+@[ext] lemma inv_eq_of_hom_inv_id {f : X ⟶ Y} [is_iso f] {g : Y ⟶ X}
+  (hom_inv_id : f ≫ g = 𝟙 X) : inv f = g :=
+begin
+  apply (cancel_epi f).mp,
+  simp [hom_inv_id],
+end
+
+lemma inv_eq_of_inv_hom_id {f : X ⟶ Y} [is_iso f] {g : Y ⟶ X}
+  (inv_hom_id : g ≫ f = 𝟙 Y) : inv f = g :=
+begin
+  apply (cancel_mono f).mp,
+  simp [inv_hom_id],
+end
+
+@[ext] lemma eq_inv_of_hom_inv_id {f : X ⟶ Y} [is_iso f] {g : Y ⟶ X}
+  (hom_inv_id : f ≫ g = 𝟙 X) : g = inv f :=
+(inv_eq_of_hom_inv_id hom_inv_id).symm
 
-@[simp] lemma hom_inv_id_assoc {Z} (f : X ⟶ Y) [is_iso f] (g : X ⟶ Z) :
-  f ≫ inv f ≫ g = g :=
-(as_iso f).hom_inv_id_assoc g
+lemma eq_inv_of_inv_hom_id {f : X ⟶ Y} [is_iso f] {g : Y ⟶ X}
+  (inv_hom_id : g ≫ f = 𝟙 Y) : g = inv f :=
+(inv_eq_of_inv_hom_id inv_hom_id).symm
 
-@[simp] lemma inv_hom_id_assoc {Z} (f : X ⟶ Y) [is_iso f] (g : Y ⟶ Z) :
-  inv f ≫ f ≫ g = g :=
-(as_iso f).inv_hom_id_assoc g
 
 instance id (X : C) : is_iso (𝟙 X) :=
-{ inv := 𝟙 X }
+⟨𝟙 X, by simp⟩
 
 instance of_iso (f : X ≅ Y) : is_iso f.hom :=
-{ .. f }
+⟨f.inv, by simp⟩
 
 instance of_iso_inv (f : X ≅ Y) : is_iso f.inv :=
 is_iso.of_iso f.symm
@@ -204,11 +240,11 @@ is_iso.of_iso_inv (as_iso f)
 instance comp_is_iso [is_iso f] [is_iso h] : is_iso (f ≫ h) :=
 is_iso.of_iso $ (as_iso f) ≪≫ (as_iso h)
 
-@[simp] lemma inv_id : inv (𝟙 X) = 𝟙 X := rfl
-@[simp] lemma inv_comp [is_iso f] [is_iso h] : inv (f ≫ h) = inv h ≫ inv f := rfl
-@[simp] lemma inv_inv [is_iso f] : inv (inv f) = f := rfl
-@[simp] lemma iso.inv_inv (f : X ≅ Y) : inv (f.inv) = f.hom := rfl
-@[simp] lemma iso.inv_hom (f : X ≅ Y) : inv (f.hom) = f.inv := rfl
+@[simp] lemma inv_id : inv (𝟙 X) = 𝟙 X := by { ext, simp, }
+@[simp] lemma inv_comp [is_iso f] [is_iso h] : inv (f ≫ h) = inv h ≫ inv f := by { ext, simp, }
+@[simp] lemma inv_inv [is_iso f] : inv (inv f) = f := by { ext, simp, }
+@[simp] lemma iso.inv_inv (f : X ≅ Y) : inv (f.inv) = f.hom := by { ext, simp, }
+@[simp] lemma iso.inv_hom (f : X ≅ Y) : inv (f.hom) = f.inv := by { ext, simp, }
 
 @[simp]
 lemma inv_comp_eq (α : X ⟶ Y) [is_iso α] {f : X ⟶ Z} {g : Y ⟶ Z} : inv α ≫ f = g ↔ f = α ≫ g :=
@@ -226,17 +262,6 @@ 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
 
-@[priority 100] -- see Note [lower instance priority]
-instance epi_of_iso (f : X ⟶ Y) [is_iso f] : epi f  :=
-{ left_cancellation := λ Z g h w,
-  -- This is an interesting test case for better rewrite automation.
-  by rw [← is_iso.inv_hom_id_assoc f g, w, is_iso.inv_hom_id_assoc f h] }
-@[priority 100] -- see Note [lower instance priority]
-instance mono_of_iso (f : X ⟶ Y) [is_iso f] : mono f :=
-{ right_cancellation := λ Z g h w,
-  by rw [← category.comp_id g, ← category.comp_id h, ← is_iso.hom_inv_id f, ← category.assoc, w,
-    ← category.assoc] }
-
 end is_iso
 
 open is_iso
@@ -247,12 +272,6 @@ begin
   erw [inv_hom_id, p, inv_hom_id],
 end
 
-instance (f : X ⟶ Y) : subsingleton (is_iso f) :=
-⟨λ a b,
- suffices a.inv = b.inv, by cases a; cases b; congr; exact this,
- show (@as_iso C _ _ _ f a).inv = (@as_iso C _ _ _ f b).inv,
- by congr' 1; ext; refl⟩
-
 lemma is_iso.inv_eq_inv {f g : X ⟶ Y} [is_iso f] [is_iso g] : inv f = inv g ↔ f = g :=
 iso.inv_eq_inv (as_iso f) (as_iso g)
 
@@ -264,6 +283,17 @@ lemma comp_hom_eq_id (g : X ⟶ Y) [is_iso g] {f : Y ⟶ X} : f ≫ g = 𝟙 Y 
 
 namespace iso
 
+@[ext] lemma inv_ext {f : X ≅ Y} {g : Y ⟶ X}
+  (hom_inv_id : f.hom ≫ g = 𝟙 X) : f.inv = g :=
+begin
+  apply (cancel_epi f.hom).mp,
+  simp [hom_inv_id],
+end
+
+@[ext] lemma inv_ext' {f : X ≅ Y} {g : Y ⟶ X}
+  (hom_inv_id : f.hom ≫ g = 𝟙 X) : g = f.inv :=
+by { symmetry, ext, assumption, }
+
 /-!
 All these cancellation lemmas can be solved by `simp [cancel_mono]` (or `simp [cancel_epi]`),
 but with the current design `cancel_mono` is not a good `simp` lemma,
@@ -323,15 +353,13 @@ variables {D : Type u₂}
 variables [category.{v₂} D]
 
 /-- A functor `F : C ⥤ D` sends isomorphisms `i : X ≅ Y` to isomorphisms `F.obj X ≅ F.obj Y` -/
+@[simps]
 def map_iso (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : F.obj X ≅ F.obj Y :=
 { hom := F.map i.hom,
   inv := F.map i.inv,
   hom_inv_id' := by rw [←map_comp, iso.hom_inv_id, ←map_id],
   inv_hom_id' := by rw [←map_comp, iso.inv_hom_id, ←map_id] }
 
-@[simp] lemma map_iso_hom (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F.map_iso i).hom = F.map i.hom := rfl
-@[simp] lemma map_iso_inv (F : C ⥤ D) {X Y : C} (i : X ≅ Y) : (F.map_iso i).inv = F.map i.inv := rfl
-
 @[simp] lemma map_iso_symm (F : C ⥤ D) {X Y : C} (i : X ≅ Y) :
   F.map_iso i.symm = (F.map_iso i).symm :=
 rfl
@@ -348,7 +376,7 @@ is_iso.of_iso $ F.map_iso (as_iso f)
 
 @[simp] lemma map_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] :
   F.map (inv f) = inv (F.map f) :=
-rfl
+by { ext, simp [←F.map_comp], }
 
 lemma map_hom_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] :
   F.map f ≫ F.map (inv f) = 𝟙 (F.obj X) :=
diff --git a/src/category_theory/limits/cofinal.lean b/src/category_theory/limits/cofinal.lean
index 75e5b54bf5ec9..cc5d8e5e8efc9 100644
--- a/src/category_theory/limits/cofinal.lean
+++ b/src/category_theory/limits/cofinal.lean
@@ -303,7 +303,7 @@ begin
   dsimp [is_colimit_whisker_equiv],
   apply P.hom_ext,
   intro j,
-  dsimp, simp,
+  dsimp, simp, dsimp, simp, -- See library note [dsimp, simp].
 end
 
 instance colimit_pre_is_iso [has_colimit G] :
diff --git a/src/category_theory/limits/cones.lean b/src/category_theory/limits/cones.lean
index dbdea4a4a988c..11736101d4480 100644
--- a/src/category_theory/limits/cones.lean
+++ b/src/category_theory/limits/cones.lean
@@ -204,11 +204,10 @@ namespace cones
 Given a cone morphism whose object part is an isomorphism, produce an
 isomorphism of cones.
 -/
-def cone_iso_of_hom_iso {K : J ⥤ C} {c d : cone K} (f : c ⟶ d) [i : is_iso f.hom] :
+lemma cone_iso_of_hom_iso {K : J ⥤ C} {c d : cone K} (f : c ⟶ d) [i : is_iso f.hom] :
   is_iso f :=
-{ inv :=
-  { hom := i.inv,
-    w' := λ j, (as_iso f.hom).inv_comp_eq.2 (f.w j).symm } }
+⟨{ hom := inv f.hom,
+   w' := λ j, (as_iso f.hom).inv_comp_eq.2 (f.w j).symm }, by tidy⟩
 
 /--
 Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to give a cone for `G`.
@@ -368,11 +367,10 @@ namespace cocones
 Given a cocone morphism whose object part is an isomorphism, produce an
 isomorphism of cocones.
 -/
-def cocone_iso_of_hom_iso {K : J ⥤ C} {c d : cocone K} (f : c ⟶ d) [i : is_iso f.hom] :
+lemma cocone_iso_of_hom_iso {K : J ⥤ C} {c d : cocone K} (f : c ⟶ d) [i : is_iso f.hom] :
   is_iso f :=
-{ inv :=
-  { hom := i.inv,
-    w' := λ j, (as_iso f.hom).comp_inv_eq.2 (f.w j).symm } }
+⟨{ hom := inv f.hom,
+   w' := λ j, (as_iso f.hom).comp_inv_eq.2 (f.w j).symm }, by tidy⟩
 
 /-- Functorially precompose a cocone for `F` by a natural transformation `G ⟶ F` to give a cocone
 for `G`. -/
@@ -487,7 +485,8 @@ let f : (F ⋙ e.functor) ⋙ e.inverse ≅ F :=
     simp only [←equivalence.counit_inv_app_functor, iso.inv_hom_id_app, map_comp,
       equivalence.fun_inv_map, assoc, id_comp, iso.inv_hom_id_app_assoc],
     dsimp, simp, -- See note [dsimp, simp].
-  end) (by tidy), }
+  end)
+  (λ c c' f, by { ext, dsimp, simp, dsimp, simp, }), }
 
 /--
 If `F` reflects isomorphisms, then `cocones.functoriality F` reflects isomorphisms
diff --git a/src/category_theory/limits/filtered_colimit_commutes_finite_limit.lean b/src/category_theory/limits/filtered_colimit_commutes_finite_limit.lean
index 58acc9dc3933c..4bded6371f99d 100644
--- a/src/category_theory/limits/filtered_colimit_commutes_finite_limit.lean
+++ b/src/category_theory/limits/filtered_colimit_commutes_finite_limit.lean
@@ -295,10 +295,9 @@ begin
     simp only [bifunctor.map_id_comp, types_comp_apply, bifunctor.map_id, types_id_apply], },
 end
 
-noncomputable
 instance colimit_limit_to_limit_colimit_is_iso :
   is_iso (colimit_limit_to_limit_colimit F) :=
-(is_iso_equiv_bijective _).symm
+(is_iso_iff_bijective _).mpr
   ⟨colimit_limit_to_limit_colimit_injective F, colimit_limit_to_limit_colimit_surjective F⟩
 
 end category_theory.limits
diff --git a/src/category_theory/limits/limits.lean b/src/category_theory/limits/limits.lean
index d544b59ad61c6..d6de964bb76ff 100644
--- a/src/category_theory/limits/limits.lean
+++ b/src/category_theory/limits/limits.lean
@@ -143,10 +143,8 @@ def unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s ≅ t
   inv_hom_id' := Q.uniq_cone_morphism }
 
 /-- Any cone morphism between limit cones is an isomorphism. -/
-def hom_is_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) (f : s ⟶ t) : is_iso f :=
-{ inv := P.lift_cone_morphism t,
-  hom_inv_id' := P.uniq_cone_morphism,
-  inv_hom_id' := Q.uniq_cone_morphism, }
+lemma hom_is_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) (f : s ⟶ t) : is_iso f :=
+⟨P.lift_cone_morphism t, ⟨P.uniq_cone_morphism, Q.uniq_cone_morphism⟩⟩
 
 /-- Limits of `F` are unique up to isomorphism. -/
 def cone_point_unique_up_to_iso {s t : cone F} (P : is_limit s) (Q : is_limit t) : s.X ≅ t.X :=
@@ -558,10 +556,8 @@ def unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) : s
   inv_hom_id' := Q.uniq_cocone_morphism }
 
 /-- Any cocone morphism between colimit cocones is an isomorphism. -/
-def hom_is_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) (f : s ⟶ t) : is_iso f :=
-{ inv := Q.desc_cocone_morphism s,
-  hom_inv_id' := P.uniq_cocone_morphism,
-  inv_hom_id' := Q.uniq_cocone_morphism, }
+lemma hom_is_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) (f : s ⟶ t) : is_iso f :=
+⟨Q.desc_cocone_morphism s, ⟨P.uniq_cocone_morphism, Q.uniq_cocone_morphism⟩⟩
 
 /-- Colimits of `F` are unique up to isomorphism. -/
 def cocone_point_unique_up_to_iso {s t : cocone F} (P : is_colimit s) (Q : is_colimit t) :
diff --git a/src/category_theory/limits/shapes/binary_products.lean b/src/category_theory/limits/shapes/binary_products.lean
index 07f2236964fa6..3e47600dc7fba 100644
--- a/src/category_theory/limits/shapes/binary_products.lean
+++ b/src/category_theory/limits/shapes/binary_products.lean
@@ -815,7 +815,7 @@ def prod_comparison_nat_iso [has_binary_products C] [has_binary_products D]
   (A : C) [∀ B, is_iso (prod_comparison F A B)] :
   prod.functor.obj A ⋙ F ≅ F ⋙ prod.functor.obj (F.obj A) :=
 { hom := prod_comparison_nat_trans F A
-  ..nat_iso.is_iso_of_is_iso_app ⟨_, _⟩ }
+  ..(@as_iso _ _ _ _ _ (nat_iso.is_iso_of_is_iso_app ⟨_, _⟩)) }
 
 end prod_comparison
 
diff --git a/src/category_theory/limits/shapes/equalizers.lean b/src/category_theory/limits/shapes/equalizers.lean
index 4994b98870ccf..59db0fa38f902 100644
--- a/src/category_theory/limits/shapes/equalizers.lean
+++ b/src/category_theory/limits/shapes/equalizers.lean
@@ -523,21 +523,21 @@ fork.is_limit.mk _
   (λ s m h, by { convert h zero, exact (category.comp_id _).symm })
 
 /-- Every equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
-def is_iso_limit_cone_parallel_pair_of_eq (h₀ : f = g) {c : cone (parallel_pair f g)}
+lemma is_iso_limit_cone_parallel_pair_of_eq (h₀ : f = g) {c : cone (parallel_pair f g)}
   (h : is_limit c) : is_iso (c.π.app zero) :=
 is_iso.of_iso $ is_limit.cone_point_unique_up_to_iso h $ is_limit_id_fork h₀
 
 /-- The equalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
-def equalizer.ι_of_eq [has_equalizer f g] (h : f = g) : is_iso (equalizer.ι f g) :=
+lemma equalizer.ι_of_eq [has_equalizer f g] (h : f = g) : is_iso (equalizer.ι f g) :=
 is_iso_limit_cone_parallel_pair_of_eq h $ limit.is_limit _
 
 /-- Every equalizer of `(f, f)` is an isomorphism. -/
-def is_iso_limit_cone_parallel_pair_of_self {c : cone (parallel_pair f f)} (h : is_limit c) :
+lemma is_iso_limit_cone_parallel_pair_of_self {c : cone (parallel_pair f f)} (h : is_limit c) :
   is_iso (c.π.app zero) :=
 is_iso_limit_cone_parallel_pair_of_eq rfl h
 
 /-- An equalizer that is an epimorphism is an isomorphism. -/
-def is_iso_limit_cone_parallel_pair_of_epi {c : cone (parallel_pair f g)}
+lemma is_iso_limit_cone_parallel_pair_of_epi {c : cone (parallel_pair f g)}
   (h : is_limit c) [epi (c.π.app zero)] : is_iso (c.π.app zero) :=
 is_iso_limit_cone_parallel_pair_of_eq ((cancel_epi _).1 (fork.condition c)) h
 
@@ -562,7 +562,7 @@ rfl
 
 @[simp] lemma equalizer.iso_source_of_self_inv :
   (equalizer.iso_source_of_self f).inv = equalizer.lift (𝟙 X) (by simp) :=
-rfl
+by { ext, simp [equalizer.iso_source_of_self], }
 
 section
 /--
@@ -656,22 +656,22 @@ cofork.is_colimit.mk _
   (λ s m h, by { convert h one, exact (category.id_comp _).symm })
 
 /-- Every coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
-def is_iso_colimit_cocone_parallel_pair_of_eq (h₀ : f = g) {c : cocone (parallel_pair f g)}
+lemma is_iso_colimit_cocone_parallel_pair_of_eq (h₀ : f = g) {c : cocone (parallel_pair f g)}
   (h : is_colimit c) : is_iso (c.ι.app one) :=
 is_iso.of_iso $ is_colimit.cocone_point_unique_up_to_iso (is_colimit_id_cofork h₀) h
 
 /-- The coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
-def coequalizer.π_of_eq [has_coequalizer f g] (h : f = g) :
+lemma coequalizer.π_of_eq [has_coequalizer f g] (h : f = g) :
   is_iso (coequalizer.π f g) :=
 is_iso_colimit_cocone_parallel_pair_of_eq h $ colimit.is_colimit _
 
 /-- Every coequalizer of `(f, f)` is an isomorphism. -/
-def is_iso_colimit_cocone_parallel_pair_of_self {c : cocone (parallel_pair f f)}
+lemma is_iso_colimit_cocone_parallel_pair_of_self {c : cocone (parallel_pair f f)}
   (h : is_colimit c) : is_iso (c.ι.app one) :=
 is_iso_colimit_cocone_parallel_pair_of_eq rfl h
 
 /-- A coequalizer that is a monomorphism is an isomorphism. -/
-def is_iso_limit_cocone_parallel_pair_of_epi {c : cocone (parallel_pair f g)}
+lemma is_iso_limit_cocone_parallel_pair_of_epi {c : cocone (parallel_pair f g)}
   (h : is_colimit c) [mono (c.ι.app one)] : is_iso (c.ι.app one) :=
 is_iso_colimit_cocone_parallel_pair_of_eq ((cancel_mono _).1 (cofork.condition c)) h
 
@@ -692,7 +692,7 @@ def coequalizer.iso_target_of_self : coequalizer f f ≅ Y :=
 
 @[simp] lemma coequalizer.iso_target_of_self_hom :
   (coequalizer.iso_target_of_self f).hom = coequalizer.desc (𝟙 Y) (by simp) :=
-rfl
+by { ext, simp [coequalizer.iso_target_of_self], }
 
 @[simp] lemma coequalizer.iso_target_of_self_inv :
   (coequalizer.iso_target_of_self f).inv = coequalizer.π f f :=
diff --git a/src/category_theory/limits/shapes/images.lean b/src/category_theory/limits/shapes/images.lean
index 34a0ac8272bb2..da30e39b67f8e 100644
--- a/src/category_theory/limits/shapes/images.lean
+++ b/src/category_theory/limits/shapes/images.lean
@@ -314,9 +314,9 @@ image.lift
   e := factor_thru_image f', }.
 
 instance (h : f = f') : is_iso (image.eq_to_hom h) :=
-{ inv := image.eq_to_hom h.symm,
-  hom_inv_id' := (cancel_mono (image.ι f)).1 (by simp [image.eq_to_hom]),
-  inv_hom_id' := (cancel_mono (image.ι f')).1 (by simp [image.eq_to_hom]), }
+⟨image.eq_to_hom h.symm,
+  ⟨(cancel_mono (image.ι f)).1 (by simp [image.eq_to_hom]),
+   (cancel_mono (image.ι f')).1 (by simp [image.eq_to_hom])⟩⟩
 
 /-- An equation between morphisms gives an isomorphism between the images. -/
 def image.eq_to_iso (h : f = f') : image f ≅ image f' := as_iso (image.eq_to_hom h)
@@ -370,12 +370,11 @@ variables [has_equalizers C]
 -/
 instance image.is_iso_precomp_iso (f : X ≅ Y) [has_image g] [has_image (f.hom ≫ g)] :
   is_iso (image.pre_comp f.hom g) :=
-{ inv := image.lift
+⟨image.lift
   { I := image (f.hom ≫ g),
     m := image.ι (f.hom ≫ g),
     e := f.inv ≫ factor_thru_image (f.hom ≫ g) },
-  hom_inv_id' := by { ext, simp [image.pre_comp], },
-  inv_hom_id' := by { ext, simp [image.pre_comp], }, }
+  ⟨by { ext, simp [image.pre_comp], }, by { ext, simp [image.pre_comp], }⟩⟩
 
 -- Note that in general we don't have the other comparison map you might expect
 -- `image f ⟶ image (f ≫ g)`.
diff --git a/src/category_theory/limits/shapes/kernels.lean b/src/category_theory/limits/shapes/kernels.lean
index 1e3ba29caebd6..520cab4d5e01a 100644
--- a/src/category_theory/limits/shapes/kernels.lean
+++ b/src/category_theory/limits/shapes/kernels.lean
@@ -192,7 +192,8 @@ equalizer.iso_source_of_self 0
   kernel_zero_iso_source.hom = kernel.ι (0 : X ⟶ Y) := rfl
 
 @[simp] lemma kernel_zero_iso_source_inv :
-  kernel_zero_iso_source.inv = kernel.lift (0 : X ⟶ Y) (𝟙 X) (by simp) := rfl
+  kernel_zero_iso_source.inv = kernel.lift (0 : X ⟶ Y) (𝟙 X) (by simp) :=
+by { ext, simp [kernel_zero_iso_source], }
 
 /-- If two morphisms are known to be equal, then their kernels are isomorphic. -/
 def kernel_iso_of_eq {f g : X ⟶ Y} [has_kernel f] [has_kernel g] (h : f = g) :
@@ -328,7 +329,7 @@ section
 variables (X Y)
 
 /-- The kernel morphism of a zero morphism is an isomorphism -/
-def kernel.ι_of_zero : is_iso (kernel.ι (0 : X ⟶ Y)) :=
+lemma kernel.ι_of_zero : is_iso (kernel.ι (0 : X ⟶ Y)) :=
 equalizer.ι_of_self _
 
 end
@@ -450,7 +451,8 @@ def cokernel_zero_iso_target : cokernel (0 : X ⟶ Y) ≅ Y :=
 coequalizer.iso_target_of_self 0
 
 @[simp] lemma cokernel_zero_iso_target_hom :
-  cokernel_zero_iso_target.hom = cokernel.desc (0 : X ⟶ Y) (𝟙 Y) (by simp) := rfl
+  cokernel_zero_iso_target.hom = cokernel.desc (0 : X ⟶ Y) (𝟙 Y) (by simp) :=
+by { ext, simp [cokernel_zero_iso_target], }
 
 @[simp] lemma cokernel_zero_iso_target_inv :
   cokernel_zero_iso_target.inv = cokernel.π (0 : X ⟶ Y) := rfl
@@ -583,7 +585,7 @@ section
 variables (X Y)
 
 /-- The cokernel of a zero morphism is an isomorphism -/
-def cokernel.π_of_zero :
+lemma cokernel.π_of_zero :
   is_iso (cokernel.π (0 : X ⟶ Y)) :=
 coequalizer.π_of_self _
 
diff --git a/src/category_theory/limits/shapes/regular_mono.lean b/src/category_theory/limits/shapes/regular_mono.lean
index 46c4eeba01eee..27563a5727377 100644
--- a/src/category_theory/limits/shapes/regular_mono.lean
+++ b/src/category_theory/limits/shapes/regular_mono.lean
@@ -115,7 +115,7 @@ regular_mono f :=
 regular_of_is_pullback_snd_of_regular comm.symm (pullback_cone.flip_is_limit t)
 
 /-- A regular monomorphism is an isomorphism if it is an epimorphism. -/
-def is_iso_of_regular_mono_of_epi (f : X ⟶ Y) [regular_mono f] [e : epi f] : is_iso f :=
+lemma is_iso_of_regular_mono_of_epi (f : X ⟶ Y) [regular_mono f] [e : epi f] : is_iso f :=
 @is_iso_limit_cone_parallel_pair_of_epi _ _ _ _ _ _ _ regular_mono.is_limit e
 
 /-- A regular epimorphism is a morphism which is the coequalizer of some parallel pair. -/
@@ -201,7 +201,7 @@ regular_epi k :=
 regular_of_is_pushout_snd_of_regular comm.symm (pushout_cocone.flip_is_colimit t)
 
 /-- A regular epimorphism is an isomorphism if it is a monomorphism. -/
-def is_iso_of_regular_epi_of_mono (f : X ⟶ Y) [regular_epi f] [m : mono f] : is_iso f :=
+lemma is_iso_of_regular_epi_of_mono (f : X ⟶ Y) [regular_epi f] [m : mono f] : is_iso f :=
 @is_iso_limit_cocone_parallel_pair_of_epi _ _ _ _ _ _ _ regular_epi.is_colimit m
 
 @[priority 100]
diff --git a/src/category_theory/limits/shapes/strong_epi.lean b/src/category_theory/limits/shapes/strong_epi.lean
index af6de75368ec4..ba3ba7c3e67d7 100644
--- a/src/category_theory/limits/shapes/strong_epi.lean
+++ b/src/category_theory/limits/shapes/strong_epi.lean
@@ -82,7 +82,7 @@ lemma strong_epi_of_strong_epi [strong_epi (f ≫ g)] : strong_epi g :=
 end
 
 /-- A strong epimorphism that is a monomorphism is an isomorphism. -/
-noncomputable def is_iso_of_mono_of_strong_epi (f : P ⟶ Q) [mono f] [strong_epi f] : is_iso f :=
-{ inv := arrow.lift $ arrow.hom_mk' $ show 𝟙 P ≫ f = f ≫ 𝟙 Q, by simp }
+lemma is_iso_of_mono_of_strong_epi (f : P ⟶ Q) [mono f] [strong_epi f] : is_iso f :=
+⟨arrow.lift $ arrow.hom_mk' $ show 𝟙 P ≫ f = f ≫ 𝟙 Q, by simp, by tidy⟩
 
 end category_theory
diff --git a/src/category_theory/limits/shapes/zero.lean b/src/category_theory/limits/shapes/zero.lean
index cf61dfca9e4f9..54c2a6f22020c 100644
--- a/src/category_theory/limits/shapes/zero.lean
+++ b/src/category_theory/limits/shapes/zero.lean
@@ -292,7 +292,7 @@ the identities on both `X` and `Y` are zero.
 def is_iso_zero_equiv (X Y : C) : is_iso (0 : X ⟶ Y) ≃ (𝟙 X = 0 ∧ 𝟙 Y = 0) :=
 { to_fun := by { introsI i, rw ←is_iso.hom_inv_id (0 : X ⟶ Y),
     rw ←is_iso.inv_hom_id (0 : X ⟶ Y), simp },
-  inv_fun := λ h, { inv := (0 : Y ⟶ X), },
+  inv_fun := λ h, ⟨(0 : Y ⟶ X), by tidy⟩,
   left_inv := by tidy,
   right_inv := by tidy, }
 
diff --git a/src/category_theory/monad/adjunction.lean b/src/category_theory/monad/adjunction.lean
index 66c33af29f3aa..3d81685974b1e 100644
--- a/src/category_theory/monad/adjunction.lean
+++ b/src/category_theory/monad/adjunction.lean
@@ -117,17 +117,14 @@ namespace reflective
 
 instance [reflective R] (X : (adjunction.of_right_adjoint R).to_monad.algebra) :
   is_iso ((adjunction.of_right_adjoint R).unit.app X.A) :=
-{ inv := X.a,
-  hom_inv_id' := X.unit,
-  inv_hom_id' :=
-  begin
+⟨X.a, ⟨X.unit, begin
     dsimp only [functor.id_obj],
     rw ← (adjunction.of_right_adjoint R).unit_naturality,
     dsimp only [functor.comp_obj, adjunction.to_monad_coe],
     rw [unit_obj_eq_map_unit, ←functor.map_comp, ←functor.map_comp],
     erw X.unit,
     simp,
-  end }
+  end⟩⟩
 
 instance comparison_ess_surj [reflective R] :
   ess_surj (monad.comparison (adjunction.of_right_adjoint R)) :=
diff --git a/src/category_theory/monad/algebra.lean b/src/category_theory/monad/algebra.lean
index 923043ea19341..4db185dd9cf6e 100644
--- a/src/category_theory/monad/algebra.lean
+++ b/src/category_theory/monad/algebra.lean
@@ -141,10 +141,9 @@ adjunction.mk_of_hom_equiv
 /--
 Given an algebra morphism whose carrier part is an isomorphism, we get an algebra isomorphism.
 -/
-def algebra_iso_of_iso {A B : algebra T} (f : A ⟶ B) [is_iso f.f] : is_iso f :=
-{ inv :=
-  { f := inv f.f,
-    h' := by { rw [is_iso.eq_comp_inv f.f, category.assoc, ← f.h], dsimp, simp } } }
+lemma algebra_iso_of_iso {A B : algebra T} (f : A ⟶ B) [is_iso f.f] : is_iso f :=
+⟨{ f := inv f.f,
+   h' := by { rw [is_iso.eq_comp_inv f.f, category.assoc, ← f.h], dsimp, simp } }, by tidy⟩
 
 instance forget_reflects_iso : reflects_isomorphisms (forget T) :=
 { reflects := λ A B, algebra_iso_of_iso T }
@@ -303,10 +302,9 @@ structure. -/
 /--
 Given a coalgebra morphism whose carrier part is an isomorphism, we get a coalgebra isomorphism.
 -/
-def coalgebra_iso_of_iso {A B : coalgebra G} (f : A ⟶ B) [is_iso f.f] : is_iso f :=
-{ inv :=
-  { f := inv f.f,
-    h' := by { rw [is_iso.eq_inv_comp f.f, ←f.h_assoc], dsimp, simp } } }
+lemma coalgebra_iso_of_iso {A B : coalgebra G} (f : A ⟶ B) [is_iso f.f] : is_iso f :=
+⟨{ f := inv f.f,
+   h' := by { rw [is_iso.eq_inv_comp f.f, ←f.h_assoc], dsimp, simp } }, by tidy⟩
 
 instance forget_reflects_iso : reflects_isomorphisms (forget G) :=
 { reflects := λ A B, coalgebra_iso_of_iso G }
diff --git a/src/category_theory/monad/limits.lean b/src/category_theory/monad/limits.lean
index c9fd490c2c6de..0a3cc1396f151 100644
--- a/src/category_theory/monad/limits.lean
+++ b/src/category_theory/monad/limits.lean
@@ -95,6 +95,7 @@ end forget_creates_limits
 
 -- Theorem 5.6.5 from [Riehl][riehl2017]
 /-- The forgetful functor from the Eilenberg-Moore category creates limits. -/
+noncomputable
 instance forget_creates_limits : creates_limits (forget T) :=
 { creates_limits_of_shape := λ J 𝒥, by exactI
   { creates_limit := λ D,
@@ -226,6 +227,7 @@ open forget_creates_colimits
 The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit
 which the monad itself preserves.
 -/
+noncomputable
 instance forget_creates_colimit (D : J ⥤ algebra T)
   [preserves_colimit (D ⋙ forget T) (T : C ⥤ C)]
   [preserves_colimit ((D ⋙ forget T) ⋙ ↑T) (T : C ⥤ C)] :
@@ -239,11 +241,13 @@ creates_colimit_of_reflects_iso $ λ c t,
   valid_lift := cocones.ext (iso.refl _) (by tidy),
   makes_colimit := lifted_cocone_is_colimit _ _ }
 
+noncomputable
 instance forget_creates_colimits_of_shape
   [preserves_colimits_of_shape J (T : C ⥤ C)] :
   creates_colimits_of_shape J (forget T) :=
 { creates_colimit := λ K, by apply_instance }
 
+noncomputable
 instance forget_creates_colimits
   [preserves_colimits (T : C ⥤ C)] :
   creates_colimits (forget T) :=
@@ -275,6 +279,7 @@ instance comp_comparison_has_limit
 monad.has_limit_of_comp_forget_has_limit (F ⋙ monad.comparison (adjunction.of_right_adjoint R))
 
 /-- Any monadic functor creates limits. -/
+noncomputable
 def monadic_creates_limits (R : D ⥤ C) [monadic_right_adjoint R] :
   creates_limits R :=
 creates_limits_of_nat_iso (monad.comparison_forget (adjunction.of_right_adjoint R))
@@ -283,6 +288,7 @@ creates_limits_of_nat_iso (monad.comparison_forget (adjunction.of_right_adjoint
 The forgetful functor from the Eilenberg-Moore category for a monad creates any colimit
 which the monad itself preserves.
 -/
+noncomputable
 def monadic_creates_colimit_of_preserves_colimit (R : D ⥤ C) (K : J ⥤ D)
   [monadic_right_adjoint R]
   [preserves_colimit (K ⋙ R) (left_adjoint R ⋙ R)]
@@ -303,6 +309,7 @@ begin
 end
 
 /-- A monadic functor creates any colimits of shapes it preserves. -/
+noncomputable
 def monadic_creates_colimits_of_shape_of_preserves_colimits_of_shape (R : D ⥤ C)
   [monadic_right_adjoint R] [preserves_colimits_of_shape J R] : creates_colimits_of_shape J R :=
 begin
@@ -315,6 +322,7 @@ begin
 end
 
 /-- A monadic functor creates colimits if it preserves colimits. -/
+noncomputable
 def monadic_creates_colimits_of_preserves_colimits (R : D ⥤ C) [monadic_right_adjoint R]
   [preserves_colimits R] : creates_colimits R :=
 { creates_colimits_of_shape := λ J 𝒥₁,
diff --git a/src/category_theory/monoidal/End.lean b/src/category_theory/monoidal/End.lean
index cc4bbe18d6e7f..0b7ef4873ded0 100644
--- a/src/category_theory/monoidal/End.lean
+++ b/src/category_theory/monoidal/End.lean
@@ -63,11 +63,11 @@ def tensoring_right_monoidal : monoidal_functor C (C ⥤ C) :=
   end,
   ε_is_iso := by apply_instance,
   μ_is_iso := λ X Y,
-  { inv :=
     -- We could avoid needing to do this explicitly by
     -- constructing a partially applied analogue of `associator_nat_iso`.
-    { app := λ Z, (α_ Z X Y).inv,
-      naturality' := λ Z Z' f, by { dsimp, rw ←associator_inv_naturality, simp, } }, },
+  ⟨{ app := λ Z, (α_ Z X Y).inv,
+      naturality' := λ Z Z' f, by { dsimp, rw ←associator_inv_naturality, simp, } },
+    by tidy⟩,
   ..tensoring_right C }.
 
 end category_theory
diff --git a/src/category_theory/monoidal/Mon_.lean b/src/category_theory/monoidal/Mon_.lean
index 7edbf17bd7ce7..537b26003102b 100644
--- a/src/category_theory/monoidal/Mon_.lean
+++ b/src/category_theory/monoidal/Mon_.lean
@@ -118,14 +118,13 @@ instance {A B : Mon_ C} (f : A ⟶ B) [e : is_iso ((forget C).map f)] : is_iso f
 
 /-- The forgetful functor from monoid objects to the ambient category reflects isomorphisms. -/
 instance : reflects_isomorphisms (forget C) :=
-{ reflects := λ X Y f e, by exactI
-  { inv :=
-    { hom := inv f.hom,
-      mul_hom' :=
-      begin
-        simp only [is_iso.comp_inv_eq, hom.mul_hom, category.assoc, ←tensor_comp_assoc,
-          is_iso.inv_hom_id, tensor_id, category.id_comp],
-      end } } }
+{ reflects := λ X Y f e, by exactI ⟨{
+  hom := inv f.hom,
+  mul_hom' :=
+  begin
+    simp only [is_iso.comp_inv_eq, hom.mul_hom, category.assoc, ←tensor_comp_assoc,
+      is_iso.inv_hom_id, tensor_id, category.id_comp],
+  end }, by tidy⟩ }
 
 instance unique_hom_from_trivial (A : Mon_ C) : unique (trivial C ⟶ A) :=
 { default :=
diff --git a/src/category_theory/monoidal/category.lean b/src/category_theory/monoidal/category.lean
index a9ea8ac9d2d84..2c6b1989c8850 100644
--- a/src/category_theory/monoidal/category.lean
+++ b/src/category_theory/monoidal/category.lean
@@ -151,10 +151,11 @@ variables {C : Type u} [category.{v} C] [monoidal_category.{v} C]
 
 instance tensor_is_iso {W X Y Z : C} (f : W ⟶ X) [is_iso f] (g : Y ⟶ Z) [is_iso g] :
   is_iso (f ⊗ g) :=
-{ ..(as_iso f ⊗ as_iso g) }
+is_iso.of_iso (as_iso f ⊗ as_iso g)
 
 @[simp] lemma inv_tensor {W X Y Z : C} (f : W ⟶ X) [is_iso f] (g : Y ⟶ Z) [is_iso g] :
-  inv (f ⊗ g) = inv f ⊗ inv g := rfl
+  inv (f ⊗ g) = inv f ⊗ inv g :=
+by { ext, simp [←tensor_comp], }
 
 variables {U V W X Y Z : C}
 
@@ -374,8 +375,7 @@ lemma pentagon_inv (W X Y Z : C) :
     = (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv :=
 begin
   apply category_theory.eq_of_inv_eq_inv,
-  dsimp,
-  rw [category.assoc, monoidal_category.pentagon]
+  simp [monoidal_category.pentagon]
 end
 
 lemma triangle_assoc_comp_left (X Y : C) :
@@ -493,7 +493,7 @@ nat_iso.of_components
 rfl
 @[simp] lemma tensor_left_tensor_inv_app (X Y Z : C) :
   (tensor_left_tensor X Y).inv.app Z = (associator X Y Z).inv :=
-rfl
+by { simp [tensor_left_tensor], }
 
 /-- Tensoring on the right with a fixed object, as a functor. -/
 @[simps]
@@ -538,7 +538,7 @@ nat_iso.of_components
 rfl
 @[simp] lemma tensor_right_tensor_inv_app (X Y Z : C) :
   (tensor_right_tensor X Y).inv.app Z = (associator Z X Y).hom :=
-rfl
+by simp [tensor_right_tensor]
 
 end
 
diff --git a/src/category_theory/monoidal/functor.lean b/src/category_theory/monoidal/functor.lean
index 9c15f78506d26..146e8ccd0a692 100644
--- a/src/category_theory/monoidal/functor.lean
+++ b/src/category_theory/monoidal/functor.lean
@@ -109,12 +109,15 @@ variables {C D}
 /--
 The unit morphism of a (strong) monoidal functor as an isomorphism.
 -/
+noncomputable
 def monoidal_functor.ε_iso (F : monoidal_functor.{v₁ v₂} C D) :
   tensor_unit D ≅ F.obj (tensor_unit C) :=
 as_iso F.ε
+
 /--
 The tensorator of a (strong) monoidal functor as an isomorphism.
 -/
+noncomputable
 def monoidal_functor.μ_iso (F : monoidal_functor.{v₁ v₂} C D) (X Y : C) :
   (F.obj X) ⊗ (F.obj Y) ≅ F.obj (X ⊗ Y) :=
 as_iso (F.μ X Y)
@@ -164,6 +167,7 @@ begin
 end
 
 /-- The tensorator as a natural isomorphism. -/
+noncomputable
 def μ_nat_iso (F : monoidal_functor.{v₁ v₂} C D) :
   (functor.prod F.to_functor F.to_functor) ⋙ (tensor D) ≅ (tensor C) ⋙ F.to_functor :=
 nat_iso.of_components
@@ -258,6 +262,7 @@ If we have a right adjoint functor `G` to a monoidal functor `F`, then `G` has a
 structure as well.
 -/
 @[simps]
+noncomputable
 def monoidal_adjoint (F : monoidal_functor C D) {G : D ⥤ C} (h : F.to_functor ⊣ G) :
   lax_monoidal_functor D C :=
 { to_functor := G,
@@ -304,6 +309,7 @@ def monoidal_adjoint (F : monoidal_functor C D) {G : D ⥤ C} (h : F.to_functor
   end }.
 
 /-- If a monoidal functor `F` is an equivalence of categories then its inverse is also monoidal. -/
+noncomputable
 def monoidal_inverse (F : monoidal_functor C D) [is_equivalence F.to_functor] :
   monoidal_functor D C :=
 { to_lax_monoidal_functor := monoidal_adjoint F (as_equivalence _).to_adjunction,
diff --git a/src/category_theory/monoidal/functor_category.lean b/src/category_theory/monoidal/functor_category.lean
index d9ae2aec6ffd1..2800c914e10e9 100644
--- a/src/category_theory/monoidal/functor_category.lean
+++ b/src/category_theory/monoidal/functor_category.lean
@@ -116,11 +116,13 @@ lemma right_unitor_inv_app {F : C ⥤ D} {X} :
 
 @[simp]
 lemma associator_hom_app {F G H : C ⥤ D} {X} :
-  ((α_ F G H).hom : (F ⊗ G) ⊗ H ⟶ F ⊗ (G ⊗ H)).app X = (α_ (F.obj X) (G.obj X) (H.obj X)).hom := rfl
+  ((α_ F G H).hom : (F ⊗ G) ⊗ H ⟶ F ⊗ (G ⊗ H)).app X = (α_ (F.obj X) (G.obj X) (H.obj X)).hom :=
+rfl
 
 @[simp]
 lemma associator_inv_app {F G H : C ⥤ D} {X} :
-  ((α_ F G H).inv : F ⊗ (G ⊗ H) ⟶ (F ⊗ G) ⊗ H).app X = (α_ (F.obj X) (G.obj X) (H.obj X)).inv := rfl
+  ((α_ F G H).inv : F ⊗ (G ⊗ H) ⟶ (F ⊗ G) ⊗ H).app X = (α_ (F.obj X) (G.obj X) (H.obj X)).inv :=
+rfl
 
 section braided_category
 
diff --git a/src/category_theory/monoidal/natural_transformation.lean b/src/category_theory/monoidal/natural_transformation.lean
index c54a1f8f74939..da34e4f8887d0 100644
--- a/src/category_theory/monoidal/natural_transformation.lean
+++ b/src/category_theory/monoidal/natural_transformation.lean
@@ -109,23 +109,6 @@ namespace monoidal_nat_iso
 
 variables {F G : lax_monoidal_functor C D}
 
-instance is_iso_of_is_iso_app (α : F ⟶ G) [∀ X : C, is_iso (α.app X)] : is_iso α :=
-{ inv :=
-  { app := λ X, inv (α.app X),
-    naturality' := λ X Y f,
-    begin
-      have h := congr_arg (λ f, inv (α.app X) ≫ (f ≫ inv (α.app Y)))
-        (α.to_nat_trans.naturality f).symm,
-      simp only [is_iso.inv_hom_id_assoc, is_iso.hom_inv_id, assoc, comp_id, cancel_mono] at h,
-      exact h
-    end,
-    tensor' := λ X Y,
-    begin
-      dsimp,
-      rw [is_iso.comp_inv_eq, assoc, monoidal_nat_trans.tensor, ←inv_tensor,
-        is_iso.inv_hom_id_assoc],
-    end }, }
-
 /--
 Construct a monoidal natural isomorphism from object level isomorphisms,
 and the monoidal naturality in the forward direction.
@@ -136,14 +119,29 @@ def of_components
   (unit : F.ε ≫ (app (𝟙_ C)).hom = G.ε)
   (tensor : ∀ X Y, F.μ X Y ≫ (app (X ⊗ Y)).hom = ((app X).hom ⊗ (app Y).hom) ≫ G.μ X Y) :
   F ≅ G :=
-as_iso { app := λ X, (app X).hom }
+{ hom := { app := λ X, (app X).hom, },
+  inv :=
+  { app := λ X, (app X).inv,
+    unit' := by { dsimp, rw [←unit, assoc, iso.hom_inv_id, comp_id], },
+    tensor' := λ X Y,
+    begin
+      dsimp,
+      rw [iso.comp_inv_eq, assoc, tensor, ←tensor_comp_assoc,
+        iso.inv_hom_id, iso.inv_hom_id, tensor_id, id_comp],
+    end,
+    ..(nat_iso.of_components app @naturality).inv, }, }
 
 @[simp] lemma of_components.hom_app
   (app : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (unit) (tensor) (X) :
   (of_components app naturality unit tensor).hom.app X = (app X).hom := rfl
 @[simp] lemma of_components.inv_app
   (app : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (unit) (tensor) (X) :
-  (of_components app naturality unit tensor).inv.app X = (app X).inv := rfl
+  (of_components app naturality unit tensor).inv.app X = (app X).inv :=
+by simp [of_components]
+
+instance is_iso_of_is_iso_app (α : F ⟶ G) [∀ X : C, is_iso (α.app X)] : is_iso α :=
+is_iso.of_iso
+  (of_components (λ X, as_iso (α.app X)) (λ X Y f, α.to_nat_trans.naturality f) α.unit α.tensor)
 
 end monoidal_nat_iso
 
diff --git a/src/category_theory/natural_isomorphism.lean b/src/category_theory/natural_isomorphism.lean
index deec92b254f73..55d1b7c2f3c93 100644
--- a/src/category_theory/natural_isomorphism.lean
+++ b/src/category_theory/natural_isomorphism.lean
@@ -76,13 +76,12 @@ lemma app_inv {F G : C ⥤ D} (α : F ≅ G) (X : C) : (α.app X).inv = α.inv.a
 variables {F G : C ⥤ D}
 
 instance hom_app_is_iso (α : F ≅ G) (X : C) : is_iso (α.hom.app X) :=
-{ inv := α.inv.app X,
-  hom_inv_id' := begin rw [←comp_app, iso.hom_inv_id, ←id_app] end,
-  inv_hom_id' := begin rw [←comp_app, iso.inv_hom_id, ←id_app] end }
+⟨α.inv.app X,
+  ⟨by rw [←comp_app, iso.hom_inv_id, ←id_app], by rw [←comp_app, iso.inv_hom_id, ←id_app]⟩⟩
+
 instance inv_app_is_iso (α : F ≅ G) (X : C) : is_iso (α.inv.app X) :=
-{ inv := α.hom.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 }
+⟨α.hom.app X,
+  ⟨by rw [←comp_app, iso.inv_hom_id, ←id_app], by rw [←comp_app, iso.hom_inv_id, ←id_app]⟩⟩
 
 section
 /-!
@@ -129,34 +128,21 @@ end
 variables {X Y : C}
 lemma naturality_1 (α : F ≅ G) (f : X ⟶ Y) :
   (α.inv.app X) ≫ (F.map f) ≫ (α.hom.app Y) = G.map f :=
-begin erw [naturality, ←category.assoc, is_iso.hom_inv_id, category.id_comp] end
+by rw [naturality, ←category.assoc, ←nat_trans.comp_app, α.inv_hom_id, id_app, category.id_comp]
 lemma naturality_2 (α : F ≅ G) (f : X ⟶ Y) :
   (α.hom.app X) ≫ (G.map f) ≫ (α.inv.app Y) = F.map f :=
-begin erw [naturality, ←category.assoc, is_iso.hom_inv_id, category.id_comp] end
-
-/--
-A natural transformation is an isomorphism if all its components are isomorphisms.
--/
--- Making this an instance would cause a typeclass inference loop with `is_iso_app_of_is_iso`.
-def is_iso_of_is_iso_app (α : F ⟶ G) [∀ X : C, is_iso (α.app X)] : is_iso α :=
-{ inv :=
-  { app := λ X, inv (α.app X),
-    naturality' := λ X Y f,
-    begin
-      have h := congr_arg (λ f, inv (α.app X) ≫ (f ≫ inv (α.app Y))) (α.naturality f).symm,
-      simp only [is_iso.inv_hom_id_assoc, is_iso.hom_inv_id, assoc, comp_id, cancel_mono] at h,
-      exact h
-    end } }
+by rw [naturality, ←category.assoc, ←nat_trans.comp_app, α.hom_inv_id, id_app, category.id_comp]
 
 /--
 The components of a natural isomorphism are isomorphisms.
 -/
 instance is_iso_app_of_is_iso (α : F ⟶ G) [is_iso α] (X) : is_iso (α.app X) :=
-{ inv := (inv α).app X,
-  hom_inv_id' := congr_fun (congr_arg nat_trans.app (is_iso.hom_inv_id α)) X,
-  inv_hom_id' := congr_fun (congr_arg nat_trans.app (is_iso.inv_hom_id α)) X }
+⟨(inv α).app X,
+  ⟨congr_fun (congr_arg nat_trans.app (is_iso.hom_inv_id α)) X,
+   congr_fun (congr_arg nat_trans.app (is_iso.inv_hom_id α)) X⟩⟩
 
-@[simp] lemma is_iso_inv_app (α : F ⟶ G) [is_iso α] (X) : (inv α).app X = inv (α.app X) := rfl
+@[simp] lemma is_iso_inv_app (α : F ⟶ G) [is_iso α] (X) : (inv α).app X = inv (α.app X) :=
+by { ext, rw ←nat_trans.comp_app, simp, }
 
 /--
 Construct a natural isomorphism between functors by giving object level isomorphisms,
@@ -165,7 +151,15 @@ and checking naturality only in the forward direction.
 def of_components (app : ∀ X : C, F.obj X ≅ G.obj X)
   (naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f) :
   F ≅ G :=
-{ hom := { app := λ X, (app X).hom }, ..is_iso_of_is_iso_app _ }
+{ hom := { app := λ X, (app X).hom },
+  inv :=
+  { app := λ X, (app X).inv,
+    naturality' := λ X Y f,
+    begin
+      have h := congr_arg (λ f, (app X).inv ≫ (f ≫ (app Y).inv)) (naturality f).symm,
+      simp only [iso.inv_hom_id_assoc, iso.hom_inv_id, assoc, comp_id, cancel_mono] at h,
+      exact h
+    end }, }
 
 @[simp] lemma of_components.app (app' : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) :
   (of_components app' naturality).app X = app' X :=
@@ -173,7 +167,15 @@ by tidy
 @[simp] lemma of_components.hom_app (app : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) :
   (of_components app naturality).hom.app X = (app X).hom := rfl
 @[simp] lemma of_components.inv_app (app : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X) :
-  (of_components app naturality).inv.app X = (app X).inv := rfl
+  (of_components app naturality).inv.app X = (app X).inv :=
+by simp [of_components]
+
+/--
+A natural transformation is an isomorphism if all its components are isomorphisms.
+-/
+-- Making this an instance would cause a typeclass inference loop with `is_iso_app_of_is_iso`.
+lemma is_iso_of_is_iso_app (α : F ⟶ G) [∀ X : C, is_iso (α.app X)] : is_iso α :=
+is_iso.of_iso (of_components (λ X, as_iso (α.app X)) (by tidy))
 
 /-- Horizontal composition of natural isomorphisms. -/
 def hcomp {F G : C ⥤ D} {H I : D ⥤ E} (α : F ≅ G) (β : H ≅ I) : F ⋙ H ≅ G ⋙ I :=
diff --git a/src/category_theory/opposites.lean b/src/category_theory/opposites.lean
index 1a8ca6c6ff483..8014808200316 100644
--- a/src/category_theory/opposites.lean
+++ b/src/category_theory/opposites.lean
@@ -102,10 +102,9 @@ end
 If `f.op` is an isomorphism `f` must be too.
 (This cannot be an instance as it would immediately loop!)
 -/
-def is_iso_of_op {X Y : C} (f : X ⟶ Y) [is_iso f.op] : is_iso f :=
-{ inv := (inv (f.op)).unop,
-  hom_inv_id' := has_hom.hom.op_inj (by simp),
-  inv_hom_id' := has_hom.hom.op_inj (by simp) }
+lemma is_iso_of_op {X Y : C} (f : X ⟶ Y) [is_iso f.op] : is_iso f :=
+⟨(inv (f.op)).unop,
+  ⟨has_hom.hom.op_inj (by simp), has_hom.hom.op_inj (by simp)⟩⟩
 
 namespace functor
 
diff --git a/src/category_theory/over.lean b/src/category_theory/over.lean
index 43be2fd9d3b2d..e3bc5ab363051 100644
--- a/src/category_theory/over.lean
+++ b/src/category_theory/over.lean
@@ -130,7 +130,8 @@ end
 
 instance forget_reflects_iso : reflects_isomorphisms (forget X) :=
 { reflects := λ Y Z f t, by exactI
-  { inv := over.hom_mk t.inv ((as_iso ((forget X).map f)).inv_comp_eq.2 (over.w f).symm) } }
+  ⟨over.hom_mk (inv ((forget X).map f)) ((as_iso ((forget X).map f)).inv_comp_eq.2 (over.w f).symm),
+   by tidy⟩ }
 
 instance forget_faithful : faithful (forget X) := {}.
 
diff --git a/src/category_theory/preadditive/biproducts.lean b/src/category_theory/preadditive/biproducts.lean
index 565b1742dd75f..796635fe296bc 100644
--- a/src/category_theory/preadditive/biproducts.lean
+++ b/src/category_theory/preadditive/biproducts.lean
@@ -54,24 +54,22 @@ If
 ```
 is invertible, then `f` is invertible.
 -/
-def is_iso_left_of_is_iso_biprod_map
+lemma is_iso_left_of_is_iso_biprod_map
   {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [is_iso (biprod.map f g)] : is_iso f :=
-{ inv := biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst,
-  hom_inv_id' :=
-  begin
+⟨biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst,
+  ⟨begin
     have t := congr_arg (λ p : W ⊞ X ⟶ W ⊞ X, biprod.inl ≫ p ≫ biprod.fst)
       (is_iso.hom_inv_id (biprod.map f g)),
     simp only [category.id_comp, category.assoc, biprod.inl_map_assoc] at t,
     simp [t],
   end,
-  inv_hom_id' :=
   begin
     have t := congr_arg (λ p : Y ⊞ Z ⟶ Y ⊞ Z, biprod.inl ≫ p ≫ biprod.fst)
       (is_iso.inv_hom_id (biprod.map f g)),
     simp only [category.id_comp, category.assoc, biprod.map_fst] at t,
     simp only [category.assoc],
     simp [t],
-  end }
+  end⟩⟩
 
 /--
 If
@@ -81,7 +79,7 @@ If
 ```
 is invertible, then `g` is invertible.
 -/
-def is_iso_right_of_is_iso_biprod_map
+lemma is_iso_right_of_is_iso_biprod_map
   {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [is_iso (biprod.map f g)] : is_iso g :=
 begin
   letI : is_iso (biprod.map g f) := by
diff --git a/src/category_theory/preadditive/schur.lean b/src/category_theory/preadditive/schur.lean
index 722297b787175..18eb795314490 100644
--- a/src/category_theory/preadditive/schur.lean
+++ b/src/category_theory/preadditive/schur.lean
@@ -38,7 +38,7 @@ variables [preadditive C] [has_kernels C]
 Schur's Lemma (for a general preadditive category),
 that a nonzero morphism between simple objects is an isomorphism.
 -/
-def is_iso_of_hom_simple {X Y : C} [simple X] [simple Y] {f : X ⟶ Y} (w : f ≠ 0) :
+lemma is_iso_of_hom_simple {X Y : C} [simple X] [simple Y] {f : X ⟶ Y} (w : f ≠ 0) :
   is_iso f :=
 begin
   haveI : mono f := preadditive.mono_of_kernel_zero (kernel_zero_of_nonzero_from_simple w),
diff --git a/src/category_theory/products/associator.lean b/src/category_theory/products/associator.lean
index 89ce847feeaf1..429dbc51729a2 100644
--- a/src/category_theory/products/associator.lean
+++ b/src/category_theory/products/associator.lean
@@ -5,7 +5,7 @@ Authors: Stephen Morgan, Scott Morrison
 -/
 import category_theory.products.basic
 
-/-#
+/-!
 The associator functor `((C × D) × E) ⥤ (C × (D × E))` and its inverse form an equivalence.
 -/
 
diff --git a/src/category_theory/reflects_isomorphisms.lean b/src/category_theory/reflects_isomorphisms.lean
index f2cd3a2afb3a3..a4ff876700ef9 100644
--- a/src/category_theory/reflects_isomorphisms.lean
+++ b/src/category_theory/reflects_isomorphisms.lean
@@ -25,7 +25,7 @@ class reflects_isomorphisms (F : C ⥤ D) :=
 (reflects : Π {A B : C} (f : A ⟶ B) [is_iso (F.map f)], is_iso f)
 
 /-- If `F` reflects isos and `F.map f` is an iso, then `f` is an iso. -/
-def is_iso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D)
+lemma is_iso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D)
   [is_iso (F.map f)] [reflects_isomorphisms F] :
   is_iso f :=
 reflects_isomorphisms.reflects F f
@@ -33,9 +33,7 @@ reflects_isomorphisms.reflects F f
 @[priority 100]
 instance of_full_and_faithful (F : C ⥤ D) [full F] [faithful F] : reflects_isomorphisms F :=
 { reflects := λ X Y f i, by exactI
-  { inv := F.preimage (inv (F.map f)),
-    hom_inv_id' := F.map_injective (by simp),
-    inv_hom_id' := F.map_injective (by simp), } }
+  ⟨F.preimage (inv (F.map f)), ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩ }
 
 end reflects_iso
 
diff --git a/src/category_theory/simple.lean b/src/category_theory/simple.lean
index 2b71e823f1bda..999c89e3f611e 100644
--- a/src/category_theory/simple.lean
+++ b/src/category_theory/simple.lean
@@ -20,24 +20,13 @@ section
 variables [has_zero_morphisms C]
 
 /-- An object is simple if monomorphisms into it are (exclusively) either isomorphisms or zero. -/
--- This is a constructive definition, from which we can extract an inverse for `f` given `f ≠ 0`.
--- We show below that although it contains data, it is a subsingleton.
-class simple (X : C) : Type (max u v) :=
-(mono_is_iso_equiv_nonzero : ∀ {Y : C} (f : Y ⟶ X) [mono f], is_iso f ≃ (f ≠ 0))
-
-@[ext] lemma simple.ext {X : C} {a b : simple X} : a = b :=
-begin
-  casesI a, casesI b,
-  congr,
-end
-
-instance subsingleton_simple (X : C) : subsingleton (simple X) :=
-subsingleton.intro (@simple.ext _ _ _ X)
+class simple (X : C) : Prop :=
+(mono_is_iso_iff_nonzero : ∀ {Y : C} (f : Y ⟶ X) [mono f], is_iso f ↔ (f ≠ 0))
 
 /-- A nonzero monomorphism to a simple object is an isomorphism. -/
-def is_iso_of_mono_of_nonzero {X Y : C} [simple Y] {f : X ⟶ Y} [mono f] (w : f ≠ 0) :
+lemma is_iso_of_mono_of_nonzero {X Y : C} [simple Y] {f : X ⟶ Y} [mono f] (w : f ≠ 0) :
   is_iso f :=
-(simple.mono_is_iso_equiv_nonzero f).symm w
+(simple.mono_is_iso_iff_nonzero f).mpr w
 
 lemma kernel_zero_of_nonzero_from_simple
   {X Y : C} [simple X] {f : X ⟶ Y} [has_kernel f] (w : f ≠ 0) :
@@ -59,7 +48,7 @@ begin
 end
 
 lemma id_nonzero (X : C) [simple.{v} X] : 𝟙 X ≠ 0 :=
-(simple.mono_is_iso_equiv_nonzero (𝟙 X)) (by apply_instance)
+(simple.mono_is_iso_iff_nonzero (𝟙 X)).mp (by apply_instance)
 
 section
 variable [has_zero_object C]
@@ -67,7 +56,7 @@ local attribute [instance] has_zero_object.has_zero
 
 /-- We don't want the definition of 'simple' to include the zero object, so we check that here. -/
 lemma zero_not_simple [simple (0 : C)] : false :=
-(simple.mono_is_iso_equiv_nonzero (0 : (0 : C) ⟶ (0 : C))) { inv := 0, } rfl
+(simple.mono_is_iso_iff_nonzero (0 : (0 : C) ⟶ (0 : C))).mp ⟨0, by tidy⟩ rfl
 
 end
 end
@@ -78,28 +67,28 @@ variables [abelian C]
 
 /-- In an abelian category, an object satisfying the dual of the definition of a simple object is
     simple. -/
-def simple_of_cosimple (X : C) (h : ∀ {Z : C} (f : X ⟶ Z) [epi f], is_iso f ≃ (f ≠ 0)) :
+lemma simple_of_cosimple (X : C) (h : ∀ {Z : C} (f : X ⟶ Z) [epi f], is_iso f ↔ (f ≠ 0)) :
   simple X :=
 ⟨λ Y f I,
  begin
   classical,
-  apply equiv_of_subsingleton_of_subsingleton,
+  fsplit,
   { introsI,
     have hx := cokernel.π_of_epi f,
     by_contradiction h,
     push_neg at h,
     substI h,
-    exact h _ (cokernel.π_of_zero _ _) hx },
+    exact (h _).mp (cokernel.π_of_zero _ _) hx },
   { intro hf,
     suffices : epi f,
     { resetI, apply abelian.is_iso_of_mono_of_epi },
     apply preadditive.epi_of_cokernel_zero,
     by_contradiction h',
-    exact cokernel_not_iso_of_nonzero hf ((h _).symm h') }
+    exact cokernel_not_iso_of_nonzero hf ((h _).mpr h') }
  end⟩
 
 /-- A nonzero epimorphism from a simple object is an isomorphism. -/
-def is_iso_of_epi_of_nonzero {X Y : C} [simple X] {f : X ⟶ Y} [epi f] (w : f ≠ 0) :
+lemma is_iso_of_epi_of_nonzero {X Y : C} [simple X] {f : X ⟶ Y} [epi f] (w : f ≠ 0) :
   is_iso f :=
 begin
   -- `f ≠ 0` means that `kernel.ι f` is not an iso, and hence zero, and hence `f` is a mono.
diff --git a/src/category_theory/sites/pretopology.lean b/src/category_theory/sites/pretopology.lean
index a41c4b122a794..2dc74b4d5ac36 100644
--- a/src/category_theory/sites/pretopology.lean
+++ b/src/category_theory/sites/pretopology.lean
@@ -208,7 +208,7 @@ def trivial : pretopology C :=
   begin
     rintro ⟨Z, g, i, rfl⟩,
     refine ⟨pullback g f, pullback.snd, _, _⟩,
-    { exactI { is_iso . inv := pullback.lift (f ≫ inv g) (𝟙 _) (by simp), hom_inv_id' := _ },
+    { resetI, refine ⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨_, by tidy⟩⟩,
       apply pullback.hom_ext,
       { rw [assoc, pullback.lift_fst, ←pullback.condition_assoc],
         simp },
diff --git a/src/category_theory/sites/sieves.lean b/src/category_theory/sites/sieves.lean
index 2043ff7498b63..b890267a824f0 100644
--- a/src/category_theory/sites/sieves.lean
+++ b/src/category_theory/sites/sieves.lean
@@ -407,7 +407,7 @@ begin
 end
 
 instance functor_inclusion_top_is_iso : is_iso ((⊤ : sieve X).functor_inclusion) :=
-{ inv := { app := λ Y a, ⟨a, ⟨⟩⟩ } }
+⟨{ app := λ Y a, ⟨a, ⟨⟩⟩ }, by tidy⟩
 
 end sieve
 end category_theory
diff --git a/src/category_theory/subterminal.lean b/src/category_theory/subterminal.lean
index e23b134fcb501..b71d9444767ea 100644
--- a/src/category_theory/subterminal.lean
+++ b/src/category_theory/subterminal.lean
@@ -83,10 +83,9 @@ lemma is_subterminal_of_terminal [has_terminal C] : is_subterminal (⊤_ C) :=
 If `A` is subterminal, its diagonal morphism is an isomorphism.
 The converse of `is_subterminal_of_is_iso_diag`.
 -/
-def is_subterminal.is_iso_diag (hA : is_subterminal A) [has_binary_product A A] :
+lemma is_subterminal.is_iso_diag (hA : is_subterminal A) [has_binary_product A A] :
   is_iso (diag A) :=
-{ inv := limits.prod.fst,
-  inv_hom_id' := by { rw is_subterminal.def at hA, tidy } }
+⟨limits.prod.fst, ⟨by simp, by { rw is_subterminal.def at hA, tidy }⟩⟩
 
 /--
 If the diagonal morphism of `A` is an isomorphism, then it is subterminal.
diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean
index ed0d159202683..a06682dcfc936 100644
--- a/src/category_theory/types.lean
+++ b/src/category_theory/types.lean
@@ -273,11 +273,10 @@ end category_theory.iso
 namespace category_theory
 
 /-- A morphism in `Type u` is an isomorphism if and only if it is bijective. -/
-noncomputable
-def is_iso_equiv_bijective {X Y : Type u} (f : X ⟶ Y) : is_iso f ≃ function.bijective f :=
-equiv_of_subsingleton_of_subsingleton
-  (λ i, ({ hom := f, .. i } : X ≅ Y).to_equiv.bijective)
-  (λ b, { .. (equiv.of_bijective f b).to_iso })
+lemma is_iso_iff_bijective {X Y : Type u} (f : X ⟶ Y) : is_iso f ↔ function.bijective f :=
+iff.intro
+  (λ i, (by exactI as_iso f : X ≅ Y).to_equiv.bijective)
+  (λ b, is_iso.of_iso (equiv.of_bijective f b).to_iso)
 
 end category_theory
 
diff --git a/src/category_theory/whiskering.lean b/src/category_theory/whiskering.lean
index 9dc645734c777..f63f6ec9a485e 100644
--- a/src/category_theory/whiskering.lean
+++ b/src/category_theory/whiskering.lean
@@ -117,10 +117,10 @@ rfl
 
 instance is_iso_whisker_left (F : C ⥤ D) {G H : D ⥤ E} (α : G ⟶ H) [is_iso α] :
   is_iso (whisker_left F α) :=
-{ .. iso_whisker_left F (as_iso α) }
+is_iso.of_iso (iso_whisker_left F (as_iso α))
 instance is_iso_whisker_right {G H : C ⥤ D} (α : G ⟶ H) (F : D ⥤ E) [is_iso α] :
   is_iso (whisker_right α F) :=
-{ .. iso_whisker_right (as_iso α) F }
+is_iso.of_iso (iso_whisker_right (as_iso α) F)
 
 variables {B : Type u₄} [category.{v₄} B]
 
diff --git a/src/category_theory/yoneda.lean b/src/category_theory/yoneda.lean
index 97e27f21af2a8..50a56fd8c5a52 100644
--- a/src/category_theory/yoneda.lean
+++ b/src/category_theory/yoneda.lean
@@ -99,7 +99,7 @@ def ext (X Y : C)
 /--
 If `yoneda.map f` is an isomorphism, so was `f`.
 -/
-def is_iso {X Y : C} (f : X ⟶ Y) [is_iso (yoneda.map f)] : is_iso f :=
+lemma is_iso {X Y : C} (f : X ⟶ Y) [is_iso (yoneda.map f)] : is_iso f :=
 is_iso_of_fully_faithful yoneda f
 
 end yoneda
@@ -124,7 +124,7 @@ instance coyoneda_faithful : faithful (@coyoneda C _) :=
 /--
 If `coyoneda.map f` is an isomorphism, so was `f`.
 -/
-def is_iso {X Y : Cᵒᵖ} (f : X ⟶ Y) [is_iso (coyoneda.map f)] : is_iso f :=
+lemma is_iso {X Y : Cᵒᵖ} (f : X ⟶ Y) [is_iso (coyoneda.map f)] : is_iso f :=
 is_iso_of_fully_faithful coyoneda f
 
 -- No need to use Cᵒᵖ here, works with any category
diff --git a/src/topology/category/TopCommRing.lean b/src/topology/category/TopCommRing.lean
index 035577994bbdf..91a3ce62262e4 100644
--- a/src/topology/category/TopCommRing.lean
+++ b/src/topology/category/TopCommRing.lean
@@ -104,9 +104,8 @@ instance : reflects_isomorphisms (forget₂ TopCommRing Top) :=
 
     -- Putting these together we obtain the isomorphism we're after:
     exact
-    { inv := ⟨e_Ring.symm, i_Top.inv.2⟩,
-      hom_inv_id' := by { ext x, exact e_Ring.left_inv x, },
-      inv_hom_id' := by { ext x, exact e_Ring.right_inv x, }, },
+    ⟨⟨e_Ring.symm, i_Top.inv.2⟩,
+      ⟨by { ext x, exact e_Ring.left_inv x, }, by { ext x, exact e_Ring.right_inv x, }⟩⟩
   end }
 
 end TopCommRing
diff --git a/src/topology/sheaves/forget.lean b/src/topology/sheaves/forget.lean
index 476998c4eb859..5c8373826f2c1 100644
--- a/src/topology/sheaves/forget.lean
+++ b/src/topology/sheaves/forget.lean
@@ -192,7 +192,7 @@ begin
       haveI : is_iso f' := is_limit.hom_is_iso hc hd' f',
       -- A cone morphism is an isomorphism exactly if the morphism between the cone points is,
       -- so we're done!
-      exact { ..((cones.forget _).map_iso (as_iso f')) }, }, },
+      exact is_iso.of_iso ((cones.forget _).map_iso (as_iso f')) }, },
 end
 
 /-!
diff --git a/src/topology/sheaves/presheaf.lean b/src/topology/sheaves/presheaf.lean
index 5319e18c889da..b8394be1d4d85 100644
--- a/src/topology/sheaves/presheaf.lean
+++ b/src/topology/sheaves/presheaf.lean
@@ -54,16 +54,18 @@ def pushforward_eq {X Y : Top.{v}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.presheaf
   f _* ℱ ≅ g _* ℱ :=
 iso_whisker_right (nat_iso.op (opens.map_iso f g h).symm) ℱ
 
-@[simp] lemma pushforward_eq_hom_app {X Y : Top.{v}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.presheaf C) (U) :
-  (pushforward_eq h ℱ).hom.app U = ℱ.map (begin dsimp [functor.op], apply has_hom.hom.op, apply eq_to_hom, rw h, end) :=
-rfl
+@[simp] lemma pushforward_eq_hom_app
+  {X Y : Top.{v}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.presheaf C) (U) :
+  (pushforward_eq h ℱ).hom.app U =
+    ℱ.map (begin dsimp [functor.op], apply has_hom.hom.op, apply eq_to_hom, rw h, end) :=
+by simp [pushforward_eq]
 
 @[simp]
 lemma pushforward_eq_rfl {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : X.presheaf C) (U) :
   (pushforward_eq (rfl : f = f) ℱ).hom.app (op U) = 𝟙 _ :=
 begin
   dsimp [pushforward_eq],
-  erw ℱ.map_id,
+  simp,
 end
 
 lemma pushforward_eq_eq {X Y : Top.{v}} {f g : X ⟶ Y} (h₁ h₂ : f = g) (ℱ : X.presheaf C) :