diff --git a/Mathlib/CategoryTheory/Limits/IsLimit.lean b/Mathlib/CategoryTheory/Limits/IsLimit.lean
index aadce6f6709af..0f2ae8fbf255d 100644
--- a/Mathlib/CategoryTheory/Limits/IsLimit.lean
+++ b/Mathlib/CategoryTheory/Limits/IsLimit.lean
@@ -56,40 +56,39 @@ cone morphism to `t`.
 
 See <https://stacks.math.columbia.edu/tag/002E>.
   -/
-@[nolint has_nonempty_instance]
+-- Porting note: removed @[nolint has_nonempty_instance]
 structure IsLimit (t : Cone F) where
-  lift : ∀ s : Cone F, s.x ⟶ t.x
-  fac' : ∀ (s : Cone F) (j : J), lift s ≫ t.π.app j = s.π.app j := by obviously
-  uniq' : ∀ (s : Cone F) (m : s.x ⟶ t.x) (w : ∀ j : J, m ≫ t.π.app j = s.π.app j), m = lift s := by
-    obviously
+  lift : ∀ s : Cone F, s.X ⟶ t.X
+  fac : ∀ (s : Cone F) (j : J), lift s ≫ t.π.app j = s.π.app j := by aesop_cat
+  uniq : ∀ (s : Cone F) (m : s.X ⟶ t.X) (_ : ∀ j : J, m ≫ t.π.app j = s.π.app j), m = lift s := by
+    aesop_cat
 #align category_theory.limits.is_limit CategoryTheory.Limits.IsLimit
+#align category_theory.limits.is_limit.fac' CategoryTheory.Limits.IsLimit.fac
+#align category_theory.limits.is_limit.uniq' CategoryTheory.Limits.IsLimit.uniq
 
-restate_axiom is_limit.fac'
 
-attribute [simp, reassoc.1] is_limit.fac
-
-restate_axiom is_limit.uniq'
+attribute [reassoc (attr := simp)] IsLimit.fac
 
 namespace IsLimit
 
 instance subsingleton {t : Cone F} : Subsingleton (IsLimit t) :=
-  ⟨by intro P Q <;> cases P <;> cases Q <;> congr <;> ext <;> solve_by_elim⟩
+  ⟨by intro P Q ; cases P ; cases Q ; congr ; ext ; aesop_cat⟩
 #align category_theory.limits.is_limit.subsingleton CategoryTheory.Limits.IsLimit.subsingleton
 
 /-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cone point
 of any cone over `F` to the cone point of a limit cone over `G`. -/
-def map {F G : J ⥤ C} (s : Cone F) {t : Cone G} (P : IsLimit t) (α : F ⟶ G) : s.x ⟶ t.x :=
+def map {F G : J ⥤ C} (s : Cone F) {t : Cone G} (P : IsLimit t) (α : F ⟶ G) : s.X ⟶ t.X :=
   P.lift ((Cones.postcompose α).obj s)
 #align category_theory.limits.is_limit.map CategoryTheory.Limits.IsLimit.map
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem map_π {F G : J ⥤ C} (c : Cone F) {d : Cone G} (hd : IsLimit d) (α : F ⟶ G) (j : J) :
     hd.map c α ≫ d.π.app j = c.π.app j ≫ α.app j :=
   fac _ _ _
 #align category_theory.limits.is_limit.map_π CategoryTheory.Limits.IsLimit.map_π
 
-theorem lift_self {c : Cone F} (t : IsLimit c) : t.lift c = 𝟙 c.x :=
-  (t.uniq _ _ fun j => id_comp _).symm
+theorem lift_self {c : Cone F} (t : IsLimit c) : t.lift c = 𝟙 c.X :=
+  (t.uniq _ _ fun _ => id_comp _).symm
 #align category_theory.limits.is_limit.lift_self CategoryTheory.Limits.IsLimit.lift_self
 
 -- Repackaging the definition in terms of cone morphisms.
@@ -99,19 +98,20 @@ def liftConeMorphism {t : Cone F} (h : IsLimit t) (s : Cone F) : s ⟶ t where H
 #align category_theory.limits.is_limit.lift_cone_morphism CategoryTheory.Limits.IsLimit.liftConeMorphism
 
 theorem uniq_cone_morphism {s t : Cone F} (h : IsLimit t) {f f' : s ⟶ t} : f = f' :=
-  have : ∀ {g : s ⟶ t}, g = h.liftConeMorphism s := by intro g <;> ext <;> exact h.uniq _ _ g.w
+  have : ∀ {g : s ⟶ t}, g = h.liftConeMorphism s := by 
+    intro g; apply ConeMorphism.ext; exact h.uniq _ _ g.w
   this.trans this.symm
 #align category_theory.limits.is_limit.uniq_cone_morphism CategoryTheory.Limits.IsLimit.uniq_cone_morphism
 
 /-- Restating the definition of a limit cone in terms of the ∃! operator. -/
 theorem existsUnique {t : Cone F} (h : IsLimit t) (s : Cone F) :
-    ∃! l : s.x ⟶ t.x, ∀ j, l ≫ t.π.app j = s.π.app j :=
+    ∃! l : s.X ⟶ t.X, ∀ j, l ≫ t.π.app j = s.π.app j :=
   ⟨h.lift s, h.fac s, h.uniq s⟩
 #align category_theory.limits.is_limit.exists_unique CategoryTheory.Limits.IsLimit.existsUnique
 
 /-- Noncomputably make a colimit cocone from the existence of unique factorizations. -/
 def ofExistsUnique {t : Cone F}
-    (ht : ∀ s : Cone F, ∃! l : s.x ⟶ t.x, ∀ j, l ≫ t.π.app j = s.π.app j) : IsLimit t := by
+    (ht : ∀ s : Cone F, ∃! l : s.X ⟶ t.X, ∀ j, l ≫ t.π.app j = s.π.app j) : IsLimit t := by
   choose s hs hs' using ht
   exact ⟨s, hs, hs'⟩
 #align category_theory.limits.is_limit.of_exists_unique CategoryTheory.Limits.IsLimit.ofExistsUnique
@@ -122,22 +122,22 @@ and separately the factorisation condition.
 -/
 @[simps]
 def mkConeMorphism {t : Cone F} (lift : ∀ s : Cone F, s ⟶ t)
-    (uniq' : ∀ (s : Cone F) (m : s ⟶ t), m = lift s) : IsLimit t
+    (uniq : ∀ (s : Cone F) (m : s ⟶ t), m = lift s) : IsLimit t
     where
   lift s := (lift s).Hom
-  uniq' s m w :=
-    have : ConeMorphism.mk m w = lift s := by apply uniq'
-    congr_arg ConeMorphism.hom this
+  uniq s m w :=
+    have : ConeMorphism.mk m w = lift s := by apply uniq
+    congrArg ConeMorphism.Hom this
 #align category_theory.limits.is_limit.mk_cone_morphism CategoryTheory.Limits.IsLimit.mkConeMorphism
 
 /-- Limit cones on `F` are unique up to isomorphism. -/
 @[simps]
 def uniqueUpToIso {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : s ≅ t
     where
-  Hom := Q.liftConeMorphism s
+  hom := Q.liftConeMorphism s
   inv := P.liftConeMorphism t
-  hom_inv_id' := P.uniq_cone_morphism
-  inv_hom_id' := Q.uniq_cone_morphism
+  hom_inv_id := P.uniq_cone_morphism
+  inv_hom_id := Q.uniq_cone_morphism
 #align category_theory.limits.is_limit.unique_up_to_iso CategoryTheory.Limits.IsLimit.uniqueUpToIso
 
 /-- Any cone morphism between limit cones is an isomorphism. -/
@@ -146,29 +146,29 @@ theorem hom_isIso {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (f : s ⟶ t) :
 #align category_theory.limits.is_limit.hom_is_iso CategoryTheory.Limits.IsLimit.hom_isIso
 
 /-- Limits of `F` are unique up to isomorphism. -/
-def conePointUniqueUpToIso {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : s.x ≅ t.x :=
+def conePointUniqueUpToIso {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) : s.X ≅ t.X :=
   (Cones.forget F).mapIso (uniqueUpToIso P Q)
 #align category_theory.limits.is_limit.cone_point_unique_up_to_iso CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem conePointUniqueUpToIso_hom_comp {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) :
-    (conePointUniqueUpToIso P Q).Hom ≫ t.π.app j = s.π.app j :=
-  (uniqueUpToIso P Q).Hom.w _
+    (conePointUniqueUpToIso P Q).hom ≫ t.π.app j = s.π.app j :=
+  (uniqueUpToIso P Q).hom.w _
 #align category_theory.limits.is_limit.cone_point_unique_up_to_iso_hom_comp CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem conePointUniqueUpToIso_inv_comp {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (j : J) :
     (conePointUniqueUpToIso P Q).inv ≫ s.π.app j = t.π.app j :=
   (uniqueUpToIso P Q).inv.w _
 #align category_theory.limits.is_limit.cone_point_unique_up_to_iso_inv_comp CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem lift_comp_conePointUniqueUpToIso_hom {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) :
-    P.lift r ≫ (conePointUniqueUpToIso P Q).Hom = Q.lift r :=
+    P.lift r ≫ (conePointUniqueUpToIso P Q).hom = Q.lift r :=
   Q.uniq _ _ (by simp)
 #align category_theory.limits.is_limit.lift_comp_cone_point_unique_up_to_iso_hom CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem lift_comp_conePointUniqueUpToIso_inv {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) :
     Q.lift r ≫ (conePointUniqueUpToIso P Q).inv = P.lift r :=
   P.uniq _ _ (by simp)
@@ -176,13 +176,13 @@ theorem lift_comp_conePointUniqueUpToIso_inv {r s t : Cone F} (P : IsLimit s) (Q
 
 /-- Transport evidence that a cone is a limit cone across an isomorphism of cones. -/
 def ofIsoLimit {r t : Cone F} (P : IsLimit r) (i : r ≅ t) : IsLimit t :=
-  IsLimit.mkConeMorphism (fun s => P.liftConeMorphism s ≫ i.Hom) fun s m => by
-    rw [← i.comp_inv_eq] <;> apply P.uniq_cone_morphism
+  IsLimit.mkConeMorphism (fun s => P.liftConeMorphism s ≫ i.hom) fun s m => by
+    rw [← i.comp_inv_eq]; apply P.uniq_cone_morphism
 #align category_theory.limits.is_limit.of_iso_limit CategoryTheory.Limits.IsLimit.ofIsoLimit
 
 @[simp]
 theorem ofIsoLimit_lift {r t : Cone F} (P : IsLimit r) (i : r ≅ t) (s) :
-    (P.ofIsoLimit i).lift s = P.lift s ≫ i.Hom.Hom :=
+    (P.ofIsoLimit i).lift s = P.lift s ≫ i.hom.Hom :=
   rfl
 #align category_theory.limits.is_limit.of_iso_limit_lift CategoryTheory.Limits.IsLimit.ofIsoLimit_lift
 
@@ -191,8 +191,8 @@ def equivIsoLimit {r t : Cone F} (i : r ≅ t) : IsLimit r ≃ IsLimit t
     where
   toFun h := h.ofIsoLimit i
   invFun h := h.ofIsoLimit i.symm
-  left_inv := by tidy
-  right_inv := by tidy
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
 #align category_theory.limits.is_limit.equiv_iso_limit CategoryTheory.Limits.IsLimit.equivIsoLimit
 
 @[simp]
@@ -213,28 +213,28 @@ first cone was limiting also.
 def ofPointIso {r t : Cone F} (P : IsLimit r) [i : IsIso (P.lift t)] : IsLimit t :=
   ofIsoLimit P
     (by
-      haveI : is_iso (P.lift_cone_morphism t).Hom := i
-      haveI : is_iso (P.lift_cone_morphism t) := cones.cone_iso_of_hom_iso _
+      haveI : IsIso (P.liftConeMorphism t).Hom := i
+      haveI : IsIso (P.liftConeMorphism t) := Cones.cone_iso_of_hom_iso _
       symm
-      apply as_iso (P.lift_cone_morphism t))
+      apply asIso (P.liftConeMorphism t))
 #align category_theory.limits.is_limit.of_point_iso CategoryTheory.Limits.IsLimit.ofPointIso
 
 variable {t : Cone F}
 
-theorem hom_lift (h : IsLimit t) {W : C} (m : W ⟶ t.x) :
+theorem hom_lift (h : IsLimit t) {W : C} (m : W ⟶ t.X) :
     m =
       h.lift
-        { x := W
+        { X := W
           π := { app := fun b => m ≫ t.π.app b } } :=
   h.uniq
-    { x := W
+    { X := W
       π := { app := fun b => m ≫ t.π.app b } } m fun b => rfl
 #align category_theory.limits.is_limit.hom_lift CategoryTheory.Limits.IsLimit.hom_lift
 
 /-- Two morphisms into a limit are equal if their compositions with
   each cone morphism are equal. -/
-theorem hom_ext (h : IsLimit t) {W : C} {f f' : W ⟶ t.x} (w : ∀ j, f ≫ t.π.app j = f' ≫ t.π.app j) :
-    f = f' := by rw [h.hom_lift f, h.hom_lift f'] <;> congr <;> exact funext w
+theorem hom_ext (h : IsLimit t) {W : C} {f f' : W ⟶ t.X} (w : ∀ j, f ≫ t.π.app j = f' ≫ t.π.app j) :
+    f = f' := by rw [h.hom_lift f, h.hom_lift f']; congr; exact funext w
 #align category_theory.limits.is_limit.hom_ext CategoryTheory.Limits.IsLimit.hom_ext
 
 /-- Given a right adjoint functor between categories of cones,
@@ -243,26 +243,26 @@ the image of a limit cone is a limit cone.
 def ofRightAdjoint {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cone G ⥤ Cone F)
     [IsRightAdjoint h] {c : Cone G} (t : IsLimit c) : IsLimit (h.obj c) :=
   mkConeMorphism (fun s => (Adjunction.ofRightAdjoint h).homEquiv s c (t.liftConeMorphism _))
-    fun s m => (Adjunction.eq_homEquiv_apply _ _ _).2 t.uniq_cone_morphism
+    fun _ _ => (Adjunction.eq_homEquiv_apply _ _ _).2 t.uniq_cone_morphism
 #align category_theory.limits.is_limit.of_right_adjoint CategoryTheory.Limits.IsLimit.ofRightAdjoint
 
 /-- Given two functors which have equivalent categories of cones, we can transport a limiting cone
 across the equivalence.
 -/
 def ofConeEquiv {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cone G ≌ Cone F) {c : Cone G} :
-    IsLimit (h.Functor.obj c) ≃ IsLimit c
+    IsLimit (h.functor.obj c) ≃ IsLimit c
     where
   toFun P := ofIsoLimit (ofRightAdjoint h.inverse P) (h.unitIso.symm.app c)
-  invFun := ofRightAdjoint h.Functor
-  left_inv := by tidy
-  right_inv := by tidy
+  invFun := ofRightAdjoint h.functor
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
 #align category_theory.limits.is_limit.of_cone_equiv CategoryTheory.Limits.IsLimit.ofConeEquiv
 
 @[simp]
 theorem ofConeEquiv_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cone G ≌ Cone F)
-    {c : Cone G} (P : IsLimit (h.Functor.obj c)) (s) :
+    {c : Cone G} (P : IsLimit (h.functor.obj c)) (s) :
     (ofConeEquiv h P).lift s =
-      ((h.unitIso.Hom.app s).Hom ≫ (h.Functor.inv.map (P.liftConeMorphism (h.Functor.obj s))).Hom) ≫
+      ((h.unitIso.hom.app s).Hom ≫ (h.functor.inv.map (P.liftConeMorphism (h.functor.obj s))).Hom) ≫
         (h.unitIso.inv.app c).Hom :=
   rfl
 #align category_theory.limits.is_limit.of_cone_equiv_apply_desc CategoryTheory.Limits.IsLimit.ofConeEquiv_apply_desc
@@ -271,7 +271,7 @@ theorem ofConeEquiv_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D}
 theorem ofConeEquiv_symm_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D}
     (h : Cone G ≌ Cone F) {c : Cone G} (P : IsLimit c) (s) :
     ((ofConeEquiv h).symm P).lift s =
-      (h.counitIso.inv.app s).Hom ≫ (h.Functor.map (P.liftConeMorphism (h.inverse.obj s))).Hom :=
+      (h.counitIso.inv.app s).Hom ≫ (h.functor.map (P.liftConeMorphism (h.inverse.obj s))).Hom :=
   rfl
 #align category_theory.limits.is_limit.of_cone_equiv_symm_apply_desc CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc
 
@@ -279,7 +279,7 @@ theorem ofConeEquiv_symm_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K 
 A cone postcomposed with a natural isomorphism is a limit cone if and only if the original cone is.
 -/
 def postcomposeHomEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cone F) :
-    IsLimit ((Cones.postcompose α.Hom).obj c) ≃ IsLimit c :=
+    IsLimit ((Cones.postcompose α.hom).obj c) ≃ IsLimit c :=
   ofConeEquiv (Cones.postcomposeEquivalence α)
 #align category_theory.limits.is_limit.postcompose_hom_equiv CategoryTheory.Limits.IsLimit.postcomposeHomEquiv
 
@@ -295,7 +295,7 @@ def postcomposeInvEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cone G) :
 between the underlying functors, and then an isomorphism between `c` transported along this and `d`.
 -/
 def equivOfNatIsoOfIso {F G : J ⥤ C} (α : F ≅ G) (c : Cone F) (d : Cone G)
-    (w : (Cones.postcompose α.Hom).obj c ≅ d) : IsLimit c ≃ IsLimit d :=
+    (w : (Cones.postcompose α.hom).obj c ≅ d) : IsLimit c ≃ IsLimit d :=
   (postcomposeHomEquiv α _).symm.trans (equivIsoLimit w)
 #align category_theory.limits.is_limit.equiv_of_nat_iso_of_iso CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
 
@@ -304,33 +304,33 @@ are themselves isomorphic.
 -/
 @[simps]
 def conePointsIsoOfNatIso {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s) (Q : IsLimit t)
-    (w : F ≅ G) : s.x ≅ t.x where
-  Hom := Q.map s w.Hom
+    (w : F ≅ G) : s.X ≅ t.X where
+  hom := Q.map s w.hom
   inv := P.map t w.inv
-  hom_inv_id' := P.hom_ext (by tidy)
-  inv_hom_id' := Q.hom_ext (by tidy)
+  hom_inv_id := P.hom_ext (by aesop_cat)
+  inv_hom_id := Q.hom_ext (by aesop_cat)
 #align category_theory.limits.is_limit.cone_points_iso_of_nat_iso CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso
 
-@[reassoc.1]
+@[reassoc]
 theorem conePointsIsoOfNatIso_hom_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s)
     (Q : IsLimit t) (w : F ≅ G) (j : J) :
-    (conePointsIsoOfNatIso P Q w).Hom ≫ t.π.app j = s.π.app j ≫ w.Hom.app j := by simp
+    (conePointsIsoOfNatIso P Q w).hom ≫ t.π.app j = s.π.app j ≫ w.hom.app j := by simp
 #align category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom_comp CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp
 
-@[reassoc.1]
+@[reassoc]
 theorem conePointsIsoOfNatIso_inv_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s)
     (Q : IsLimit t) (w : F ≅ G) (j : J) :
     (conePointsIsoOfNatIso P Q w).inv ≫ s.π.app j = t.π.app j ≫ w.inv.app j := by simp
 #align category_theory.limits.is_limit.cone_points_iso_of_nat_iso_inv_comp CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp
 
-@[reassoc.1]
+@[reassoc]
 theorem lift_comp_conePointsIsoOfNatIso_hom {F G : J ⥤ C} {r s : Cone F} {t : Cone G}
     (P : IsLimit s) (Q : IsLimit t) (w : F ≅ G) :
-    P.lift r ≫ (conePointsIsoOfNatIso P Q w).Hom = Q.map r w.Hom :=
+    P.lift r ≫ (conePointsIsoOfNatIso P Q w).hom = Q.map r w.hom :=
   Q.hom_ext (by simp)
 #align category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_hom CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom
 
-@[reassoc.1]
+@[reassoc]
 theorem lift_comp_conePointsIsoOfNatIso_inv {F G : J ⥤ C} {r s : Cone G} {t : Cone F}
     (P : IsLimit t) (Q : IsLimit s) (w : F ≅ G) :
     Q.lift r ≫ (conePointsIsoOfNatIso P Q w).inv = P.map r w.inv :=
@@ -343,21 +343,21 @@ open CategoryTheory.Equivalence
 
 /-- If `s : cone F` is a limit cone, so is `s` whiskered by an equivalence `e`.
 -/
-def whiskerEquivalence {s : Cone F} (P : IsLimit s) (e : K ≌ J) : IsLimit (s.whisker e.Functor) :=
-  ofRightAdjoint (Cones.whiskeringEquivalence e).Functor P
+def whiskerEquivalence {s : Cone F} (P : IsLimit s) (e : K ≌ J) : IsLimit (s.whisker e.functor) :=
+  ofRightAdjoint (Cones.whiskeringEquivalence e).functor P
 #align category_theory.limits.is_limit.whisker_equivalence CategoryTheory.Limits.IsLimit.whiskerEquivalence
 
 /-- If `s : cone F` whiskered by an equivalence `e` is a limit cone, so is `s`.
 -/
-def ofWhiskerEquivalence {s : Cone F} (e : K ≌ J) (P : IsLimit (s.whisker e.Functor)) : IsLimit s :=
+def ofWhiskerEquivalence {s : Cone F} (e : K ≌ J) (P : IsLimit (s.whisker e.functor)) : IsLimit s :=
   equivIsoLimit ((Cones.whiskeringEquivalence e).unitIso.app s).symm
     (ofRightAdjoint (Cones.whiskeringEquivalence e).inverse P : _)
 #align category_theory.limits.is_limit.of_whisker_equivalence CategoryTheory.Limits.IsLimit.ofWhiskerEquivalence
 
 /-- Given an equivalence of diagrams `e`, `s` is a limit cone iff `s.whisker e.functor` is.
 -/
-def whiskerEquivalenceEquiv {s : Cone F} (e : K ≌ J) : IsLimit s ≃ IsLimit (s.whisker e.Functor) :=
-  ⟨fun h => h.whiskerEquivalence e, ofWhiskerEquivalence e, by tidy, by tidy⟩
+def whiskerEquivalenceEquiv {s : Cone F} (e : K ≌ J) : IsLimit s ≃ IsLimit (s.whisker e.functor) :=
+  ⟨fun h => h.whiskerEquivalence e, ofWhiskerEquivalence e, by aesop_cat, by aesop_cat⟩
 #align category_theory.limits.is_limit.whisker_equivalence_equiv CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv
 
 /-- We can prove two cone points `(s : cone F).X` and `(t.cone G).X` are isomorphic if
@@ -371,74 +371,84 @@ and the functor (up to natural isomorphism).
 -/
 @[simps]
 def conePointsIsoOfEquivalence {F : J ⥤ C} {s : Cone F} {G : K ⥤ C} {t : Cone G} (P : IsLimit s)
-    (Q : IsLimit t) (e : J ≌ K) (w : e.Functor ⋙ G ≅ F) : s.x ≅ t.x :=
+    (Q : IsLimit t) (e : J ≌ K) (w : e.functor ⋙ G ≅ F) : s.X ≅ t.X :=
   let w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ invFunIdAssoc e G
-  { Hom := Q.lift ((Cones.equivalenceOfReindexing e.symm w').Functor.obj s)
-    inv := P.lift ((Cones.equivalenceOfReindexing e w).Functor.obj t)
-    hom_inv_id' := by
+  { hom := Q.lift ((Cones.equivalenceOfReindexing e.symm w').functor.obj s)
+    inv := P.lift ((Cones.equivalenceOfReindexing e w).functor.obj t)
+    hom_inv_id := by
       apply hom_ext P; intro j
       dsimp
-      simp only [limits.cone.whisker_π, limits.cones.postcompose_obj_π, fac, whisker_left_app,
-        assoc, id_comp, inv_fun_id_assoc_hom_app, fac_assoc, nat_trans.comp_app]
-      rw [counit_app_functor, ← functor.comp_map, w.hom.naturality]
+      simp only [Limits.Cone.whisker_π, Limits.Cones.postcompose_obj_π, fac, whiskerLeft_app,
+        assoc, id_comp, invFunIdAssoc_hom_app, fac_assoc, NatTrans.comp_app]
+      rw [counit_app_functor, ←Functor.comp_map]
+      have l : 
+        NatTrans.app w.hom j = NatTrans.app w.hom (Prefunctor.obj (𝟭 J).toPrefunctor j) := by dsimp
+      rw [l,w.hom.naturality]
       simp
-    inv_hom_id' := by
+    inv_hom_id := by
       apply hom_ext Q
-      tidy }
+      aesop_cat }
 #align category_theory.limits.is_limit.cone_points_iso_of_equivalence CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence
 
 end Equivalence
 
 /-- The universal property of a limit cone: a map `W ⟶ X` is the same as
   a cone on `F` with vertex `W`. -/
-def homIso (h : IsLimit t) (W : C) : ULift.{u₁} (W ⟶ t.x : Type v₃) ≅ (const J).obj W ⟶ F
-    where
-  Hom f := (t.extend f.down).π
+def homIso (h : IsLimit t) (W : C) : ULift.{u₁} (W ⟶ t.X : Type v₃) ≅ (const J).obj W ⟶ F where
+  hom f := (t.extend f.down).π
   inv π :=
     ⟨h.lift
-        { x := W
+        { X := W
           π }⟩
-  hom_inv_id' := by ext f <;> apply h.hom_ext <;> intro j <;> simp <;> dsimp <;> rfl
+  hom_inv_id := by 
+    funext f; apply ULift.ext
+    apply h.hom_ext; intro j; simp
+  inv_hom_id := by 
+    funext f; dsimp [const]; aesop_cat
 #align category_theory.limits.is_limit.hom_iso CategoryTheory.Limits.IsLimit.homIso
 
 @[simp]
-theorem homIso_hom (h : IsLimit t) {W : C} (f : ULift.{u₁} (W ⟶ t.x)) :
-    (IsLimit.homIso h W).Hom f = (t.extend f.down).π :=
+theorem homIso_hom (h : IsLimit t) {W : C} (f : ULift.{u₁} (W ⟶ t.X)) :
+    (IsLimit.homIso h W).hom f = (t.extend f.down).π :=
   rfl
 #align category_theory.limits.is_limit.hom_iso_hom CategoryTheory.Limits.IsLimit.homIso_hom
 
 /-- The limit of `F` represents the functor taking `W` to
   the set of cones on `F` with vertex `W`. -/
-def natIso (h : IsLimit t) : yoneda.obj t.x ⋙ uliftFunctor.{u₁} ≅ F.cones :=
-  NatIso.ofComponents (fun W => IsLimit.homIso h (unop W)) (by tidy)
+def natIso (h : IsLimit t) : yoneda.obj t.X ⋙ uliftFunctor.{u₁} ≅ F.cones := by
+  refine NatIso.ofComponents (fun W => IsLimit.homIso h (unop W)) ?_
+  intro X Y f 
+  dsimp [yoneda,homIso,const,uliftFunctor,cones]
+  funext g 
+  aesop_cat
 #align category_theory.limits.is_limit.nat_iso CategoryTheory.Limits.IsLimit.natIso
 
 /-- Another, more explicit, formulation of the universal property of a limit cone.
 See also `hom_iso`.
 -/
 def homIso' (h : IsLimit t) (W : C) :
-    ULift.{u₁} (W ⟶ t.x : Type v₃) ≅
+    ULift.{u₁} (W ⟶ t.X : Type v₃) ≅
       { p : ∀ j, W ⟶ F.obj j // ∀ {j j'} (f : j ⟶ j'), p j ≫ F.map f = p j' } :=
   h.homIso W ≪≫
-    { Hom := fun π =>
-        ⟨fun j => π.app j, fun j j' f => by convert ← (π.naturality f).symm <;> apply id_comp⟩
+    { hom := fun π =>
+        ⟨fun j => π.app j, fun f => by convert ← (π.naturality f).symm; apply id_comp⟩
       inv := fun p =>
         { app := fun j => p.1 j
-          naturality' := fun j j' f => by dsimp; rw [id_comp]; exact (p.2 f).symm } }
+          naturality := fun j j' f => by dsimp; rw [id_comp]; exact (p.2 f).symm } }
 #align category_theory.limits.is_limit.hom_iso' CategoryTheory.Limits.IsLimit.homIso'
 
 /-- If G : C → D is a faithful functor which sends t to a limit cone,
   then it suffices to check that the induced maps for the image of t
   can be lifted to maps of C. -/
 def ofFaithful {t : Cone F} {D : Type u₄} [Category.{v₄} D] (G : C ⥤ D) [Faithful G]
-    (ht : IsLimit (G.mapCone t)) (lift : ∀ s : Cone F, s.x ⟶ t.x)
-    (h : ∀ s, G.map (lift s) = ht.lift (G.mapCone s)) : IsLimit t :=
+    (ht : IsLimit (mapCone G t)) (lift : ∀ s : Cone F, s.X ⟶ t.X)
+    (h : ∀ s, G.map (lift s) = ht.lift (mapCone G s)) : IsLimit t :=
   { lift
-    fac' := fun s j => by apply G.map_injective <;> rw [G.map_comp, h] <;> apply ht.fac
-    uniq' := fun s m w => by
+    fac := fun s j => by apply G.map_injective; rw [G.map_comp, h]; apply ht.fac
+    uniq := fun s m w => by
       apply G.map_injective; rw [h]
-      refine' ht.uniq (G.map_cone s) _ fun j => _
-      convert ← congr_arg (fun f => G.map f) (w j)
+      refine' ht.uniq (mapCone G s) _ fun j => _
+      convert ← congrArg (fun f => G.map f) (w j)
       apply G.map_comp }
 #align category_theory.limits.is_limit.of_faithful CategoryTheory.Limits.IsLimit.ofFaithful
 
@@ -446,22 +456,21 @@ def ofFaithful {t : Cone F} {D : Type u₄} [Category.{v₄} D] (G : C ⥤ D) [F
 `G.map_cone c` is also a limit.
 -/
 def mapConeEquiv {D : Type u₄} [Category.{v₄} D] {K : J ⥤ C} {F G : C ⥤ D} (h : F ≅ G) {c : Cone K}
-    (t : IsLimit (F.mapCone c)) : IsLimit (G.mapCone c) := by
-  apply postcompose_inv_equiv (iso_whisker_left K h : _) (G.map_cone c) _
-  apply t.of_iso_limit (postcompose_whisker_left_map_cone h.symm c).symm
+    (t : IsLimit (mapCone F c)) : IsLimit (mapCone G c) := by
+  apply postcomposeInvEquiv (isoWhiskerLeft K h : _) (mapCone G c) _
+  apply t.ofIsoLimit (postcomposeWhiskerLeftMapCone h.symm c).symm
 #align category_theory.limits.is_limit.map_cone_equiv CategoryTheory.Limits.IsLimit.mapConeEquiv
 
 /-- A cone is a limit cone exactly if
 there is a unique cone morphism from any other cone.
 -/
-def isoUniqueConeMorphism {t : Cone F} : IsLimit t ≅ ∀ s, Unique (s ⟶ t)
-    where
-  Hom h s :=
+def isoUniqueConeMorphism {t : Cone F} : IsLimit t ≅ ∀ s, Unique (s ⟶ t) where
+  hom h s :=
     { default := h.liftConeMorphism s
       uniq := fun _ => h.uniq_cone_morphism }
   inv h :=
     { lift := fun s => (h s).default.Hom
-      uniq' := fun s f w => congr_arg ConeMorphism.hom ((h s).uniq ⟨f, w⟩) }
+      uniq := fun s f w => congrArg ConeMorphism.Hom ((h s).uniq ⟨f, w⟩) }
 #align category_theory.limits.is_limit.iso_unique_cone_morphism CategoryTheory.Limits.IsLimit.isoUniqueConeMorphism
 
 namespace OfNatIso
@@ -471,26 +480,28 @@ variable {X : C} (h : yoneda.obj X ⋙ uliftFunctor.{u₁} ≅ F.cones)
 /-- If `F.cones` is represented by `X`, each morphism `f : Y ⟶ X` gives a cone with cone point
 `Y`. -/
 def coneOfHom {Y : C} (f : Y ⟶ X) : Cone F where
-  x := Y
-  π := h.Hom.app (op Y) ⟨f⟩
+  X := Y
+  π := h.hom.app (op Y) ⟨f⟩
 #align category_theory.limits.is_limit.of_nat_iso.cone_of_hom CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom
 
 /-- If `F.cones` is represented by `X`, each cone `s` gives a morphism `s.X ⟶ X`. -/
-def homOfCone (s : Cone F) : s.x ⟶ X :=
-  (h.inv.app (op s.x) s.π).down
+def homOfCone (s : Cone F) : s.X ⟶ X :=
+  (h.inv.app (op s.X) s.π).down
 #align category_theory.limits.is_limit.of_nat_iso.hom_of_cone CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone
 
 @[simp]
-theorem coneOfHom_of_cone (s : Cone F) : coneOfHom h (homOfCone h s) = s := by
-  dsimp [cone_of_hom, hom_of_cone]; cases s; congr ; dsimp
-  convert congr_fun (congr_fun (congr_arg nat_trans.app h.inv_hom_id) (op s_X)) s_π
-  exact ULift.up_down _
-#align category_theory.limits.is_limit.of_nat_iso.cone_of_hom_of_cone CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_of_cone
+theorem coneOfHom_homOfCone (s : Cone F) : coneOfHom h (homOfCone h s) = s := by
+  dsimp [coneOfHom, homOfCone]; 
+  match s with 
+  | .mk s_X s_π => 
+    congr ; dsimp
+    convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) (op s_X)) s_π
+#align category_theory.limits.is_limit.of_nat_iso.cone_of_hom_of_cone CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_homOfCone
 
 @[simp]
-theorem homOfCone_of_hom {Y : C} (f : Y ⟶ X) : homOfCone h (coneOfHom h f) = f :=
-  congr_arg ULift.down (congr_fun (congr_fun (congr_arg NatTrans.app h.hom_inv_id) (op Y)) ⟨f⟩ : _)
-#align category_theory.limits.is_limit.of_nat_iso.hom_of_cone_of_hom CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_of_hom
+theorem homOfCone_coneOfHom {Y : C} (f : Y ⟶ X) : homOfCone h (coneOfHom h f) = f :=
+  congrArg ULift.down (congrFun (congrFun (congrArg NatTrans.app h.hom_inv_id) (op Y)) ⟨f⟩ : _)
+#align category_theory.limits.is_limit.of_nat_iso.hom_of_cone_of_hom CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom
 
 /-- If `F.cones` is represented by `X`, the cone corresponding to the identity morphism on `X`
 will be a limit cone. -/
@@ -501,21 +512,21 @@ def limitCone : Cone F :=
 /-- If `F.cones` is represented by `X`, the cone corresponding to a morphism `f : Y ⟶ X` is
 the limit cone extended by `f`. -/
 theorem coneOfHom_fac {Y : C} (f : Y ⟶ X) : coneOfHom h f = (limitCone h).extend f := by
-  dsimp [cone_of_hom, limit_cone, cone.extend]
+  dsimp [coneOfHom, limitCone, Cone.extend]
   congr with j
-  have t := congr_fun (h.hom.naturality f.op) ⟨𝟙 X⟩
+  have t := congrFun (h.hom.naturality f.op) ⟨𝟙 X⟩
   dsimp at t
   simp only [comp_id] at t
-  rw [congr_fun (congr_arg nat_trans.app t) j]
+  rw [congrFun (congrArg NatTrans.app t) j]
   rfl
 #align category_theory.limits.is_limit.of_nat_iso.cone_of_hom_fac CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac
 
 /-- If `F.cones` is represented by `X`, any cone is the extension of the limit cone by the
 corresponding morphism. -/
 theorem cone_fac (s : Cone F) : (limitCone h).extend (homOfCone h s) = s := by
-  rw [← cone_of_hom_of_cone h s]
-  conv_lhs => simp only [hom_of_cone_of_hom]
-  apply (cone_of_hom_fac _ _).symm
+  rw [← coneOfHom_homOfCone h s]
+  conv_lhs => simp only [homOfCone_coneOfHom]
+  apply (coneOfHom_fac _ _).symm
 #align category_theory.limits.is_limit.of_nat_iso.cone_fac CategoryTheory.Limits.IsLimit.OfNatIso.cone_fac
 
 end OfNatIso
@@ -530,17 +541,17 @@ the representing object is a limit cone.
 def ofNatIso {X : C} (h : yoneda.obj X ⋙ uliftFunctor.{u₁} ≅ F.cones) : IsLimit (limitCone h)
     where
   lift s := homOfCone h s
-  fac' s j := by
+  fac s j := by
     have h := cone_fac h s
     cases s
     injection h with h₁ h₂
     simp only [heq_iff_eq] at h₂
     conv_rhs => rw [← h₂]; rfl
-  uniq' s m w := by
-    rw [← hom_of_cone_of_hom h m]
+  uniq s m w := by
+    rw [← homOfCone_coneOfHom h m]
     congr
-    rw [cone_of_hom_fac]
-    dsimp [cone.extend]; cases s; congr with j; exact w j
+    rw [coneOfHom_fac]
+    dsimp [Cone.extend]; cases s; congr with j; exact w j
 #align category_theory.limits.is_limit.of_nat_iso CategoryTheory.Limits.IsLimit.ofNatIso
 
 end
@@ -552,42 +563,40 @@ cocone morphism from `t`.
 
 See <https://stacks.math.columbia.edu/tag/002F>.
 -/
-@[nolint has_nonempty_instance]
+-- Porting note: remove @[nolint has_nonempty_instance]
 structure IsColimit (t : Cocone F) where
-  desc : ∀ s : Cocone F, t.x ⟶ s.x
-  fac' : ∀ (s : Cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j := by obviously
-  uniq' :
-    ∀ (s : Cocone F) (m : t.x ⟶ s.x) (w : ∀ j : J, t.ι.app j ≫ m = s.ι.app j), m = desc s := by
-    obviously
+  desc : ∀ s : Cocone F, t.X ⟶ s.X
+  fac : ∀ (s : Cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j := by aesop_cat
+  uniq :
+    ∀ (s : Cocone F) (m : t.X ⟶ s.X) (_ : ∀ j : J, t.ι.app j ≫ m = s.ι.app j), m = desc s := by
+    aesop_cat
 #align category_theory.limits.is_colimit CategoryTheory.Limits.IsColimit
+#align category_theory.limits.is_colimit.fac' CategoryTheory.Limits.IsColimit.fac
+#align category_theory.limits.is_colimit.uniq' CategoryTheory.Limits.IsColimit.uniq
 
-restate_axiom is_colimit.fac'
-
-attribute [simp, reassoc.1] is_colimit.fac
-
-restate_axiom is_colimit.uniq'
+attribute [reassoc (attr := simp)] IsColimit.fac
 
 namespace IsColimit
 
 instance subsingleton {t : Cocone F} : Subsingleton (IsColimit t) :=
-  ⟨by intro P Q <;> cases P <;> cases Q <;> congr <;> ext <;> solve_by_elim⟩
+  ⟨by intro P Q ; cases P ; cases Q ; congr ; ext ; aesop_cat⟩
 #align category_theory.limits.is_colimit.subsingleton CategoryTheory.Limits.IsColimit.subsingleton
 
 /-- Given a natural transformation `α : F ⟶ G`, we give a morphism from the cocone point
 of a colimit cocone over `F` to the cocone point of any cocone over `G`. -/
-def map {F G : J ⥤ C} {s : Cocone F} (P : IsColimit s) (t : Cocone G) (α : F ⟶ G) : s.x ⟶ t.x :=
+def map {F G : J ⥤ C} {s : Cocone F} (P : IsColimit s) (t : Cocone G) (α : F ⟶ G) : s.X ⟶ t.X :=
   P.desc ((Cocones.precompose α).obj t)
 #align category_theory.limits.is_colimit.map CategoryTheory.Limits.IsColimit.map
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem ι_map {F G : J ⥤ C} {c : Cocone F} (hc : IsColimit c) (d : Cocone G) (α : F ⟶ G) (j : J) :
     c.ι.app j ≫ IsColimit.map hc d α = α.app j ≫ d.ι.app j :=
   fac _ _ _
 #align category_theory.limits.is_colimit.ι_map CategoryTheory.Limits.IsColimit.ι_map
 
 @[simp]
-theorem desc_self {t : Cocone F} (h : IsColimit t) : h.desc t = 𝟙 t.x :=
-  (h.uniq _ _ fun j => comp_id _).symm
+theorem desc_self {t : Cocone F} (h : IsColimit t) : h.desc t = 𝟙 t.X :=
+  (h.uniq _ _ fun _ => comp_id _).symm
 #align category_theory.limits.is_colimit.desc_self CategoryTheory.Limits.IsColimit.desc_self
 
 -- Repackaging the definition in terms of cocone morphisms.
@@ -597,19 +606,19 @@ def descCoconeMorphism {t : Cocone F} (h : IsColimit t) (s : Cocone F) : t ⟶ s
 #align category_theory.limits.is_colimit.desc_cocone_morphism CategoryTheory.Limits.IsColimit.descCoconeMorphism
 
 theorem uniq_cocone_morphism {s t : Cocone F} (h : IsColimit t) {f f' : t ⟶ s} : f = f' :=
-  have : ∀ {g : t ⟶ s}, g = h.descCoconeMorphism s := by intro g <;> ext <;> exact h.uniq _ _ g.w
+  have : ∀ {g : t ⟶ s}, g = h.descCoconeMorphism s := by intro g; aesop_cat; exact h.uniq _ _ g.w
   this.trans this.symm
 #align category_theory.limits.is_colimit.uniq_cocone_morphism CategoryTheory.Limits.IsColimit.uniq_cocone_morphism
 
 /-- Restating the definition of a colimit cocone in terms of the ∃! operator. -/
 theorem existsUnique {t : Cocone F} (h : IsColimit t) (s : Cocone F) :
-    ∃! d : t.x ⟶ s.x, ∀ j, t.ι.app j ≫ d = s.ι.app j :=
+    ∃! d : t.X ⟶ s.X, ∀ j, t.ι.app j ≫ d = s.ι.app j :=
   ⟨h.desc s, h.fac s, h.uniq s⟩
 #align category_theory.limits.is_colimit.exists_unique CategoryTheory.Limits.IsColimit.existsUnique
 
 /-- Noncomputably make a colimit cocone from the existence of unique factorizations. -/
 def ofExistsUnique {t : Cocone F}
-    (ht : ∀ s : Cocone F, ∃! d : t.x ⟶ s.x, ∀ j, t.ι.app j ≫ d = s.ι.app j) : IsColimit t := by
+    (ht : ∀ s : Cocone F, ∃! d : t.X ⟶ s.X, ∀ j, t.ι.app j ≫ d = s.ι.app j) : IsColimit t := by
   choose s hs hs' using ht
   exact ⟨s, hs, hs'⟩
 #align category_theory.limits.is_colimit.of_exists_unique CategoryTheory.Limits.IsColimit.ofExistsUnique
@@ -623,19 +632,19 @@ def mkCoconeMorphism {t : Cocone F} (desc : ∀ s : Cocone F, t ⟶ s)
     (uniq' : ∀ (s : Cocone F) (m : t ⟶ s), m = desc s) : IsColimit t
     where
   desc s := (desc s).Hom
-  uniq' s m w :=
+  uniq s m w :=
     have : CoconeMorphism.mk m w = desc s := by apply uniq'
-    congr_arg CoconeMorphism.hom this
+    congrArg CoconeMorphism.Hom this
 #align category_theory.limits.is_colimit.mk_cocone_morphism CategoryTheory.Limits.IsColimit.mkCoconeMorphism
 
 /-- Colimit cocones on `F` are unique up to isomorphism. -/
 @[simps]
 def uniqueUpToIso {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : s ≅ t
     where
-  Hom := P.descCoconeMorphism t
+  hom := P.descCoconeMorphism t
   inv := Q.descCoconeMorphism s
-  hom_inv_id' := P.uniq_cocone_morphism
-  inv_hom_id' := Q.uniq_cocone_morphism
+  hom_inv_id := P.uniq_cocone_morphism
+  inv_hom_id := Q.uniq_cocone_morphism
 #align category_theory.limits.is_colimit.unique_up_to_iso CategoryTheory.Limits.IsColimit.uniqueUpToIso
 
 /-- Any cocone morphism between colimit cocones is an isomorphism. -/
@@ -644,29 +653,29 @@ theorem hom_isIso {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (f : s 
 #align category_theory.limits.is_colimit.hom_is_iso CategoryTheory.Limits.IsColimit.hom_isIso
 
 /-- Colimits of `F` are unique up to isomorphism. -/
-def coconePointUniqueUpToIso {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : s.x ≅ t.x :=
+def coconePointUniqueUpToIso {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) : s.X ≅ t.X :=
   (Cocones.forget F).mapIso (uniqueUpToIso P Q)
 #align category_theory.limits.is_colimit.cocone_point_unique_up_to_iso CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem comp_coconePointUniqueUpToIso_hom {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t)
-    (j : J) : s.ι.app j ≫ (coconePointUniqueUpToIso P Q).Hom = t.ι.app j :=
-  (uniqueUpToIso P Q).Hom.w _
+    (j : J) : s.ι.app j ≫ (coconePointUniqueUpToIso P Q).hom = t.ι.app j :=
+  (uniqueUpToIso P Q).hom.w _
 #align category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_hom CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem comp_coconePointUniqueUpToIso_inv {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t)
     (j : J) : t.ι.app j ≫ (coconePointUniqueUpToIso P Q).inv = s.ι.app j :=
   (uniqueUpToIso P Q).inv.w _
 #align category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_inv CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem coconePointUniqueUpToIso_hom_desc {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) :
-    (coconePointUniqueUpToIso P Q).Hom ≫ Q.desc r = P.desc r :=
+    (coconePointUniqueUpToIso P Q).hom ≫ Q.desc r = P.desc r :=
   P.uniq _ _ (by simp)
 #align category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_hom_desc CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc
 
-@[simp, reassoc.1]
+@[reassoc (attr := simp)]
 theorem coconePointUniqueUpToIso_inv_desc {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) :
     (coconePointUniqueUpToIso P Q).inv ≫ P.desc r = Q.desc r :=
   Q.uniq _ _ (by simp)
@@ -675,7 +684,7 @@ theorem coconePointUniqueUpToIso_inv_desc {r s t : Cocone F} (P : IsColimit s) (
 /-- Transport evidence that a cocone is a colimit cocone across an isomorphism of cocones. -/
 def ofIsoColimit {r t : Cocone F} (P : IsColimit r) (i : r ≅ t) : IsColimit t :=
   IsColimit.mkCoconeMorphism (fun s => i.inv ≫ P.descCoconeMorphism s) fun s m => by
-    rw [i.eq_inv_comp] <;> apply P.uniq_cocone_morphism
+    rw [i.eq_inv_comp]; apply P.uniq_cocone_morphism
 #align category_theory.limits.is_colimit.of_iso_colimit CategoryTheory.Limits.IsColimit.ofIsoColimit
 
 @[simp]
@@ -689,8 +698,8 @@ def equivIsoColimit {r t : Cocone F} (i : r ≅ t) : IsColimit r ≃ IsColimit t
     where
   toFun h := h.ofIsoColimit i
   invFun h := h.ofIsoColimit i.symm
-  left_inv := by tidy
-  right_inv := by tidy
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
 #align category_theory.limits.is_colimit.equiv_iso_colimit CategoryTheory.Limits.IsColimit.equivIsoColimit
 
 @[simp]
@@ -711,33 +720,33 @@ first cocone was colimiting also.
 def ofPointIso {r t : Cocone F} (P : IsColimit r) [i : IsIso (P.desc t)] : IsColimit t :=
   ofIsoColimit P
     (by
-      haveI : is_iso (P.desc_cocone_morphism t).Hom := i
-      haveI : is_iso (P.desc_cocone_morphism t) := cocones.cocone_iso_of_hom_iso _
-      apply as_iso (P.desc_cocone_morphism t))
+      haveI : IsIso (P.descCoconeMorphism t).Hom := i
+      haveI : IsIso (P.descCoconeMorphism t) := Cocones.cocone_iso_of_hom_iso _
+      apply asIso (P.descCoconeMorphism t))
 #align category_theory.limits.is_colimit.of_point_iso CategoryTheory.Limits.IsColimit.ofPointIso
 
 variable {t : Cocone F}
 
-theorem hom_desc (h : IsColimit t) {W : C} (m : t.x ⟶ W) :
+theorem hom_desc (h : IsColimit t) {W : C} (m : t.X ⟶ W) :
     m =
       h.desc
-        { x := W
+        { X := W
           ι :=
             { app := fun b => t.ι.app b ≫ m
-              naturality' := by intros <;> erw [← assoc, t.ι.naturality, comp_id, comp_id] } } :=
+              naturality := by intros; erw [← assoc, t.ι.naturality, comp_id, comp_id] } } :=
   h.uniq
-    { x := W
+    { X := W
       ι :=
         { app := fun b => t.ι.app b ≫ m
-          naturality' := _ } }
-    m fun b => rfl
+          naturality := _ } }
+    m fun _ => rfl
 #align category_theory.limits.is_colimit.hom_desc CategoryTheory.Limits.IsColimit.hom_desc
 
 /-- Two morphisms out of a colimit are equal if their compositions with
   each cocone morphism are equal. -/
-theorem hom_ext (h : IsColimit t) {W : C} {f f' : t.x ⟶ W}
+theorem hom_ext (h : IsColimit t) {W : C} {f f' : t.X ⟶ W}
     (w : ∀ j, t.ι.app j ≫ f = t.ι.app j ≫ f') : f = f' := by
-  rw [h.hom_desc f, h.hom_desc f'] <;> congr <;> exact funext w
+  rw [h.hom_desc f, h.hom_desc f']; congr; exact funext w
 #align category_theory.limits.is_colimit.hom_ext CategoryTheory.Limits.IsColimit.hom_ext
 
 /-- Given a left adjoint functor between categories of cocones,
@@ -746,7 +755,7 @@ the image of a colimit cocone is a colimit cocone.
 def ofLeftAdjoint {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cocone G ⥤ Cocone F)
     [IsLeftAdjoint h] {c : Cocone G} (t : IsColimit c) : IsColimit (h.obj c) :=
   mkCoconeMorphism
-    (fun s => ((Adjunction.ofLeftAdjoint h).homEquiv c s).symm (t.descCoconeMorphism _)) fun s m =>
+    (fun s => ((Adjunction.ofLeftAdjoint h).homEquiv c s).symm (t.descCoconeMorphism _)) fun _ _ =>
     (Adjunction.homEquiv_apply_eq _ _ _).1 t.uniq_cocone_morphism
 #align category_theory.limits.is_colimit.of_left_adjoint CategoryTheory.Limits.IsColimit.ofLeftAdjoint
 
@@ -754,20 +763,20 @@ def ofLeftAdjoint {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cocone
 we can transport a colimiting cocone across the equivalence.
 -/
 def ofCoconeEquiv {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cocone G ≌ Cocone F)
-    {c : Cocone G} : IsColimit (h.Functor.obj c) ≃ IsColimit c
+    {c : Cocone G} : IsColimit (h.functor.obj c) ≃ IsColimit c
     where
   toFun P := ofIsoColimit (ofLeftAdjoint h.inverse P) (h.unitIso.symm.app c)
-  invFun := ofLeftAdjoint h.Functor
-  left_inv := by tidy
-  right_inv := by tidy
+  invFun := ofLeftAdjoint h.functor
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
 #align category_theory.limits.is_colimit.of_cocone_equiv CategoryTheory.Limits.IsColimit.ofCoconeEquiv
 
 @[simp]
 theorem ofCoconeEquiv_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D}
-    (h : Cocone G ≌ Cocone F) {c : Cocone G} (P : IsColimit (h.Functor.obj c)) (s) :
+    (h : Cocone G ≌ Cocone F) {c : Cocone G} (P : IsColimit (h.functor.obj c)) (s) :
     (ofCoconeEquiv h P).desc s =
-      (h.Unit.app c).Hom ≫
-        (h.inverse.map (P.descCoconeMorphism (h.Functor.obj s))).Hom ≫ (h.unitInv.app s).Hom :=
+      (h.unit.app c).Hom ≫
+        (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))).Hom ≫ (h.unitInv.app s).Hom :=
   rfl
 #align category_theory.limits.is_colimit.of_cocone_equiv_apply_desc CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc
 
@@ -775,7 +784,7 @@ theorem ofCoconeEquiv_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤
 theorem ofCoconeEquiv_symm_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D}
     (h : Cocone G ≌ Cocone F) {c : Cocone G} (P : IsColimit c) (s) :
     ((ofCoconeEquiv h).symm P).desc s =
-      (h.Functor.map (P.descCoconeMorphism (h.inverse.obj s))).Hom ≫ (h.counit.app s).Hom :=
+      (h.functor.map (P.descCoconeMorphism (h.inverse.obj s))).Hom ≫ (h.counit.app s).Hom :=
   rfl
 #align category_theory.limits.is_colimit.of_cocone_equiv_symm_apply_desc CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc
 
@@ -783,7 +792,7 @@ theorem ofCoconeEquiv_symm_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K
 if and only if the original cocone is.
 -/
 def precomposeHomEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cocone G) :
-    IsColimit ((Cocones.precompose α.Hom).obj c) ≃ IsColimit c :=
+    IsColimit ((Cocones.precompose α.hom).obj c) ≃ IsColimit c :=
   ofCoconeEquiv (Cocones.precomposeEquivalence α)
 #align category_theory.limits.is_colimit.precompose_hom_equiv CategoryTheory.Limits.IsColimit.precomposeHomEquiv
 
@@ -808,34 +817,34 @@ are themselves isomorphic.
 -/
 @[simps]
 def coconePointsIsoOfNatIso {F G : J ⥤ C} {s : Cocone F} {t : Cocone G} (P : IsColimit s)
-    (Q : IsColimit t) (w : F ≅ G) : s.x ≅ t.x
+    (Q : IsColimit t) (w : F ≅ G) : s.X ≅ t.X
     where
-  Hom := P.map t w.Hom
+  hom := P.map t w.hom
   inv := Q.map s w.inv
-  hom_inv_id' := P.hom_ext (by tidy)
-  inv_hom_id' := Q.hom_ext (by tidy)
+  hom_inv_id := P.hom_ext (by aesop_cat)
+  inv_hom_id := Q.hom_ext (by aesop_cat)
 #align category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso
 
-@[reassoc.1]
+@[reassoc]
 theorem comp_coconePointsIsoOfNatIso_hom {F G : J ⥤ C} {s : Cocone F} {t : Cocone G}
     (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) :
-    s.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).Hom = w.Hom.app j ≫ t.ι.app j := by simp
+    s.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).hom = w.hom.app j ≫ t.ι.app j := by simp
 #align category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_hom CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom
 
-@[reassoc.1]
+@[reassoc]
 theorem comp_coconePointsIsoOfNatIso_inv {F G : J ⥤ C} {s : Cocone F} {t : Cocone G}
     (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) (j : J) :
     t.ι.app j ≫ (coconePointsIsoOfNatIso P Q w).inv = w.inv.app j ≫ s.ι.app j := by simp
 #align category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_inv CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv
 
-@[reassoc.1]
+@[reassoc]
 theorem coconePointsIsoOfNatIso_hom_desc {F G : J ⥤ C} {s : Cocone F} {r t : Cocone G}
     (P : IsColimit s) (Q : IsColimit t) (w : F ≅ G) :
-    (coconePointsIsoOfNatIso P Q w).Hom ≫ Q.desc r = P.map _ w.Hom :=
+    (coconePointsIsoOfNatIso P Q w).hom ≫ Q.desc r = P.map _ w.hom :=
   P.hom_ext (by simp)
 #align category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_hom_desc CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc
 
-@[reassoc.1]
+@[reassoc]
 theorem coconePointsIsoOfNatIso_inv_desc {F G : J ⥤ C} {s : Cocone G} {r t : Cocone F}
     (P : IsColimit t) (Q : IsColimit s) (w : F ≅ G) :
     (coconePointsIsoOfNatIso P Q w).inv ≫ P.desc r = Q.map _ w.inv :=
@@ -849,13 +858,13 @@ open CategoryTheory.Equivalence
 /-- If `s : cocone F` is a colimit cocone, so is `s` whiskered by an equivalence `e`.
 -/
 def whiskerEquivalence {s : Cocone F} (P : IsColimit s) (e : K ≌ J) :
-    IsColimit (s.whisker e.Functor) :=
-  ofLeftAdjoint (Cocones.whiskeringEquivalence e).Functor P
+    IsColimit (s.whisker e.functor) :=
+  ofLeftAdjoint (Cocones.whiskeringEquivalence e).functor P
 #align category_theory.limits.is_colimit.whisker_equivalence CategoryTheory.Limits.IsColimit.whiskerEquivalence
 
 /-- If `s : cocone F` whiskered by an equivalence `e` is a colimit cocone, so is `s`.
 -/
-def ofWhiskerEquivalence {s : Cocone F} (e : K ≌ J) (P : IsColimit (s.whisker e.Functor)) :
+def ofWhiskerEquivalence {s : Cocone F} (e : K ≌ J) (P : IsColimit (s.whisker e.functor)) :
     IsColimit s :=
   equivIsoColimit ((Cocones.whiskeringEquivalence e).unitIso.app s).symm
     (ofLeftAdjoint (Cocones.whiskeringEquivalence e).inverse P : _)
@@ -864,8 +873,8 @@ def ofWhiskerEquivalence {s : Cocone F} (e : K ≌ J) (P : IsColimit (s.whisker
 /-- Given an equivalence of diagrams `e`, `s` is a colimit cocone iff `s.whisker e.functor` is.
 -/
 def whiskerEquivalenceEquiv {s : Cocone F} (e : K ≌ J) :
-    IsColimit s ≃ IsColimit (s.whisker e.Functor) :=
-  ⟨fun h => h.whiskerEquivalence e, ofWhiskerEquivalence e, by tidy, by tidy⟩
+    IsColimit s ≃ IsColimit (s.whisker e.functor) :=
+  ⟨fun h => h.whiskerEquivalence e, ofWhiskerEquivalence e, by aesop_cat, by aesop_cat⟩
 #align category_theory.limits.is_colimit.whisker_equivalence_equiv CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv
 
 /-- We can prove two cocone points `(s : cocone F).X` and `(t.cocone G).X` are isomorphic if
@@ -879,75 +888,78 @@ and the functor (up to natural isomorphism).
 -/
 @[simps]
 def coconePointsIsoOfEquivalence {F : J ⥤ C} {s : Cocone F} {G : K ⥤ C} {t : Cocone G}
-    (P : IsColimit s) (Q : IsColimit t) (e : J ≌ K) (w : e.Functor ⋙ G ≅ F) : s.x ≅ t.x :=
+    (P : IsColimit s) (Q : IsColimit t) (e : J ≌ K) (w : e.functor ⋙ G ≅ F) : s.X ≅ t.X :=
   let w' : e.inverse ⋙ F ≅ G := (isoWhiskerLeft e.inverse w).symm ≪≫ invFunIdAssoc e G
-  { Hom := P.desc ((Cocones.equivalenceOfReindexing e w).Functor.obj t)
-    inv := Q.desc ((Cocones.equivalenceOfReindexing e.symm w').Functor.obj s)
-    hom_inv_id' := by
+  { hom := P.desc ((Cocones.equivalenceOfReindexing e w).functor.obj t)
+    inv := Q.desc ((Cocones.equivalenceOfReindexing e.symm w').functor.obj s)
+    hom_inv_id := by
       apply hom_ext P; intro j
       dsimp
-      simp only [limits.cocone.whisker_ι, fac, inv_fun_id_assoc_inv_app, whisker_left_app, assoc,
-        comp_id, limits.cocones.precompose_obj_ι, fac_assoc, nat_trans.comp_app]
-      rw [counit_inv_app_functor, ← functor.comp_map, ← w.inv.naturality_assoc]
+      simp only [Limits.Cocone.whisker_ι, fac, invFunIdAssoc_inv_app, whiskerLeft_app, assoc,
+        comp_id, Limits.Cocones.precompose_obj_ι, fac_assoc, NatTrans.comp_app]
+      rw [counitInv_app_functor, ← Functor.comp_map, ← w.inv.naturality_assoc]
       dsimp
       simp
-    inv_hom_id' := by
+    inv_hom_id := by
       apply hom_ext Q
-      tidy }
+      aesop_cat }
 #align category_theory.limits.is_colimit.cocone_points_iso_of_equivalence CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence
 
 end Equivalence
 
 /-- The universal property of a colimit cocone: a map `X ⟶ W` is the same as
   a cocone on `F` with vertex `W`. -/
-def homIso (h : IsColimit t) (W : C) : ULift.{u₁} (t.x ⟶ W : Type v₃) ≅ F ⟶ (const J).obj W
-    where
-  Hom f := (t.extend f.down).ι
+def homIso (h : IsColimit t) (W : C) : ULift.{u₁} (t.X ⟶ W : Type v₃) ≅ F ⟶ (const J).obj W where
+  hom f := (t.extend f.down).ι
   inv ι :=
     ⟨h.desc
-        { x := W
+        { X := W
           ι }⟩
-  hom_inv_id' := by ext f <;> apply h.hom_ext <;> intro j <;> simp <;> dsimp <;> rfl
+  hom_inv_id := by 
+    funext f; apply ULift.ext
+    apply h.hom_ext; intro j; simp
+  inv_hom_id := by 
+    funext f; dsimp [const]; aesop_cat
 #align category_theory.limits.is_colimit.hom_iso CategoryTheory.Limits.IsColimit.homIso
 
 @[simp]
-theorem homIso_hom (h : IsColimit t) {W : C} (f : ULift (t.x ⟶ W)) :
-    (IsColimit.homIso h W).Hom f = (t.extend f.down).ι :=
+theorem homIso_hom (h : IsColimit t) {W : C} (f : ULift (t.X ⟶ W)) :
+    (IsColimit.homIso h W).hom f = (t.extend f.down).ι :=
   rfl
 #align category_theory.limits.is_colimit.hom_iso_hom CategoryTheory.Limits.IsColimit.homIso_hom
 
 /-- The colimit of `F` represents the functor taking `W` to
   the set of cocones on `F` with vertex `W`. -/
-def natIso (h : IsColimit t) : coyoneda.obj (op t.x) ⋙ uliftFunctor.{u₁} ≅ F.cocones :=
-  NatIso.ofComponents (IsColimit.homIso h) (by intros <;> ext <;> dsimp <;> rw [← assoc] <;> rfl)
+def natIso (h : IsColimit t) : coyoneda.obj (op t.X) ⋙ uliftFunctor.{u₁} ≅ F.cocones :=
+  NatIso.ofComponents (IsColimit.homIso h) (by intros; funext; aesop_cat)
 #align category_theory.limits.is_colimit.nat_iso CategoryTheory.Limits.IsColimit.natIso
 
 /-- Another, more explicit, formulation of the universal property of a colimit cocone.
 See also `hom_iso`.
 -/
 def homIso' (h : IsColimit t) (W : C) :
-    ULift.{u₁} (t.x ⟶ W : Type v₃) ≅
+    ULift.{u₁} (t.X ⟶ W : Type v₃) ≅
       { p : ∀ j, F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j } :=
   h.homIso W ≪≫
-    { Hom := fun ι =>
-        ⟨fun j => ι.app j, fun j j' f => by convert ← ι.naturality f <;> apply comp_id⟩
+    { hom := fun ι =>
+        ⟨fun j => ι.app j, fun {j} {j'} f => by convert ← ι.naturality f; apply comp_id⟩
       inv := fun p =>
         { app := fun j => p.1 j
-          naturality' := fun j j' f => by dsimp; rw [comp_id]; exact p.2 f } }
+          naturality := fun j j' f => by dsimp; rw [comp_id]; exact p.2 f } }
 #align category_theory.limits.is_colimit.hom_iso' CategoryTheory.Limits.IsColimit.homIso'
 
 /-- If G : C → D is a faithful functor which sends t to a colimit cocone,
   then it suffices to check that the induced maps for the image of t
   can be lifted to maps of C. -/
 def ofFaithful {t : Cocone F} {D : Type u₄} [Category.{v₄} D] (G : C ⥤ D) [Faithful G]
-    (ht : IsColimit (G.mapCocone t)) (desc : ∀ s : Cocone F, t.x ⟶ s.x)
-    (h : ∀ s, G.map (desc s) = ht.desc (G.mapCocone s)) : IsColimit t :=
+    (ht : IsColimit (mapCocone G t)) (desc : ∀ s : Cocone F, t.X ⟶ s.X)
+    (h : ∀ s, G.map (desc s) = ht.desc (mapCocone G s)) : IsColimit t :=
   { desc
-    fac' := fun s j => by apply G.map_injective <;> rw [G.map_comp, h] <;> apply ht.fac
-    uniq' := fun s m w => by
+    fac := fun s j => by apply G.map_injective ; rw [G.map_comp, h] ; apply ht.fac
+    uniq := fun s m w => by
       apply G.map_injective; rw [h]
-      refine' ht.uniq (G.map_cocone s) _ fun j => _
-      convert ← congr_arg (fun f => G.map f) (w j)
+      refine' ht.uniq (mapCocone G s) _ fun j => _
+      convert ← congrArg (fun f => G.map f) (w j)
       apply G.map_comp }
 #align category_theory.limits.is_colimit.of_faithful CategoryTheory.Limits.IsColimit.ofFaithful
 
@@ -955,22 +967,21 @@ def ofFaithful {t : Cocone F} {D : Type u₄} [Category.{v₄} D] (G : C ⥤ D)
 `G.map_cone c` is also a colimit.
 -/
 def mapCoconeEquiv {D : Type u₄} [Category.{v₄} D] {K : J ⥤ C} {F G : C ⥤ D} (h : F ≅ G)
-    {c : Cocone K} (t : IsColimit (F.mapCocone c)) : IsColimit (G.mapCocone c) := by
-  apply is_colimit.of_iso_colimit _ (precompose_whisker_left_map_cocone h c)
-  apply (precompose_inv_equiv (iso_whisker_left K h : _) _).symm t
+    {c : Cocone K} (t : IsColimit (mapCocone F c)) : IsColimit (mapCocone G c) := by
+  apply IsColimit.ofIsoColimit _ (precomposeWhiskerLeftMapCocone h c)
+  apply (precomposeInvEquiv (isoWhiskerLeft K h : _) _).symm t
 #align category_theory.limits.is_colimit.map_cocone_equiv CategoryTheory.Limits.IsColimit.mapCoconeEquiv
 
 /-- A cocone is a colimit cocone exactly if
 there is a unique cocone morphism from any other cocone.
 -/
-def isoUniqueCoconeMorphism {t : Cocone F} : IsColimit t ≅ ∀ s, Unique (t ⟶ s)
-    where
-  Hom h s :=
+def isoUniqueCoconeMorphism {t : Cocone F} : IsColimit t ≅ ∀ s, Unique (t ⟶ s) where
+  hom h s :=
     { default := h.descCoconeMorphism s
       uniq := fun _ => h.uniq_cocone_morphism }
   inv h :=
     { desc := fun s => (h s).default.Hom
-      uniq' := fun s f w => congr_arg CoconeMorphism.hom ((h s).uniq ⟨f, w⟩) }
+      uniq := fun s f w => congrArg CoconeMorphism.Hom ((h s).uniq ⟨f, w⟩) }
 #align category_theory.limits.is_colimit.iso_unique_cocone_morphism CategoryTheory.Limits.IsColimit.isoUniqueCoconeMorphism
 
 namespace OfNatIso
@@ -981,26 +992,27 @@ variable {X : C} (h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁} ≅ F.cocones)
 point `Y`. -/
 def coconeOfHom {Y : C} (f : X ⟶ Y) : Cocone F
     where
-  x := Y
-  ι := h.Hom.app Y ⟨f⟩
+  X := Y
+  ι := h.hom.app Y ⟨f⟩
 #align category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom
 
 /-- If `F.cocones` is corepresented by `X`, each cocone `s` gives a morphism `X ⟶ s.X`. -/
-def homOfCocone (s : Cocone F) : X ⟶ s.x :=
-  (h.inv.app s.x s.ι).down
+def homOfCocone (s : Cocone F) : X ⟶ s.X:=
+  (h.inv.app s.X s.ι).down
 #align category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone
 
 @[simp]
-theorem coconeOfHom_of_cocone (s : Cocone F) : coconeOfHom h (homOfCocone h s) = s := by
-  dsimp [cocone_of_hom, hom_of_cocone]; cases s; congr ; dsimp
-  convert congr_fun (congr_fun (congr_arg nat_trans.app h.inv_hom_id) s_X) s_ι
-  exact ULift.up_down _
-#align category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom_of_cocone CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_of_cocone
+theorem coconeOfHom_homOfCocone (s : Cocone F) : coconeOfHom h (homOfCocone h s) = s := by
+  dsimp [coconeOfHom, homOfCocone]; 
+  have ⟨s_X,s_ι⟩ := s
+  congr ; dsimp
+  convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) s_X) s_ι
+#align category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom_of_cocone CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_homOfCocone
 
 @[simp]
-theorem homOfCocone_of_hom {Y : C} (f : X ⟶ Y) : homOfCocone h (coconeOfHom h f) = f :=
-  congr_arg ULift.down (congr_fun (congr_fun (congr_arg NatTrans.app h.hom_inv_id) Y) ⟨f⟩ : _)
-#align category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone_of_hom CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_of_hom
+theorem homOfCocone_cooneOfHom {Y : C} (f : X ⟶ Y) : homOfCocone h (coconeOfHom h f) = f :=
+  congrArg ULift.down (congrFun (congrFun (congrArg NatTrans.app h.hom_inv_id) Y) ⟨f⟩ : _)
+#align category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone_of_hom CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_cooneOfHom
 
 /-- If `F.cocones` is corepresented by `X`, the cocone corresponding to the identity morphism on `X`
 will be a colimit cocone. -/
@@ -1011,21 +1023,21 @@ def colimitCocone : Cocone F :=
 /-- If `F.cocones` is corepresented by `X`, the cocone corresponding to a morphism `f : Y ⟶ X` is
 the colimit cocone extended by `f`. -/
 theorem coconeOfHom_fac {Y : C} (f : X ⟶ Y) : coconeOfHom h f = (colimitCocone h).extend f := by
-  dsimp [cocone_of_hom, colimit_cocone, cocone.extend]
+  dsimp [coconeOfHom, colimitCocone, Cocone.extend]
   congr with j
-  have t := congr_fun (h.hom.naturality f) ⟨𝟙 X⟩
+  have t := congrFun (h.hom.naturality f) ⟨𝟙 X⟩
   dsimp at t
   simp only [id_comp] at t
-  rw [congr_fun (congr_arg nat_trans.app t) j]
+  rw [congrFun (congrArg NatTrans.app t) j]
   rfl
 #align category_theory.limits.is_colimit.of_nat_iso.cocone_of_hom_fac CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_fac
 
 /-- If `F.cocones` is corepresented by `X`, any cocone is the extension of the colimit cocone by the
 corresponding morphism. -/
 theorem cocone_fac (s : Cocone F) : (colimitCocone h).extend (homOfCocone h s) = s := by
-  rw [← cocone_of_hom_of_cocone h s]
-  conv_lhs => simp only [hom_of_cocone_of_hom]
-  apply (cocone_of_hom_fac _ _).symm
+  rw [← coconeOfHom_homOfCocone h s]
+  conv_lhs => simp only [homOfCocone_cooneOfHom]
+  apply (coconeOfHom_fac _ _).symm
 #align category_theory.limits.is_colimit.of_nat_iso.cocone_fac CategoryTheory.Limits.IsColimit.OfNatIso.cocone_fac
 
 end OfNatIso
@@ -1040,17 +1052,17 @@ the representing object is a colimit cocone.
 def ofNatIso {X : C} (h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁} ≅ F.cocones) :
     IsColimit (colimitCocone h) where
   desc s := homOfCocone h s
-  fac' s j := by
+  fac s j := by
     have h := cocone_fac h s
     cases s
     injection h with h₁ h₂
     simp only [heq_iff_eq] at h₂
     conv_rhs => rw [← h₂]; rfl
-  uniq' s m w := by
-    rw [← hom_of_cocone_of_hom h m]
+  uniq s m w := by
+    rw [← homOfCocone_cooneOfHom h m]
     congr
-    rw [cocone_of_hom_fac]
-    dsimp [cocone.extend]; cases s; congr with j; exact w j
+    rw [coconeOfHom_fac]
+    dsimp [Cocone.extend]; cases s; congr with j; exact w j
 #align category_theory.limits.is_colimit.of_nat_iso CategoryTheory.Limits.IsColimit.ofNatIso
 
 end