diff --git a/src/algebra/homology/differential_object.lean b/src/algebra/homology/differential_object.lean
index 02f49a1f5775f..28818d58f07d9 100644
--- a/src/algebra/homology/differential_object.lean
+++ b/src/algebra/homology/differential_object.lean
@@ -24,8 +24,35 @@ noncomputable theory
 
 namespace homological_complex
 
-variables {β : Type*} [add_comm_group β] (b : β)
-variables (V : Type*) [category V] [has_zero_morphisms V]
+variables {β : Type*} [add_comm_group β] {b : β}
+variables {V : Type*} [category V] [has_zero_morphisms V]
+
+/-- Since `eq_to_hom` only preserves the fact that `X.X i = X.X j` but not `i = j`, this definition
+is used to aid the simplifier. -/
+abbreviation _root_.category_theory.differential_object.X_eq_to_hom
+  (X : differential_object (graded_object_with_shift b V))
+  {i j : β} (h : i = j) : X.X i ⟶ X.X j := eq_to_hom (congr_arg X.X h)
+
+@[simp] lemma _root_.category_theory.differential_object.X_eq_to_hom_refl
+  (X : differential_object (graded_object_with_shift b V)) (i : β) :
+  X.X_eq_to_hom (refl i) = 𝟙 _ := rfl
+
+@[simp, reassoc] lemma eq_to_hom_d (X : differential_object (graded_object_with_shift b V))
+  {x y : β} (h : x = y) :
+  X.X_eq_to_hom h ≫ X.d y = X.d x ≫ X.X_eq_to_hom (by { cases h, refl }) :=
+by { cases h, dsimp, simp }
+
+@[simp, reassoc] lemma d_eq_to_hom (X : homological_complex V (complex_shape.up' b))
+  {x y z : β} (h : y = z) :
+  X.d x y ≫ eq_to_hom (congr_arg X.X h) = X.d x z :=
+by { cases h, simp }
+
+@[simp, reassoc] lemma eq_to_hom_f {X Y : differential_object (graded_object_with_shift b V)}
+  (f : X ⟶ Y) {x y : β} (h : x = y) :
+  X.X_eq_to_hom h ≫ f.f y = f.f x ≫ Y.X_eq_to_hom h :=
+by { cases h, simp }
+
+variables (b V)
 
 /--
 The functor from differential graded objects to homological complexes.
diff --git a/src/category_theory/differential_object.lean b/src/category_theory/differential_object.lean
index a6e3176ffff7e..cef33be1d1454 100644
--- a/src/category_theory/differential_object.lean
+++ b/src/category_theory/differential_object.lean
@@ -36,7 +36,7 @@ a morphism `d : X ⟶ X⟦1⟧`, such that `d^2 = 0`.
 structure differential_object :=
 (X : C)
 (d : X ⟶ X⟦1⟧)
-(d_squared' : d ≫ d⟦1⟧' = 0 . obviously)
+(d_squared' : d ≫ d⟦(1:ℤ)⟧' = 0 . obviously)
 
 restate_axiom differential_object.d_squared'
 attribute [simp] differential_object.d_squared
@@ -83,6 +83,11 @@ lemma comp_f {X Y Z : differential_object C} (f : X ⟶ Y) (g : Y ⟶ Z) :
   (f ≫ g).f = f.f ≫ g.f :=
 rfl
 
+@[simp]
+lemma eq_to_hom_f {X Y : differential_object C} (h : X = Y) :
+  hom.f (eq_to_hom h) = eq_to_hom (congr_arg _ h) :=
+by { subst h, rw [eq_to_hom_refl, eq_to_hom_refl], refl }
+
 variables (C)
 
 /-- The forgetful functor taking a differential object to its underlying object. -/
@@ -95,7 +100,7 @@ instance forget_faithful : faithful (forget C) :=
 
 instance has_zero_morphisms : has_zero_morphisms (differential_object C) :=
 { has_zero := λ X Y,
-  ⟨{ f := 0, }⟩}
+  ⟨{ f := 0 }⟩}
 
 variables {C}
 
@@ -115,6 +120,16 @@ An isomorphism of differential objects gives an isomorphism of the underlying ob
 @[simp] lemma iso_app_trans {X Y Z : differential_object C} (f : X ≅ Y) (g : Y ≅ Z) :
   iso_app (f ≪≫ g) = iso_app f ≪≫ iso_app g := rfl
 
+/-- An isomorphism of differential objects can be constructed
+from an isomorphism of the underlying objects that commutes with the differentials. -/
+@[simps] def mk_iso {X Y : differential_object C}
+  (f : X.X ≅ Y.X) (hf : X.d ≫ f.hom⟦1⟧' = f.hom ≫ Y.d) : X ≅ Y :=
+{ hom := ⟨f.hom, hf⟩,
+  inv := ⟨f.inv, by { dsimp, rw [← functor.map_iso_inv, iso.comp_inv_eq, category.assoc,
+    iso.eq_inv_comp, functor.map_iso_hom, ← hf], congr }⟩,
+  hom_inv_id' := by { ext1, dsimp, exact f.hom_inv_id },
+  inv_hom_id' := by { ext1, dsimp, exact f.inv_hom_id } }
+
 end differential_object
 
 namespace functor
diff --git a/src/category_theory/equivalence.lean b/src/category_theory/equivalence.lean
index 9cbe8fa3df704..28be1b6de041f 100644
--- a/src/category_theory/equivalence.lean
+++ b/src/category_theory/equivalence.lean
@@ -392,6 +392,8 @@ mk' ::
 
 restate_axiom is_equivalence.functor_unit_iso_comp'
 
+attribute [simp, reassoc] is_equivalence.functor_unit_iso_comp
+
 namespace is_equivalence
 
 instance of_equivalence (F : C ≌ D) : is_equivalence F.functor :=
@@ -433,6 +435,12 @@ is_equivalence.of_equivalence F.as_equivalence.symm
 @[simp] lemma as_equivalence_inverse (F : C ⥤ D) [is_equivalence F] :
   F.as_equivalence.inverse = inv F := rfl
 
+@[simp] lemma as_equivalence_unit {F : C ⥤ D} [h : is_equivalence F] :
+  F.as_equivalence.unit_iso = @@is_equivalence.unit_iso _ _ h := rfl
+
+@[simp] lemma as_equivalence_counit {F : C ⥤ D} [is_equivalence F] :
+  F.as_equivalence.counit_iso = is_equivalence.counit_iso := rfl
+
 @[simp] lemma inv_inv (F : C ⥤ D) [is_equivalence F] :
   inv (inv F) = F := rfl
 
diff --git a/src/category_theory/graded_object.lean b/src/category_theory/graded_object.lean
index 414e370b9f0fa..920133ec6536c 100644
--- a/src/category_theory/graded_object.lean
+++ b/src/category_theory/graded_object.lean
@@ -82,6 +82,10 @@ begin
   simp,
 end
 
+@[simp] lemma eq_to_hom_apply {β : Type w} {X Y : Π b : β, C} (h : X = Y) (b : β) :
+   (eq_to_hom h : X ⟶ Y) b = eq_to_hom (by subst h) :=
+ by { subst h, refl }
+
 /--
 The equivalence between β-graded objects and γ-graded objects,
 given an equivalence between β and γ.
diff --git a/src/category_theory/limits/has_limits.lean b/src/category_theory/limits/has_limits.lean
index a3c68ccea38d0..d206e0bbeb14e 100644
--- a/src/category_theory/limits/has_limits.lean
+++ b/src/category_theory/limits/has_limits.lean
@@ -491,8 +491,7 @@ lemma has_limits_of_size_shrink [has_limits_of_size.{(max v₁ v₂) (max u₁ u
 ⟨λ J hJ, by exactI has_limits_of_shape_of_equivalence
   (ulift_hom_ulift_category.equiv.{v₂ u₂} J).symm⟩
 
-@[priority 100]
-instance has_smallest_limits_of_has_limits [has_limits C] :
+lemma has_smallest_limits_of_has_limits [has_limits C] :
   has_limits_of_size.{0 0} C := has_limits_of_size_shrink.{0 0} C
 
 end limit
@@ -958,8 +957,7 @@ lemma has_colimits_of_size_shrink [has_colimits_of_size.{(max v₁ v₂) (max u
 ⟨λ J hJ, by exactI has_colimits_of_shape_of_equivalence
   (ulift_hom_ulift_category.equiv.{v₂ u₂} J).symm⟩
 
-@[priority 100]
-instance has_smallest_colimits_of_has_colimits [has_colimits C] :
+lemma has_smallest_colimits_of_has_colimits [has_colimits C] :
   has_colimits_of_size.{0 0} C := has_colimits_of_size_shrink.{0 0} C
 
 end colimit
diff --git a/src/category_theory/monoidal/End.lean b/src/category_theory/monoidal/End.lean
index 8eb24cc502613..7a37d952ac68f 100644
--- a/src/category_theory/monoidal/End.lean
+++ b/src/category_theory/monoidal/End.lean
@@ -121,7 +121,7 @@ end
 
 @[simp, reassoc]
 lemma μ_naturalityₗ {m n m' : M} (f : m ⟶ m') (X : C) :
-  (F.obj n).map((F.map f).app X) ≫ (F.μ m' n).app X =
+  (F.obj n).map ((F.map f).app X) ≫ (F.μ m' n).app X =
     (F.μ m n).app X ≫ (F.map (f ⊗ 𝟙 n)).app X :=
 begin
   rw ← μ_naturality₂ F f (𝟙 n) X,
@@ -137,6 +137,24 @@ begin
   simp,
 end
 
+@[simp, reassoc]
+lemma μ_inv_naturalityₗ {m n m' : M} (f : m ⟶ m') (X : C) :
+  (F.μ_iso m n).inv.app X ≫ (F.obj n).map ((F.map f).app X) =
+    (F.map (f ⊗ 𝟙 n)).app X ≫ (F.μ_iso m' n).inv.app X :=
+begin
+  rw [← is_iso.comp_inv_eq, category.assoc, ← is_iso.eq_inv_comp],
+  simp,
+end
+
+@[simp, reassoc]
+lemma μ_inv_naturalityᵣ {m n n' : M} (g : n ⟶ n') (X : C) :
+  (F.μ_iso m n).inv.app X ≫ (F.map g).app ((F.obj m).obj X) =
+    (F.map (𝟙 m ⊗ g)).app X ≫ (F.μ_iso m n').inv.app X :=
+begin
+  rw [← is_iso.comp_inv_eq, category.assoc, ← is_iso.eq_inv_comp],
+  simp,
+end
+
 @[reassoc]
 lemma left_unitality_app (n : M) (X : C) :
   (F.obj n).map (F.ε.app X) ≫ (F.μ (𝟙_M) n).app X
diff --git a/src/category_theory/monoidal/discrete.lean b/src/category_theory/monoidal/discrete.lean
index f056580d65f24..7b5463aacc5bc 100644
--- a/src/category_theory/monoidal/discrete.lean
+++ b/src/category_theory/monoidal/discrete.lean
@@ -23,9 +23,11 @@ variables (M : Type u) [monoid M]
 
 namespace category_theory
 
+@[to_additive]
 instance monoid_discrete : monoid (discrete M) := by { dsimp [discrete], apply_instance }
 
-instance : monoidal_category (discrete M) :=
+@[to_additive discrete.add_monoidal]
+instance discrete.monoidal : monoidal_category (discrete M) :=
 { tensor_unit := 1,
   tensor_obj := λ X Y, X * Y,
   tensor_hom := λ W X Y Z f g, eq_to_hom (by rw [eq_of_hom f, eq_of_hom g]),
@@ -39,7 +41,8 @@ variables {M} {N : Type u} [monoid N]
 A multiplicative morphism between monoids gives a monoidal functor between the corresponding
 discrete monoidal categories.
 -/
-@[simps]
+@[to_additive dicrete.add_monoidal_functor "An additive morphism between add_monoids gives a
+  monoidal functor between the corresponding discrete monoidal categories.", simps]
 def discrete.monoidal_functor (F : M →* N) : monoidal_functor (discrete M) (discrete N) :=
 { obj := F,
   map := λ X Y f, eq_to_hom (F.congr_arg (eq_of_hom f)),
@@ -51,6 +54,8 @@ variables {K : Type u} [monoid K]
 /--
 The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.
 -/
+@[to_additive dicrete.add_monoidal_functor_comp "The monoidal natural isomorphism corresponding to
+composing two additive morphisms."]
 def discrete.monoidal_functor_comp (F : M →* N) (G : N →* K) :
   discrete.monoidal_functor F ⊗⋙ discrete.monoidal_functor G ≅
   discrete.monoidal_functor (G.comp F) :=
diff --git a/src/category_theory/natural_isomorphism.lean b/src/category_theory/natural_isomorphism.lean
index 83d3624bca609..b0aa03fd8d6d8 100644
--- a/src/category_theory/natural_isomorphism.lean
+++ b/src/category_theory/natural_isomorphism.lean
@@ -124,7 +124,7 @@ by simp only [←category.assoc, cancel_mono]
 by simp only [←category.assoc, cancel_mono]
 
 @[simp] lemma inv_inv_app {F G : C ⥤ D} (e : F ≅ G) (X : C) :
-   inv (e.inv.app X) = e.hom.app X := by { ext, simp }
+  inv (e.inv.app X) = e.hom.app X := by { ext, simp }
 
 end
 
diff --git a/src/category_theory/triangulated/basic.lean b/src/category_theory/triangulated/basic.lean
index beaedcd510b65..7aa66f149d901 100644
--- a/src/category_theory/triangulated/basic.lean
+++ b/src/category_theory/triangulated/basic.lean
@@ -40,14 +40,14 @@ structure triangle := mk' ::
 (obj₃ : C)
 (mor₁ : obj₁ ⟶ obj₂)
 (mor₂ : obj₂ ⟶ obj₃)
-(mor₃ : obj₃ ⟶ obj₁⟦1⟧)
+(mor₃ : obj₃ ⟶ obj₁⟦(1:ℤ)⟧)
 
 /--
 A triangle `(X,Y,Z,f,g,h)` in `C` is defined by the morphisms `f : X ⟶ Y`, `g : Y ⟶ Z`
 and `h : Z ⟶ X⟦1⟧`.
 -/
 @[simps]
-def triangle.mk {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ X⟦1⟧) : triangle C :=
+def triangle.mk {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1:ℤ)⟧) : triangle C :=
 { obj₁ := X,
   obj₂ := Y,
   obj₃ := Z,