From 8fcb2164edf97b22a26f1f2a656b98825378cbea Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Sat, 18 Feb 2023 21:19:06 -0500
Subject: [PATCH] # This is a combination of 126 commits. # This is the 1st
 commit message:

automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean

# The commit message #2 will be skipped:

# feat: port CategoryTheory.Limits.IsLimit

# The commit message #3 will be skipped:

# Initial file copy from mathport

# The commit message #4 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #5 will be skipped:

# feat: port CategoryTheory.Limits.Cones

# The commit message #6 will be skipped:

# Initial file copy from mathport

# The commit message #7 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #8 will be skipped:

# feat: port CategoryTheory.Yoneda

# The commit message #9 will be skipped:

# Initial file copy from mathport

# The commit message #10 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #11 will be skipped:

# feat: port CategoryTheory.Functor.Currying

# The commit message #12 will be skipped:

# Initial file copy from mathport

# The commit message #13 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #14 will be skipped:

# fix all but one decl

# The commit message #15 will be skipped:

# fix last errors

# The commit message #16 will be skipped:

# feat: port CategoryTheory.Functor.Hom

# The commit message #17 will be skipped:

# Initial file copy from mathport

# The commit message #18 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #19 will be skipped:

# feat: port CategoryTheory.Types

# The commit message #20 will be skipped:

# Initial file copy from mathport

# The commit message #21 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #22 will be skipped:

# feat: port CategoryTheory.EpiMono

# The commit message #23 will be skipped:

# Initial file copy from mathport

# The commit message #24 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #25 will be skipped:

# feat: port CategoryTheory.Groupoid

# The commit message #26 will be skipped:

# Initial file copy from mathport

# The commit message #27 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #28 will be skipped:

# feat: port CategoryTheory.Pi.Basic

# The commit message #29 will be skipped:

# Initial file copy from mathport

# The commit message #30 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #31 will be skipped:

# fix some errors

# The commit message #32 will be skipped:

# some more fixes

# The commit message #33 will be skipped:

# more fixes

# The commit message #34 will be skipped:

# finally fixed

# The commit message #35 will be skipped:

# lint

# The commit message #36 will be skipped:

# add porting note for scary warning

# The commit message #37 will be skipped:

# add porting note about proliferation of match

# The commit message #38 will be skipped:

# initial pass

# The commit message #39 will be skipped:

# fix errors

# The commit message #40 will be skipped:

# lint

# The commit message #41 will be skipped:

# fix errors; lint; add porting notes

# The commit message #42 will be skipped:

# fix errors; lint; add porting note

# The commit message #43 will be skipped:

# fix error

# The commit message #44 will be skipped:

# fix some errors

# The commit message #45 will be skipped:

# minor fixes

# The commit message #46 will be skipped:

# fix all but four

# The commit message #47 will be skipped:

# fix last errors; lint

# The commit message #48 will be skipped:

# feat: port CategoryTheory.DiscreteCategory

# The commit message #49 will be skipped:

# Initial file copy from mathport

# The commit message #50 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #51 will be skipped:

# get file to build

# The commit message #52 will be skipped:

# lint

# The commit message #53 will be skipped:

# lint some more

# The commit message #54 will be skipped:

# feat: port CategoryTheory.Functor.ReflectsIsomorphisms

# The commit message #55 will be skipped:

# Initial file copy from mathport

# The commit message #56 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #57 will be skipped:

# feat: port CategoryTheory.Functor.EpiMono

# The commit message #58 will be skipped:

# Initial file copy from mathport

# The commit message #59 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #60 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Adjunction

# The commit message #61 will be skipped:

# Initial file copy from mathport

# The commit message #62 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #63 will be skipped:

# feat: port CategoryTheory.LiftingProperties.Basic

# The commit message #64 will be skipped:

# Initial file copy from mathport

# The commit message #65 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #66 will be skipped:

# feat: port CategoryTheory.CommSq

# The commit message #67 will be skipped:

# Initial file copy from mathport

# The commit message #68 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #69 will be skipped:

# first pass

# The commit message #70 will be skipped:

# names and removing restate_axiom

# The commit message #71 will be skipped:

# fix lint

# The commit message #72 will be skipped:

# remove spurious edit

# The commit message #73 will be skipped:

# fix errors; lint

# The commit message #74 will be skipped:

# feat: port CategoryTheory.Adjunction.Basic

# The commit message #75 will be skipped:

# Initial file copy from mathport

# The commit message #76 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #77 will be skipped:

# Initial file copy from mathport

# The commit message #78 will be skipped:

# Mathbin -> Mathlib; add import to Mathlib.lean

# The commit message #79 will be skipped:

# push it as far as possible

# The commit message #80 will be skipped:

# minor changes

# The commit message #81 will be skipped:

# seems to work

# The commit message #82 will be skipped:

# add example and equivalence file for testing

# The commit message #83 will be skipped:

# test: create `slice.lean` test file

# The commit message #84 will be skipped:

# remove equivalence.lean

# The commit message #85 will be skipped:

# remove rewriteTarget'; change MonadExceptOf to MonadExcept

# The commit message #86 will be skipped:

# add documentation and clean up

# The commit message #87 will be skipped:

# move iteration tactics to core

# The commit message #88 will be skipped:

# modify documentation lines

# The commit message #89 will be skipped:

# add module documentation(?)

# The commit message #90 will be skipped:

# fix module docs

# The commit message #91 will be skipped:

# fix test/slice.lean

# The commit message #92 will be skipped:

# fix all but refl error

# The commit message #93 will be skipped:

# fix refl error and lint errors

# The commit message #94 will be skipped:

# fix final long line

# The commit message #95 will be skipped:

# use `Mathport` syntax
# * use existing docs
# * fix docs typos

# The commit message #96 will be skipped:

# test: add simple `rhs`/`lhs` tests

# The commit message #97 will be skipped:

# minor changes to `Tactic.Core`
# * use `m` instead of `TacticM` now that we use `MonadExcept`
# * simplify code for `iterateRange`
# * minor docs tweaks

# The commit message #98 will be skipped:

# update slice naming

# The commit message #99 will be skipped:

# some progress

# The commit message #100 will be skipped:

# only one error left

# The commit message #101 will be skipped:

# filled in last sorry

# The commit message #102 will be skipped:

# break long lines

# The commit message #103 will be skipped:

# delete linter command

# The commit message #104 will be skipped:

# fix comments

# The commit message #105 will be skipped:

# fix two simpNF lints

# The commit message #106 will be skipped:

# fill in some docstrings

# The commit message #107 will be skipped:

# fix most linter issues

# The commit message #108 will be skipped:

# add missing aligns for fields; lint

# The commit message #109 will be skipped:

# restore lost import line

# The commit message #110 will be skipped:

# fix errors; lint

# The commit message #111 will be skipped:

# feat: port CategoryTheory.Limits.Shapes.StrongEpi

# The commit message #112 will be skipped:

# Initial file copy from mathport

# The commit message #113 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean

# The commit message #114 will be skipped:

# fix errors; lint

# The commit message #115 will be skipped:

# Update Mathlib.lean

# The commit message #116 will be skipped:

# fix errors; lint

# The commit message #117 will be skipped:

# fix errors; lint; shorten filename

# The commit message #118 will be skipped:

# fix some errors

# The commit message #119 will be skipped:

# fix some more

# The commit message #120 will be skipped:

# fix errors

# The commit message #121 will be skipped:

# lint

# The commit message #122 will be skipped:

# fix errors

# The commit message #123 will be skipped:

# lint

# The commit message #124 will be skipped:

# feat: port CategoryTheory.Category.Ulift

# The commit message #125 will be skipped:

# Initial file copy from mathport

# The commit message #126 will be skipped:

# automated fixes
#
# Mathbin -> Mathlib
#
# fix certain import statements
#
# move "by" to end of line
#
# add import to Mathlib.lean
---
 Mathlib.lean                                  |   22 +-
 Mathlib/CategoryTheory/Adjunction/Basic.lean  |   10 +-
 Mathlib/CategoryTheory/Category/Ulift.lean    |  223 ++++
 Mathlib/CategoryTheory/CommSq.lean            |   19 +-
 Mathlib/CategoryTheory/DiscreteCategory.lean  |   78 +-
 Mathlib/CategoryTheory/Equivalence.lean       |  228 ++--
 Mathlib/CategoryTheory/Equivalence.lean.orig  |  813 +++++++++++++
 Mathlib/CategoryTheory/Functor/Currying.lean  |    4 +-
 Mathlib/CategoryTheory/Groupoid.lean          |    6 +-
 Mathlib/CategoryTheory/Iso.lean               |    7 +-
 Mathlib/CategoryTheory/Limits/Cones.lean      |  114 +-
 Mathlib/CategoryTheory/Limits/HasLimits.lean  |   76 +-
 Mathlib/CategoryTheory/Limits/IsLimit.lean    | 1084 +++++++++++++++++
 .../Limits/Shapes/StrongEpi.lean              |   47 +-
 Mathlib/CategoryTheory/Pi/Basic.lean          |  121 +-
 Mathlib/CategoryTheory/Types.lean             |    3 +-
 Mathlib/CategoryTheory/Yoneda.lean            |   33 +
 Mathlib/Tactic/Core.lean                      |   33 -
 lean-toolchain                                |    2 +-
 test/slice.lean                               |   18 +-
 20 files changed, 2550 insertions(+), 391 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/Category/Ulift.lean
 create mode 100644 Mathlib/CategoryTheory/Equivalence.lean.orig
 create mode 100644 Mathlib/CategoryTheory/Limits/IsLimit.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 8edf9b49cc0f6..6582e428f81a5 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -223,10 +223,6 @@ import Mathlib.Algebra.Tropical.Basic
 import Mathlib.Algebra.Tropical.BigOperators
 import Mathlib.Algebra.Tropical.Lattice
 import Mathlib.CategoryTheory.Adjunction.Basic
-import Mathlib.CategoryTheory.Adjunction.FullyFaithful
-import Mathlib.CategoryTheory.Adjunction.Mates
-import Mathlib.CategoryTheory.Adjunction.Reflective
-import Mathlib.CategoryTheory.Adjunction.Whiskering
 import Mathlib.CategoryTheory.Arrow
 import Mathlib.CategoryTheory.Balanced
 import Mathlib.CategoryTheory.Bicategory.Basic
@@ -238,16 +234,9 @@ import Mathlib.CategoryTheory.Category.GaloisConnection
 import Mathlib.CategoryTheory.Category.KleisliCat
 import Mathlib.CategoryTheory.Category.Preorder
 import Mathlib.CategoryTheory.Category.RelCat
-import Mathlib.CategoryTheory.Category.ULift
-import Mathlib.CategoryTheory.CommSq
+import Mathlib.CategoryTheory.Category.Ulift
 import Mathlib.CategoryTheory.Comma
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
-import Mathlib.CategoryTheory.Conj
-import Mathlib.CategoryTheory.Core
-import Mathlib.CategoryTheory.DiscreteCategory
-import Mathlib.CategoryTheory.Endomorphism
-import Mathlib.CategoryTheory.EpiMono
-import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Equivalence
 import Mathlib.CategoryTheory.EssentialImage
 import Mathlib.CategoryTheory.EssentiallySmall
@@ -265,24 +254,15 @@ import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.InvIsos
 import Mathlib.CategoryTheory.Functor.ReflectsIso
 import Mathlib.CategoryTheory.Groupoid
-import Mathlib.CategoryTheory.Groupoid.Basic
 import Mathlib.CategoryTheory.Iso
-import Mathlib.CategoryTheory.IsomorphismClasses
 import Mathlib.CategoryTheory.LiftingProperties.Adjunction
 import Mathlib.CategoryTheory.LiftingProperties.Basic
 import Mathlib.CategoryTheory.Limits.Cones
 import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
-import Mathlib.CategoryTheory.Monoidal.Category
-import Mathlib.CategoryTheory.Monoidal.Functor
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Opposites
-import Mathlib.CategoryTheory.PEmpty
-import Mathlib.CategoryTheory.PUnit
 import Mathlib.CategoryTheory.Pi.Basic
-import Mathlib.CategoryTheory.Products.Associator
-import Mathlib.CategoryTheory.Products.Basic
-import Mathlib.CategoryTheory.Products.Bifunctor
 import Mathlib.CategoryTheory.Sigma.Basic
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.Sums.Basic
diff --git a/Mathlib/CategoryTheory/Adjunction/Basic.lean b/Mathlib/CategoryTheory/Adjunction/Basic.lean
index 610789b9be365..a5b65f05aaa50 100644
--- a/Mathlib/CategoryTheory/Adjunction/Basic.lean
+++ b/Mathlib/CategoryTheory/Adjunction/Basic.lean
@@ -177,14 +177,14 @@ theorem homEquiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
 #align category_theory.adjunction.hom_equiv_naturality_right_symm CategoryTheory.Adjunction.homEquiv_naturality_right_symm
 
 @[simp]
-theorem left_triangle : whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = 𝟙 _ := by
+theorem left_triangle : whiskerRight adj.unit F ≫ whiskerLeft F adj.counit = NatTrans.id _ := by
   ext; dsimp
   erw [← adj.homEquiv_counit, Equiv.symm_apply_eq, adj.homEquiv_unit]
   simp
 #align category_theory.adjunction.left_triangle CategoryTheory.Adjunction.left_triangle
 
 @[simp]
-theorem right_triangle : whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = 𝟙 _ := by
+theorem right_triangle : whiskerLeft G adj.unit ≫ whiskerRight adj.counit G = NatTrans.id _ := by
   ext; dsimp
   erw [← adj.homEquiv_unit, ← Equiv.eq_symm_apply, adj.homEquiv_counit]
   simp
@@ -387,10 +387,10 @@ def mkOfUnitCounit (adj : CoreUnitCounit F G) : F ⊣ G :=
           exact t } }
 #align category_theory.adjunction.mk_of_unit_counit CategoryTheory.Adjunction.mkOfUnitCounit
 
-/- Porting note: simpNF linter claims these are solved by simp but that
+/- Porting note: simpNF linter claims these are solved by simp but that 
 is not true -/
-attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_symm_apply
-attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_apply
+attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_symm_apply 
+attribute [nolint simpNF] CategoryTheory.Adjunction.mkOfUnitCounit_homEquiv_apply 
 
 /-- The adjunction between the identity functor on a category and itself. -/
 def id : 𝟭 C ⊣ 𝟭 C where
diff --git a/Mathlib/CategoryTheory/Category/Ulift.lean b/Mathlib/CategoryTheory/Category/Ulift.lean
new file mode 100644
index 0000000000000..94b95ea489771
--- /dev/null
+++ b/Mathlib/CategoryTheory/Category/Ulift.lean
@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2021 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Adam Topaz
+
+! This file was ported from Lean 3 source module category_theory.category.ulift
+! leanprover-community/mathlib commit 32253a1a1071173b33dc7d6a218cf722c6feb514
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Category.Basic
+import Mathlib.CategoryTheory.Equivalence
+import Mathlib.CategoryTheory.EqToHom
+
+/-!
+# Basic API for ulift
+
+This file contains a very basic API for working with the categorical
+instance on `ulift C` where `C` is a type with a category instance.
+
+1. `category_theory.ulift.up` is the functorial version of the usual `ulift.up`.
+2. `category_theory.ulift.down` is the functorial version of the usual `ulift.down`.
+3. `category_theory.ulift.equivalence` is the categorical equivalence between
+  `C` and `ulift C`.
+
+# ulift_hom
+
+Given a type `C : Type u`, `ulift_hom.{w} C` is just an alias for `C`.
+If we have `category.{v} C`, then `ulift_hom.{w} C` is endowed with a category instance
+whose morphisms are obtained by applying `ulift.{w}` to the morphisms from `C`.
+
+This is a category equivalent to `C`. The forward direction of the equivalence is `ulift_hom.up`,
+the backward direction is `ulift_hom.donw` and the equivalence is `ulift_hom.equiv`.
+
+# as_small
+
+This file also contains a construction which takes a type `C : Type u` with a
+category instance `category.{v} C` and makes a small category
+`as_small.{w} C : Type (max w v u)` equivalent to `C`.
+
+The forward direction of the equivalence, `C ⥤ as_small C`, is denoted `as_small.up`
+and the backward direction is `as_small.down`. The equivalence itself is `as_small.equiv`.
+-/
+
+
+universe w₁ v₁ v₂ u₁ u₂
+
+namespace CategoryTheory
+
+variable {C : Type u₁} [Category.{v₁} C]
+
+/-- The functorial version of `ulift.up`. -/
+@[simps]
+def Ulift.upFunctor : C ⥤ ULift.{u₂} C where
+  obj := ULift.up
+  map X Y f := f
+#align category_theory.ulift.up_functor CategoryTheory.Ulift.upFunctor
+
+/-- The functorial version of `ulift.down`. -/
+@[simps]
+def Ulift.downFunctor : ULift.{u₂} C ⥤ C
+    where
+  obj := ULift.down
+  map X Y f := f
+#align category_theory.ulift.down_functor CategoryTheory.Ulift.downFunctor
+
+/-- The categorical equivalence between `C` and `ulift C`. -/
+@[simps]
+def Ulift.equivalence : C ≌ ULift.{u₂} C
+    where
+  Functor := Ulift.upFunctor
+  inverse := Ulift.downFunctor
+  unitIso :=
+    { Hom := 𝟙 _
+      inv := 𝟙 _ }
+  counitIso :=
+    { Hom :=
+        { app := fun X => 𝟙 _
+          naturality' := fun X Y f => by
+            change f ≫ 𝟙 _ = 𝟙 _ ≫ f
+            simp }
+      inv :=
+        { app := fun X => 𝟙 _
+          naturality' := fun X Y f => by
+            change f ≫ 𝟙 _ = 𝟙 _ ≫ f
+            simp }
+      hom_inv_id' := by
+        ext
+        change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
+        simp
+      inv_hom_id' := by
+        ext
+        change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
+        simp }
+  functor_unitIso_comp' X := by
+    change 𝟙 X ≫ 𝟙 X = 𝟙 X
+    simp
+#align category_theory.ulift.equivalence CategoryTheory.Ulift.equivalence
+
+section UliftHom
+
+/-- `ulift_hom.{w} C` is an alias for `C`, which is endowed with a category instance
+  whose morphisms are obtained by applying `ulift.{w}` to the morphisms from `C`.
+-/
+def UliftHom.{w, u} (C : Type u) :=
+  C
+#align category_theory.ulift_hom CategoryTheory.UliftHom
+
+instance {C} [Inhabited C] : Inhabited (UliftHom C) :=
+  ⟨(Inhabited.default C : C)⟩
+
+/-- The obvious function `ulift_hom C → C`. -/
+def UliftHom.objDown {C} (A : UliftHom C) : C :=
+  A
+#align category_theory.ulift_hom.obj_down CategoryTheory.UliftHom.objDown
+
+/-- The obvious function `C → ulift_hom C`. -/
+def UliftHom.objUp {C} (A : C) : UliftHom C :=
+  A
+#align category_theory.ulift_hom.obj_up CategoryTheory.UliftHom.objUp
+
+@[simp]
+theorem objDown_objUp {C} (A : C) : (UliftHom.objUp A).objDown = A :=
+  rfl
+#align category_theory.obj_down_obj_up CategoryTheory.objDown_objUp
+
+@[simp]
+theorem objUp_objDown {C} (A : UliftHom C) : UliftHom.objUp A.objDown = A :=
+  rfl
+#align category_theory.obj_up_obj_down CategoryTheory.objUp_objDown
+
+instance : Category.{max v₂ v₁} (UliftHom.{v₂} C)
+    where
+  Hom A B := ULift.{v₂} <| A.objDown ⟶ B.objDown
+  id A := ⟨𝟙 _⟩
+  comp A B C f g := ⟨f.down ≫ g.down⟩
+
+/-- One half of the quivalence between `C` and `ulift_hom C`. -/
+@[simps]
+def UliftHom.up : C ⥤ UliftHom C where
+  obj := UliftHom.objUp
+  map X Y f := ⟨f⟩
+#align category_theory.ulift_hom.up CategoryTheory.UliftHom.up
+
+/-- One half of the quivalence between `C` and `ulift_hom C`. -/
+@[simps]
+def UliftHom.down : UliftHom C ⥤ C where
+  obj := UliftHom.objDown
+  map X Y f := f.down
+#align category_theory.ulift_hom.down CategoryTheory.UliftHom.down
+
+/-- The equivalence between `C` and `ulift_hom C`. -/
+def UliftHom.equiv : C ≌ UliftHom C
+    where
+  Functor := UliftHom.up
+  inverse := UliftHom.down
+  unitIso := NatIso.ofComponents (fun A => eqToIso rfl) (by tidy)
+  counitIso := NatIso.ofComponents (fun A => eqToIso rfl) (by tidy)
+#align category_theory.ulift_hom.equiv CategoryTheory.UliftHom.equiv
+
+end UliftHom
+
+/-- `as_small C` is a small category equivalent to `C`.
+  More specifically, if `C : Type u` is endowed with `category.{v} C`, then
+  `as_small.{w} C : Type (max w v u)` is endowed with an instance of a small category.
+
+  The objects and morphisms of `as_small C` are defined by applying `ulift` to the
+  objects and morphisms of `C`.
+
+  Note: We require a category instance for this definition in order to have direct
+  access to the universe level `v`.
+-/
+@[nolint unused_arguments]
+def AsSmall.{w, v, u} (C : Type u) [Category.{v} C] :=
+  ULift.{max w v} C
+#align category_theory.as_small CategoryTheory.AsSmall
+
+instance : SmallCategory (AsSmall.{w₁} C)
+    where
+  Hom X Y := ULift.{max w₁ u₁} <| X.down ⟶ Y.down
+  id X := ⟨𝟙 _⟩
+  comp X Y Z f g := ⟨f.down ≫ g.down⟩
+
+/-- One half of the equivalence between `C` and `as_small C`. -/
+@[simps]
+def AsSmall.up : C ⥤ AsSmall C where
+  obj X := ⟨X⟩
+  map X Y f := ⟨f⟩
+#align category_theory.as_small.up CategoryTheory.AsSmall.up
+
+/-- One half of the equivalence between `C` and `as_small C`. -/
+@[simps]
+def AsSmall.down : AsSmall C ⥤ C where
+  obj X := X.down
+  map X Y f := f.down
+#align category_theory.as_small.down CategoryTheory.AsSmall.down
+
+/-- The equivalence between `C` and `as_small C`. -/
+@[simps]
+def AsSmall.equiv : C ≌ AsSmall C where
+  Functor := AsSmall.up
+  inverse := AsSmall.down
+  unitIso := NatIso.ofComponents (fun X => eqToIso rfl) (by tidy)
+  counitIso :=
+    NatIso.ofComponents
+      (fun X =>
+        eqToIso <| by
+          ext
+          rfl)
+      (by tidy)
+#align category_theory.as_small.equiv CategoryTheory.AsSmall.equiv
+
+instance [Inhabited C] : Inhabited (AsSmall C) :=
+  ⟨⟨Inhabited.default _⟩⟩
+
+/-- The equivalence between `C` and `ulift_hom (ulift C)`. -/
+def UliftHomUliftCategory.equiv.{v', u', v, u} (C : Type u) [Category.{v} C] :
+    C ≌ UliftHom.{v'} (ULift.{u'} C) :=
+  Ulift.equivalence.trans UliftHom.equiv
+#align category_theory.ulift_hom_ulift_category.equiv CategoryTheory.UliftHomUliftCategory.equiv
+
+end CategoryTheory
+
diff --git a/Mathlib/CategoryTheory/CommSq.lean b/Mathlib/CategoryTheory/CommSq.lean
index 9a7f103ff036c..12ffba8bc2641 100644
--- a/Mathlib/CategoryTheory/CommSq.lean
+++ b/Mathlib/CategoryTheory/CommSq.lean
@@ -121,7 +121,7 @@ structure LiftStruct (sq : CommSq f i p g) where
 
 namespace LiftStruct
 
-/-- A `LiftStruct` for a commutative square gives a `LiftStruct` for the
+/-- A `lift_struct` for a commutative square gives a `lift_struct` for the
 corresponding square in the opposite category. -/
 @[simps]
 def op {sq : CommSq f i p g} (l : LiftStruct sq) : LiftStruct sq.op
@@ -131,8 +131,8 @@ def op {sq : CommSq f i p g} (l : LiftStruct sq) : LiftStruct sq.op
   fac_right := by rw [← op_comp, l.fac_left]
 #align category_theory.comm_sq.lift_struct.op CategoryTheory.CommSq.LiftStruct.op
 
-/-- A `LiftStruct` for a commutative square in the opposite category
-gives a `LiftStruct` for the corresponding square in the original category. -/
+/-- A `lift_struct` for a commutative square in the opposite category
+gives a `lift_struct` for the corresponding square in the original category. -/
 @[simps]
 def unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y} {sq : CommSq f i p g}
     (l : LiftStruct sq) : LiftStruct sq.unop
@@ -142,7 +142,7 @@ def unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B 
   fac_right := by rw [← unop_comp, l.fac_left]
 #align category_theory.comm_sq.lift_struct.unop CategoryTheory.CommSq.LiftStruct.unop
 
-/-- Equivalences of `LiftStruct` for a square and the corresponding square
+/-- Equivalences of `lift_struct` for a square and the corresponding square
 in the opposite category. -/
 @[simps]
 def opEquiv (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.op
@@ -153,7 +153,7 @@ def opEquiv (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.op
   right_inv := by aesop_cat
 #align category_theory.comm_sq.lift_struct.op_equiv CategoryTheory.CommSq.LiftStruct.opEquiv
 
-/-- Equivalences of `LiftStruct` for a square in the oppositive category and
+/-- Equivalences of `lift_struct` for a square in the oppositive category and
 the corresponding square in the original category. -/
 def unopEquiv {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
     (sq : CommSq f i p g) : LiftStruct sq ≃ LiftStruct sq.unop
@@ -171,7 +171,8 @@ instance subsingleton_liftStruct_of_epi (sq : CommSq f i p g) [Epi i] :
   ⟨fun l₁ l₂ => by
     ext
     rw [← cancel_epi i]
-    simp only [LiftStruct.fac_left]⟩
+    simp only [LiftStruct.fac_left]
+    ⟩
 #align category_theory.comm_sq.subsingleton_lift_struct_of_epi CategoryTheory.CommSq.subsingleton_liftStruct_of_epi
 
 instance subsingleton_liftStruct_of_mono (sq : CommSq f i p g) [Mono p] :
@@ -185,9 +186,9 @@ instance subsingleton_liftStruct_of_mono (sq : CommSq f i p g) [Mono p] :
 variable (sq : CommSq f i p g)
 
 
-/-- The assertion that a square has a `LiftStruct`. -/
+/-- The assertion that a square has a `lift_struct`. -/
 class HasLift : Prop where
-  /-- Square has a `LiftStruct`. -/
+  /-- Square has a `lift_struct`. -/
   exists_lift : Nonempty sq.LiftStruct
 #align category_theory.comm_sq.has_lift CategoryTheory.CommSq.HasLift
 
@@ -219,7 +220,7 @@ theorem iff_unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {
 
 end HasLift
 
-/-- A choice of a diagonal morphism that is part of a `LiftStruct` when
+/-- A choice of a diagonal morphism that is part of a `lift_struct` when
 the square has a lift. -/
 noncomputable def lift [hsq : HasLift sq] : B ⟶ X :=
   hsq.exists_lift.some.l
diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
index 9518b44d11cdb..cac60eb13ddee 100644
--- a/Mathlib/CategoryTheory/DiscreteCategory.lean
+++ b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -44,7 +44,7 @@ universe v₁ v₂ v₃ u₁ u₁' u₂ u₃
 
 -- This is intentionally a structure rather than a type synonym
 -- to enforce using `DiscreteEquiv` (or `Discrete.mk` and `Discrete.as`) to move between
--- `Discrete α` and `α`. Otherwise there is too much API leakage.
+-- `discrete α` and `α`. Otherwise there is too much API leakage.
 /-- A wrapper for promoting any type to a category,
 with the only morphisms being equalities.
 -/
@@ -64,7 +64,8 @@ theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X
 
 /-- `Discrete α` is equivalent to the original type `α`.-/
 @[simps]
-def discreteEquiv {α : Type u₁} : Discrete α ≃ α where
+def discreteEquiv {α : Type u₁} : Discrete α ≃ α
+    where
   toFun := Discrete.as
   invFun := Discrete.mk
   left_inv := by aesop_cat
@@ -81,7 +82,8 @@ somewhat annoyingly we have to define `X ⟶ Y` as `ULift (PLift (X = Y))`.
 
 See <https://stacks.math.columbia.edu/tag/001A>
 -/
-instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α) where
+instance discreteCategory (α : Type u₁) : SmallCategory (Discrete α)
+    where
   Hom X Y := ULift (PLift (X.as = Y.as))
   id X := ULift.up (PLift.up rfl)
   comp {X Y Z} g f := by
@@ -105,15 +107,22 @@ instance [Subsingleton α] : Subsingleton (Discrete α) :=
     ext
     apply Subsingleton.elim⟩
 
-/-
-Porting note: It seems that `aesop` currently has no way to add lemmas locally.
+/- ./././Mathport/Syntax/Translate/Expr.lean:334:4: warning: unsupported (TODO): `[tacs] -/
+/-- A simple tactic to run `cases` on any `discrete α` hypotheses. -/
+--unsafe def _root_.tactic.discrete_cases : tactic Unit :=
+--  sorry
+--#align tactic.discrete_cases tactic.discrete_cases
 
-attribute [local tidy] tactic.discrete_cases
-`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), PLift _]]
--/
 
+--run_cmd
+--  add_interactive [`` tactic.discrete_cases]
+
+--attribute [local tidy] tactic.discrete_cases
+--`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), plift _]]
+
+--macro (name := discrete_cases) "discrete_cases" : tactic =>
+--  `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
 /- Porting note: rewrote `discrete_cases` tactic -/
-/-- A simple tactic to run `cases` on any `discrete α` hypotheses. -/
 macro "discrete_cases": tactic =>
   `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
 
@@ -143,7 +152,7 @@ protected abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y :=
       exact h)
 #align category_theory.discrete.eq_to_iso CategoryTheory.Discrete.eqToIso
 
-/-- A variant of `eqToHom` that lifts terms to the discrete category. -/
+/-- A variant of `eq_to_hom` that lifts terms to the discrete category. -/
 abbrev eqToHom' {a b : α} (h : a = b) : Discrete.mk a ⟶ Discrete.mk b :=
   Discrete.eqToHom h
 #align category_theory.discrete.eq_to_hom' CategoryTheory.Discrete.eqToHom'
@@ -163,8 +172,12 @@ variable {C : Type u₂} [Category.{v₂} C]
 instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f :=
   ⟨⟨Discrete.eqToHom (eq_of_hom f).symm, by aesop_cat⟩⟩
 
-/-- Any function `I → C` gives a functor `Discrete I ⥤ C`.-/
-def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C where
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
+/-- Any function `I → C` gives a functor `Discrete I ⥤ C`.
+-/
+def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C
+    where
   obj := F ∘ Discrete.as
   map {X Y} f := by
     dsimp
@@ -195,6 +208,8 @@ def functorComp {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) :
   NatIso.ofComponents (fun X => Iso.refl _) (by aesop_cat)
 #align category_theory.discrete.functor_comp CategoryTheory.Discrete.functorComp
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
 /-- For functors out of a discrete category,
 a natural transformation is just a collection of maps,
 as the naturality squares are trivial.
@@ -203,20 +218,24 @@ as the naturality squares are trivial.
 def natTrans {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ⟶ G.obj i) : F ⟶ G
     where
   app := f
-  naturality := fun {X Y} ⟨⟨g⟩⟩ => by
+  naturality {X Y} g := by
+    rcases g with ⟨⟨g⟩⟩
     discrete_cases
     rcases g
     change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
     simp
 #align category_theory.discrete.nat_trans CategoryTheory.Discrete.natTrans
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
 /-- For functors out of a discrete category,
 a natural isomorphism is just a collection of isomorphisms,
 as the naturality squares are trivial.
 -/
 @[simps!]
 def natIso {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i) : F ≅ G :=
-  NatIso.ofComponents f fun ⟨⟨g⟩⟩ => by
+  NatIso.ofComponents f fun g => by
+    rcases g with ⟨⟨g⟩⟩
     discrete_cases
     rcases g
     change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
@@ -228,6 +247,8 @@ theorem natIso_app {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discret
     (i : Discrete I) : (Discrete.natIso f).app i = f i := by aesop_cat
 #align category_theory.discrete.nat_iso_app CategoryTheory.Discrete.natIso_app
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
 /-- Every functor `F` from a discrete category is naturally isomorphic (actually, equal) to
   `discrete.functor (F.obj)`. -/
 @[simp]
@@ -242,11 +263,16 @@ def compNatIsoDiscrete {I : Type u₁} {D : Type u₃} [Category.{v₃} D] (F :
   natIso fun _ => Iso.refl _
 #align category_theory.discrete.comp_nat_iso_discrete CategoryTheory.Discrete.compNatIsoDiscrete
 
-/-- We can promote a type-level `Equiv` to
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
+/-- We can promote a type-level `equiv` to
 an equivalence between the corresponding `discrete` categories.
 -/
 @[simps]
-def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J where
+def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J
+    where
   functor := Discrete.functor (Discrete.mk ∘ (e : I → J))
   inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I))
   unitIso :=
@@ -263,9 +289,10 @@ def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ D
           simp)
 #align category_theory.discrete.equivalence CategoryTheory.Discrete.equivalence
 
-/-- We can convert an equivalence of `discrete` categories to a type-level `Equiv`. -/
+/-- We can convert an equivalence of `discrete` categories to a type-level `equiv`. -/
 @[simps]
-def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β where
+def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β
+    where
   toFun := Discrete.as ∘ h.functor.obj ∘ Discrete.mk
   invFun := Discrete.as ∘ h.inverse.obj ∘ Discrete.mk
   left_inv a := by simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2
@@ -280,23 +307,27 @@ variable {J : Type v₁}
 
 open Opposite
 
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:72:18: unsupported
+\  non-interactive tactic tactic.op_induction' -/
+/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported
+\  tactic `discrete_cases #[] -/
 /-- A discrete category is equivalent to its opposite category. -/
 @[simps! functor_obj_as inverse_obj]
 protected def opposite (α : Type u₁) : (Discrete α)ᵒᵖ ≌ Discrete α :=
   let F : Discrete α ⥤ (Discrete α)ᵒᵖ := Discrete.functor fun x => op (Discrete.mk x)
   Equivalence.mk F.leftOp F
-  (NatIso.ofComponents (fun ⟨X⟩ => Iso.refl _) <| fun {X Y} ⟨⟨f⟩⟩ => by
+  (NatIso.ofComponents (fun ⟨X⟩ => Iso.refl _)
+    <| fun {X Y} f => by
       induction X using Opposite.rec
       induction Y using Opposite.rec
+      rcases f with ⟨⟨f⟩⟩
       discrete_cases
       rcases f
       aesop_cat)
   (Discrete.natIso <| fun ⟨X⟩ => Iso.refl _)
-
 /-
-  Porting note:
-  The following is what was generated by mathport:
-
   refine'
     Equivalence.mk (F.leftOp) F _
       (Discrete.natIso fun X =>
@@ -330,3 +361,4 @@ theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F
 end Discrete
 
 end CategoryTheory
+
diff --git a/Mathlib/CategoryTheory/Equivalence.lean b/Mathlib/CategoryTheory/Equivalence.lean
index e647b92d214c8..3db834162b42d 100644
--- a/Mathlib/CategoryTheory/Equivalence.lean
+++ b/Mathlib/CategoryTheory/Equivalence.lean
@@ -48,9 +48,9 @@ if it is full, faithful and essentially surjective.
 ## Main results
 
 * `Equivalence.mk`: upgrade an equivalence to a (half-)adjoint equivalence
-* `IsEquivalence.equivOfIso`: when `F` and `G` are isomorphic functors, `F` is an equivalence
+* `IsEquivalence.equiv_of_iso`: when `F` and `G` are isomorphic functors, `F` is an equivalence
 iff `G` is.
-* `Equivalence.ofFullyFaithfullyEssSurj`: a fully faithful essentially surjective functor is an
+* `Equivalence.of_fully_faithfully_essSurj`: a fully faithful essentially surjective functor is an
   equivalence.
 
 ## Notations
@@ -89,14 +89,14 @@ structure Equivalence (C : Type u₁) (D : Type u₂) [Category.{v₁} C] [Categ
   /-- The composition `inverse ⋙ functor` is also isomorphic to the identity -/
   counitIso : inverse ⋙ functor ≅ 𝟭 D
   /-- The natural isomorphism compose to the identity -/
-  functor_unitIso_comp :
-    ∀ X : C, functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) =
+  functor_unit_iso_comp : 
+    ∀ X : C, functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 
       𝟙 (functor.obj X) := by aesop_cat
 #align category_theory.equivalence CategoryTheory.Equivalence
 
 /-- We infix the usual notation for an equivalence -/
 infixr:10 " ≌ " => Equivalence
-
+ 
 variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
 
 namespace Equivalence
@@ -124,33 +124,37 @@ abbrev counitInv (e : C ≌ D) : 𝟭 D ⟶ e.inverse ⋙ e.functor :=
 /- While these abbreviations are convenient, they also cause some trouble,
 preventing structure projections from unfolding. -/
 @[simp]
-theorem Equivalence_mk'_unit (functor inverse unit_iso counit_iso f) :
+theorem equivalence_mk'_unit (functor inverse unit_iso counit_iso f) :
     (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unit = unit_iso.hom :=
   rfl
-#align category_theory.equivalence.equivalence_mk'_unit CategoryTheory.Equivalence.Equivalence_mk'_unit
+#align
+  category_theory.equivalence.equivalence_mk'_unit CategoryTheory.Equivalence.equivalence_mk'_unit
 
 @[simp]
-theorem Equivalence_mk'_counit (functor inverse unit_iso counit_iso f) :
+theorem equivalence_mk'_counit (functor inverse unit_iso counit_iso f) :
     (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counit = counit_iso.hom :=
   rfl
-#align category_theory.equivalence.equivalence_mk'_counit CategoryTheory.Equivalence.Equivalence_mk'_counit
+#align category_theory.equivalence.equivalence_mk'_counit 
+  CategoryTheory.Equivalence.equivalence_mk'_counit
 
 @[simp]
-theorem Equivalence_mk'_unitInv (functor inverse unit_iso counit_iso f) :
+theorem equivalence_mk'_unitInv (functor inverse unit_iso counit_iso f) :
     (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unitInv = unit_iso.inv :=
   rfl
-#align category_theory.equivalence.equivalence_mk'_unit_inv CategoryTheory.Equivalence.Equivalence_mk'_unitInv
+#align category_theory.equivalence.equivalence_mk'_unit_inv 
+  CategoryTheory.Equivalence.equivalence_mk'_unitInv
 
 @[simp]
-theorem Equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) :
+theorem equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) :
     (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counitInv = counit_iso.inv :=
   rfl
-#align category_theory.equivalence.equivalence_mk'_counit_inv CategoryTheory.Equivalence.Equivalence_mk'_counitInv
+#align category_theory.equivalence.equivalence_mk'_counit_inv 
+  CategoryTheory.Equivalence.equivalence_mk'_counitInv
 
 @[simp]
 theorem functor_unit_comp (e : C ≌ D) (X : C) :
     e.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X) :=
-  e.functor_unitIso_comp X
+  e.functor_unit_iso_comp X
 #align category_theory.equivalence.functor_unit_comp CategoryTheory.Equivalence.functor_unit_comp
 
 @[simp]
@@ -160,22 +164,25 @@ theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
   erw [Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
       (Iso.refl _)]
   exact e.functor_unit_comp X
-#align category_theory.equivalence.counit_inv_functor_comp CategoryTheory.Equivalence.counitInv_functor_comp
+#align category_theory.equivalence.counit_inv_functor_comp 
+  CategoryTheory.Equivalence.counitInv_functor_comp
 
-theorem counitInv_app_functor (e : C ≌ D) (X : C) :
+theorem counit_inv_app_functor (e : C ≌ D) (X : C) :
     e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X) :=
   by
   symm
   erw [← Iso.comp_hom_eq_id (e.counitIso.app _), functor_unit_comp]
   rfl
-#align category_theory.equivalence.counit_inv_app_functor CategoryTheory.Equivalence.counitInv_app_functor
+#align category_theory.equivalence.counit_inv_app_functor 
+  CategoryTheory.Equivalence.counit_inv_app_functor
 
 theorem counit_app_functor (e : C ≌ D) (X : C) :
     e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X) :=
   by
   erw [← Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)), functor_unit_comp]
   rfl
-#align category_theory.equivalence.counit_app_functor CategoryTheory.Equivalence.counit_app_functor
+#align 
+  category_theory.equivalence.counit_app_functor CategoryTheory.Equivalence.counit_app_functor
 
 /-- The other triangle equality. The proof follows the following proof in Globular:
   http://globular.science/1905.001 -/
@@ -206,13 +213,14 @@ theorem unit_inverse_comp (e : C ≌ D) (Y : D) :
 #align category_theory.equivalence.unit_inverse_comp CategoryTheory.Equivalence.unit_inverse_comp
 
 @[simp]
-theorem inverse_counitInv_comp (e : C ≌ D) (Y : D) :
+theorem inverse_counit_inv_comp (e : C ≌ D) (Y : D) :
     e.inverse.map (e.counitInv.app Y) ≫ e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) :=
   by
   erw [Iso.inv_eq_inv (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y))
       (Iso.refl _)]
   exact e.unit_inverse_comp Y
-#align category_theory.equivalence.inverse_counit_inv_comp CategoryTheory.Equivalence.inverse_counitInv_comp
+#align category_theory.equivalence.inverse_counit_inv_comp 
+  CategoryTheory.Equivalence.inverse_counit_inv_comp
 
 theorem unit_app_inverse (e : C ≌ D) (Y : D) :
     e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y) := by
@@ -220,12 +228,13 @@ theorem unit_app_inverse (e : C ≌ D) (Y : D) :
   dsimp
 #align category_theory.equivalence.unit_app_inverse CategoryTheory.Equivalence.unit_app_inverse
 
-theorem unitInv_app_inverse (e : C ≌ D) (Y : D) :
+theorem unit_inv_app_inverse (e : C ≌ D) (Y : D) :
     e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y) := by
   symm
   erw [← Iso.hom_comp_eq_id (e.unitIso.app _), unit_inverse_comp]
   rfl
-#align category_theory.equivalence.unit_inv_app_inverse CategoryTheory.Equivalence.unitInv_app_inverse
+#align
+  category_theory.equivalence.unit_inv_app_inverse CategoryTheory.Equivalence.unit_inv_app_inverse
 
 @[simp]
 theorem fun_inv_map (e : C ≌ D) (X Y : D) (f : X ⟶ Y) :
@@ -245,9 +254,9 @@ section
 variable {F : C ⥤ D} {G : D ⥤ C} (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D)
 
 /-- If `η : 𝟭 C ≅ F ⋙ G` is part of a (not necessarily half-adjoint) equivalence, we can upgrade it
-to a refined natural isomorphism `adjointifyη η : 𝟭 C ≅ F ⋙ G` which exhibits the properties
-required for a half-adjoint equivalence. See `Equivalence.mk`. -/
-def adjointifyη : 𝟭 C ≅ F ⋙ G := by
+to a refined natural isomorphism `adjointify_η η : 𝟭 C ≅ F ⋙ G` which exhibits the properties
+required for a half-adjoint equivalence. See `equivalence.mk`. -/
+def adjointifyη : 𝟭 C ≅ F ⋙ G := by 
   calc
     𝟭 C ≅ F ⋙ G := η
     _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm
@@ -256,6 +265,7 @@ def adjointifyη : 𝟭 C ≅ F ⋙ G := by
     _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm
     _ ≅ 𝟭 C ⋙ F ⋙ G := isoWhiskerRight η.symm (F ⋙ G)
     _ ≅ F ⋙ G := leftUnitor (F ⋙ G)
+    
 #align category_theory.equivalence.adjointify_η CategoryTheory.Equivalence.adjointifyη
 
 theorem adjointify_η_ε (X : C) :
@@ -281,7 +291,7 @@ protected def mk (F : C ⥤ D) (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G 
 
 /-- Equivalence of categories is reflexive. -/
 @[refl, simps]
-def refl : C ≌ C :=
+def refl : C ≌ C := 
   ⟨𝟭 C, 𝟭 C, Iso.refl _, Iso.refl _, fun _ => Category.id_comp _⟩
 #align category_theory.equivalence.refl CategoryTheory.Equivalence.refl
 
@@ -291,7 +301,7 @@ instance : Inhabited (C ≌ C) :=
 /-- Equivalence of categories is symmetric. -/
 @[symm, simps]
 def symm (e : C ≌ D) : D ≌ C :=
-  ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm, e.inverse_counitInv_comp⟩
+  ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm, e.inverse_counit_inv_comp⟩
 #align category_theory.equivalence.symm CategoryTheory.Equivalence.symm
 
 variable {E : Type u₃} [Category.{v₃} E]
@@ -308,12 +318,12 @@ def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E
   counitIso := by
     refine' Iso.trans _ f.counitIso
     exact isoWhiskerLeft f.inverse (isoWhiskerRight e.counitIso f.functor)
-  -- We wouldn't have needed to give this proof if we'd used `Equivalence.mk`,
+  -- We wouldn't have needed to give this proof if we'd used `equivalence.mk`,
   -- but we choose to avoid using that here, for the sake of good structure projection `simp`
   -- lemmas.
-  functor_unitIso_comp X := by
+  functor_unit_iso_comp X := by
     dsimp
-    rw [← f.functor.map_comp_assoc, e.functor.map_comp, ← counitInv_app_functor, fun_inv_map,
+    rw [← f.functor.map_comp_assoc, e.functor.map_comp, ← counit_inv_app_functor, fun_inv_map,
       Iso.inv_hom_id_app_assoc, assoc, Iso.inv_hom_id_app, counit_app_functor, ← Functor.map_comp]
     erw [comp_id, Iso.hom_inv_id_app, Functor.map_id]
 #align category_theory.equivalence.trans CategoryTheory.Equivalence.trans
@@ -325,20 +335,22 @@ def funInvIdAssoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F 
 #align category_theory.equivalence.fun_inv_id_assoc CategoryTheory.Equivalence.funInvIdAssoc
 
 @[simp]
-theorem funInvIdAssoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
+theorem fun_inv_id_assoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
     (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X) :=
   by
   dsimp [funInvIdAssoc]
   aesop_cat
-#align category_theory.equivalence.fun_inv_id_assoc_hom_app CategoryTheory.Equivalence.funInvIdAssoc_hom_app
+#align category_theory.equivalence.fun_inv_id_assoc_hom_app 
+  CategoryTheory.Equivalence.fun_inv_id_assoc_hom_app
 
 @[simp]
-theorem funInvIdAssoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
+theorem fun_inv_id_assoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
     (funInvIdAssoc e F).inv.app X = F.map (e.unit.app X) :=
   by
   dsimp [funInvIdAssoc]
   aesop_cat
-#align category_theory.equivalence.fun_inv_id_assoc_inv_app CategoryTheory.Equivalence.funInvIdAssoc_inv_app
+#align category_theory.equivalence.fun_inv_id_assoc_inv_app 
+  CategoryTheory.Equivalence.fun_inv_id_assoc_inv_app
 
 /-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
 functor. -/
@@ -347,20 +359,22 @@ def invFunIdAssoc (e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ F 
 #align category_theory.equivalence.inv_fun_id_assoc CategoryTheory.Equivalence.invFunIdAssoc
 
 @[simp]
-theorem invFunIdAssoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
+theorem inv_fun_id_assoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
     (invFunIdAssoc e F).hom.app X = F.map (e.counit.app X) :=
   by
   dsimp [invFunIdAssoc]
   aesop_cat
-#align category_theory.equivalence.inv_fun_id_assoc_hom_app CategoryTheory.Equivalence.invFunIdAssoc_hom_app
+#align category_theory.equivalence.inv_fun_id_assoc_hom_app 
+  CategoryTheory.Equivalence.inv_fun_id_assoc_hom_app
 
 @[simp]
-theorem invFunIdAssoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
+theorem inv_fun_id_assoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
     (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X) :=
   by
   dsimp [invFunIdAssoc]
   aesop_cat
-#align category_theory.equivalence.inv_fun_id_assoc_inv_app CategoryTheory.Equivalence.invFunIdAssoc_inv_app
+#align category_theory.equivalence.inv_fun_id_assoc_inv_app 
+  CategoryTheory.Equivalence.inv_fun_id_assoc_inv_app
 
 /-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`. -/
 @[simps! functor inverse unitIso counitIso]
@@ -386,9 +400,9 @@ section CancellationLemmas
 
 variable (e : C ≌ D)
 
-/- We need special forms of `cancel_natIso_hom_right(_assoc)` and
-`cancel_natIso_inv_right(_assoc)` for units and counits, because neither `simp` or `rw` will apply
-those lemmas in this setting without providing `e.unitIso` (or similar) as an explicit argument.
+/- We need special forms of `cancel_nat_iso_hom_right(_assoc)` and
+`cancel_nat_iso_inv_right(_assoc)` for units and counits, because neither `simp` or `rw` will apply
+those lemmas in this setting without providing `e.unit_iso` (or similar) as an explicit argument.
 We also provide the lemmas for length four compositions, since they're occasionally useful.
 (e.g. in proving that equivalences take monos to monos) -/
 @[simp]
@@ -397,45 +411,52 @@ theorem cancel_unit_right {X Y : C} (f f' : X ⟶ Y) :
 #align category_theory.equivalence.cancel_unit_right CategoryTheory.Equivalence.cancel_unit_right
 
 @[simp]
-theorem cancel_unitInv_right {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) :
+theorem cancel_unit_inv_right {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) :
     f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f' := by simp only [cancel_mono]
-#align category_theory.equivalence.cancel_unit_inv_right CategoryTheory.Equivalence.cancel_unitInv_right
+#align
+  category_theory.equivalence.cancel_unit_inv_right CategoryTheory.Equivalence.cancel_unit_inv_right
 
 @[simp]
 theorem cancel_counit_right {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) :
     f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f' := by simp only [cancel_mono]
-#align category_theory.equivalence.cancel_counit_right CategoryTheory.Equivalence.cancel_counit_right
+#align
+  category_theory.equivalence.cancel_counit_right CategoryTheory.Equivalence.cancel_counit_right
 
 @[simp]
-theorem cancel_counitInv_right {X Y : D} (f f' : X ⟶ Y) :
+theorem cancel_counit_inv_right {X Y : D} (f f' : X ⟶ Y) :
     f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f' := by simp only [cancel_mono]
-#align category_theory.equivalence.cancel_counit_inv_right CategoryTheory.Equivalence.cancel_counitInv_right
+#align category_theory.equivalence.cancel_counit_inv_right 
+  CategoryTheory.Equivalence.cancel_counit_inv_right
 
 @[simp]
 theorem cancel_unit_right_assoc {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) :
     f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g' := by
   simp only [← Category.assoc, cancel_mono]
-#align category_theory.equivalence.cancel_unit_right_assoc CategoryTheory.Equivalence.cancel_unit_right_assoc
+#align category_theory.equivalence.cancel_unit_right_assoc 
+  CategoryTheory.Equivalence.cancel_unit_right_assoc
 
 @[simp]
-theorem cancel_counitInv_right_assoc {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
+theorem cancel_counit_inv_right_assoc {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
     (g' : X' ⟶ Y) : f ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g' := by
   simp only [← Category.assoc, cancel_mono]
-#align category_theory.equivalence.cancel_counit_inv_right_assoc CategoryTheory.Equivalence.cancel_counitInv_right_assoc
+#align category_theory.equivalence.cancel_counit_inv_right_assoc 
+  CategoryTheory.Equivalence.cancel_counit_inv_right_assoc
 
 @[simp]
 theorem cancel_unit_right_assoc' {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
     (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
     f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' := by
   simp only [← Category.assoc, cancel_mono]
-#align category_theory.equivalence.cancel_unit_right_assoc' CategoryTheory.Equivalence.cancel_unit_right_assoc'
+#align category_theory.equivalence.cancel_unit_right_assoc' 
+  CategoryTheory.Equivalence.cancel_unit_right_assoc'
 
 @[simp]
-theorem cancel_counitInv_right_assoc' {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
+theorem cancel_counit_inv_right_assoc' {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
     (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
     f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' :=
   by simp only [← Category.assoc, cancel_mono]
-#align category_theory.equivalence.cancel_counit_inv_right_assoc' CategoryTheory.Equivalence.cancel_counitInv_right_assoc'
+#align category_theory.equivalence.cancel_counit_inv_right_assoc' 
+  CategoryTheory.Equivalence.cancel_counit_inv_right_assoc'
 
 end CancellationLemmas
 
@@ -490,14 +511,14 @@ class IsEquivalence (F : C ⥤ D) where mk' ::
   /-- Composition `inverse ⋙ F` is isomorphic to the identity. =-/
   counitIso : inverse ⋙ F ≅ 𝟭 D
   /-- We natural isomorphisms are inverse -/
-  functor_unitIso_comp :
+  functor_unit_iso_comp :
     ∀ X : C,
       F.map ((unitIso.hom : 𝟭 C ⟶ F ⋙ inverse).app X) ≫ counitIso.hom.app (F.obj X) =
         𝟙 (F.obj X) := by
     aesop_cat
 #align category_theory.is_equivalence CategoryTheory.IsEquivalence
 
-attribute [reassoc (attr := simp)] IsEquivalence.functor_unitIso_comp
+attribute [reassoc (attr := simp)] IsEquivalence.functor_unit_iso_comp
 
 namespace IsEquivalence
 
@@ -507,7 +528,8 @@ instance ofEquivalence (F : C ≌ D) : IsEquivalence F.functor :=
 
 instance ofEquivalenceInverse (F : C ≌ D) : IsEquivalence F.inverse :=
   IsEquivalence.ofEquivalence F.symm
-#align category_theory.is_equivalence.of_equivalence_inverse CategoryTheory.IsEquivalence.ofEquivalenceInverse
+#align category_theory.is_equivalence.of_equivalence_inverse 
+  CategoryTheory.IsEquivalence.ofEquivalenceInverse
 
 open Equivalence
 
@@ -524,7 +546,7 @@ namespace Functor
 /-- Interpret a functor that is an equivalence as an equivalence. -/
 def asEquivalence (F : C ⥤ D) [IsEquivalence F] : C ≌ D :=
   ⟨F, IsEquivalence.inverse F, IsEquivalence.unitIso, IsEquivalence.counitIso,
-    IsEquivalence.functor_unitIso_comp⟩
+    IsEquivalence.functor_unit_iso_comp⟩
 #align category_theory.functor.as_equivalence CategoryTheory.Functor.asEquivalence
 
 instance isEquivalenceRefl : IsEquivalence (𝟭 C) :=
@@ -541,26 +563,26 @@ instance isEquivalenceInv (F : C ⥤ D) [IsEquivalence F] : IsEquivalence F.inv
 #align category_theory.functor.is_equivalence_inv CategoryTheory.Functor.isEquivalenceInv
 
 @[simp]
-theorem asEquivalence_functor (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.functor = F :=
+theorem as_equivalence_functor (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.functor = F :=
   rfl
-#align category_theory.functor.as_equivalence_functor CategoryTheory.Functor.asEquivalence_functor
+#align category_theory.functor.as_equivalence_functor CategoryTheory.Functor.as_equivalence_functor
 
 @[simp]
-theorem asEquivalence_inverse (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.inverse = inv F :=
+theorem as_equivalence_inverse (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.inverse = inv F :=
   rfl
-#align category_theory.functor.as_equivalence_inverse CategoryTheory.Functor.asEquivalence_inverse
+#align category_theory.functor.as_equivalence_inverse CategoryTheory.Functor.as_equivalence_inverse
 
 @[simp]
-theorem asEquivalence_unit {F : C ⥤ D} [IsEquivalence F] :
+theorem as_equivalence_unit {F : C ⥤ D} [IsEquivalence F] :
     F.asEquivalence.unitIso = IsEquivalence.unitIso :=
   rfl
-#align category_theory.functor.as_equivalence_unit CategoryTheory.Functor.asEquivalence_unit
+#align category_theory.functor.as_equivalence_unit CategoryTheory.Functor.as_equivalence_unit
 
 @[simp]
-theorem asEquivalence_counit {F : C ⥤ D} [IsEquivalence F] :
+theorem as_equivalence_counit {F : C ⥤ D} [IsEquivalence F] :
     F.asEquivalence.counitIso = IsEquivalence.counitIso :=
   rfl
-#align category_theory.functor.as_equivalence_counit CategoryTheory.Functor.asEquivalence_counit
+#align category_theory.functor.as_equivalence_counit CategoryTheory.Functor.as_equivalence_counit
 
 @[simp]
 theorem inv_inv (F : C ⥤ D) [IsEquivalence F] : inv (inv F) = F :=
@@ -589,18 +611,20 @@ theorem inverse_inv (E : C ≌ D) : E.inverse.inv = E.functor :=
 #align category_theory.equivalence.inverse_inv CategoryTheory.Equivalence.inverse_inv
 
 @[simp]
-theorem functor_asEquivalence (E : C ≌ D) : E.functor.asEquivalence = E :=
+theorem functor_as_equivalence (E : C ≌ D) : E.functor.asEquivalence = E :=
   by
   cases E
   congr
-#align category_theory.equivalence.functor_as_equivalence CategoryTheory.Equivalence.functor_asEquivalence
+#align category_theory.equivalence.functor_as_equivalence 
+  CategoryTheory.Equivalence.functor_as_equivalence
 
 @[simp]
-theorem inverse_asEquivalence (E : C ≌ D) : E.inverse.asEquivalence = E.symm :=
+theorem inverse_as_equivalence (E : C ≌ D) : E.inverse.asEquivalence = E.symm :=
   by
   cases E
   congr
-#align category_theory.equivalence.inverse_as_equivalence CategoryTheory.Equivalence.inverse_asEquivalence
+#align category_theory.equivalence.inverse_as_equivalence 
+  CategoryTheory.Equivalence.inverse_as_equivalence
 
 end Equivalence
 
@@ -630,7 +654,7 @@ def ofIso {F G : C ⥤ D} (e : F ≅ G) (hF : IsEquivalence F) : IsEquivalence G
   inverse := hF.inverse
   unitIso := hF.unitIso ≪≫ NatIso.hcomp e (Iso.refl hF.inverse)
   counitIso := NatIso.hcomp (Iso.refl hF.inverse) e.symm ≪≫ hF.counitIso
-  functor_unitIso_comp X := by
+  functor_unit_iso_comp X := by
     dsimp [NatIso.hcomp]
     erw [id_comp, F.map_id, comp_id]
     apply (cancel_epi (e.hom.app X)).mp
@@ -638,29 +662,29 @@ def ofIso {F G : C ⥤ D} (e : F ≅ G) (hF : IsEquivalence F) : IsEquivalence G
     slice_lhs 2 3 => rw [← NatTrans.vcomp_app', e.hom_inv_id]
     simp only [NatTrans.id_app, id_comp, comp_id, F.map_comp, assoc]
     erw [hF.counitIso.hom.naturality]
-    slice_lhs 1 2 => rw [functor_unitIso_comp]
+    slice_lhs 1 2 => rw [functor_unit_iso_comp]
     simp only [Functor.id_map, id_comp]
 #align category_theory.is_equivalence.of_iso CategoryTheory.IsEquivalence.ofIso
 
-/-- Compatibility of `ofIso` with the composition of isomorphisms of functors -/
-theorem ofIso_trans {F G H : C ⥤ D} (e : F ≅ G) (e' : G ≅ H) (hF : IsEquivalence F) :
+/-- Compatibility of `of_iso` with the composition of isomorphisms of functors -/
+theorem of_iso_trans {F G H : C ⥤ D} (e : F ≅ G) (e' : G ≅ H) (hF : IsEquivalence F) :
     ofIso e' (ofIso e hF) = ofIso (e ≪≫ e') hF :=
   by
   dsimp [ofIso]
   congr 1 <;> ext X <;> dsimp [NatIso.hcomp]
   · simp only [id_comp, assoc, Functor.map_comp]
   · simp only [Functor.map_id, comp_id, id_comp, assoc]
-#align category_theory.is_equivalence.of_iso_trans CategoryTheory.IsEquivalence.ofIso_trans
+#align category_theory.is_equivalence.of_iso_trans CategoryTheory.IsEquivalence.of_iso_trans
 
-/-- Compatibility of `ofIso` with identity isomorphisms of functors -/
-theorem ofIso_refl (F : C ⥤ D) (hF : IsEquivalence F) : ofIso (Iso.refl F) hF = hF :=
+/-- Compatibility of `of_iso` with identity isomorphisms of functors -/
+theorem of_iso_refl (F : C ⥤ D) (hF : IsEquivalence F) : ofIso (Iso.refl F) hF = hF :=
   by
   rcases hF with ⟨Finv, Funit, Fcounit, Fcomp⟩
   dsimp [ofIso]
   congr 1 <;> ext X <;> dsimp [NatIso.hcomp]
   · simp only [comp_id, map_id]
   · simp only [id_comp, map_id]
-#align category_theory.is_equivalence.of_iso_refl CategoryTheory.IsEquivalence.ofIso_refl
+#align category_theory.is_equivalence.of_iso_refl CategoryTheory.IsEquivalence.of_iso_refl
 
 /-- When `F` and `G` are two isomorphic functors, then `F` is an equivalence iff `G` is. -/
 @[simps]
@@ -668,8 +692,8 @@ def equivOfIso {F G : C ⥤ D} (e : F ≅ G) : IsEquivalence F ≃ IsEquivalence
     where
   toFun := ofIso e
   invFun := ofIso e.symm
-  left_inv hF := by rw [ofIso_trans, Iso.self_symm_id, ofIso_refl]
-  right_inv hF := by rw [ofIso_trans, Iso.symm_self_id, ofIso_refl]
+  left_inv hF := by rw [of_iso_trans, Iso.self_symm_id, of_iso_refl]
+  right_inv hF := by rw [of_iso_trans, Iso.symm_self_id, of_iso_refl]
 #align category_theory.is_equivalence.equiv_of_iso CategoryTheory.IsEquivalence.equivOfIso
 
 /-- If `G` and `F ⋙ G` are equivalence of categories, then `F` is also an equivalence. -/
@@ -697,20 +721,22 @@ namespace Equivalence
 
 See <https://stacks.math.columbia.edu/tag/02C3>.
 -/
-theorem essSurj_of_equivalence (F : C ⥤ D) [IsEquivalence F] : EssSurj F :=
+theorem ess_surj_of_equivalence (F : C ⥤ D) [IsEquivalence F] : EssSurj F :=
   ⟨fun Y => ⟨F.inv.obj Y, ⟨F.asEquivalence.counitIso.app Y⟩⟩⟩
-#align category_theory.equivalence.ess_surj_of_equivalence CategoryTheory.Equivalence.essSurj_of_equivalence
+#align category_theory.equivalence.ess_surj_of_equivalence 
+  CategoryTheory.Equivalence.ess_surj_of_equivalence
 
 -- see Note [lower instance priority]
 /-- An equivalence is faithful.
 
 See <https://stacks.math.columbia.edu/tag/02C3>.
 -/
-instance (priority := 100) faithfulOfEquivalence (F : C ⥤ D) [IsEquivalence F] : Faithful F where
+instance (priority := 100) faithful_of_equivalence (F : C ⥤ D) [IsEquivalence F] : Faithful F where
   map_injective := @fun X Y f g h => by
-    have p : F.inv.map (F.map f) = F.inv.map (F.map g) := congrArg F.inv.map h
+    have p : F.inv.map (F.map f) = F.inv.map (F.map g) := congrArg F.inv.map h  
     simpa only [cancel_epi, cancel_mono, IsEquivalence.inv_fun_map] using p
-#align category_theory.equivalence.faithful_of_equivalence CategoryTheory.Equivalence.faithfulOfEquivalence
+#align category_theory.equivalence.faithful_of_equivalence 
+  CategoryTheory.Equivalence.faithful_of_equivalence
 
 -- see Note [lower instance priority]
 /-- An equivalence is full.
@@ -719,8 +745,8 @@ See <https://stacks.math.columbia.edu/tag/02C3>.
 -/
 instance (priority := 100) fullOfEquivalence (F : C ⥤ D) [IsEquivalence F] : Full F
     where
-  preimage {X Y} f := F.asEquivalence.unit.app X ≫ F.inv.map f ≫ F.asEquivalence.unitInv.app Y
-  witness {X Y} f :=
+  preimage := @fun X Y f => F.asEquivalence.unit.app X ≫ F.inv.map f ≫ F.asEquivalence.unitInv.app Y
+  witness := @fun X Y f => 
     F.inv.map_injective <| by
       simpa only [IsEquivalence.inv_fun_map, assoc, Iso.inv_hom_id_app_assoc,
         Iso.inv_hom_id_app] using comp_id _
@@ -730,10 +756,11 @@ instance (priority := 100) fullOfEquivalence (F : C ⥤ D) [IsEquivalence F] : F
 private noncomputable def equivalenceInverse (F : C ⥤ D) [Full F] [Faithful F] [EssSurj F] : D ⥤ C
     where
   obj X := F.objPreimage X
-  map {X Y} f := F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
+  map := @fun X Y f => F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
   map_id X := by apply F.map_injective; aesop_cat
-  map_comp {X Y Z} f g := by apply F.map_injective; simp
--- #align category_theory.equivalence.equivalence_inverse CategoryTheory.Equivalence.equivalenceInverse
+  map_comp := @fun X Y Z f g => by apply F.map_injective; simp 
+-- #align
+--   category_theory.equivalence.equivalence_inverse CategoryTheory.Equivalence.equivalenceInverse
 /- Porting note: this is a private def in mathlib -/
 
 --
@@ -745,37 +772,44 @@ noncomputable def ofFullyFaithfullyEssSurj (F : C ⥤ D) [Full F] [Faithful F] [
     IsEquivalence F :=
   IsEquivalence.mk (equivalenceInverse F)
     (NatIso.ofComponents (fun X => (F.preimageIso <| F.objObjPreimageIso <| F.obj X).symm)
-      fun f => by
+      @fun X Y f => by
       apply F.map_injective
       aesop_cat)
     (NatIso.ofComponents F.objObjPreimageIso (by aesop_cat))
-#align category_theory.equivalence.of_fully_faithfully_ess_surj CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj
+#align category_theory.equivalence.of_fully_faithfully_ess_surj 
+  CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj
 
 @[simp]
 theorem functor_map_inj_iff (e : C ≌ D) {X Y : C} (f g : X ⟶ Y) :
     e.functor.map f = e.functor.map g ↔ f = g :=
   ⟨fun h => e.functor.map_injective h, fun h => h ▸ rfl⟩
-#align category_theory.equivalence.functor_map_inj_iff CategoryTheory.Equivalence.functor_map_inj_iff
+#align
+  category_theory.equivalence.functor_map_inj_iff CategoryTheory.Equivalence.functor_map_inj_iff
 
 @[simp]
 theorem inverse_map_inj_iff (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) :
     e.inverse.map f = e.inverse.map g ↔ f = g :=
   functor_map_inj_iff e.symm f g
-#align category_theory.equivalence.inverse_map_inj_iff CategoryTheory.Equivalence.inverse_map_inj_iff
+#align
+  category_theory.equivalence.inverse_map_inj_iff CategoryTheory.Equivalence.inverse_map_inj_iff
 
-instance essSurjInducedFunctor {C' : Type _} (e : C' ≃ D) : EssSurj (inducedFunctor e) where
-  mem_essImage Y := ⟨e.symm Y, by simpa using ⟨default⟩⟩
-#align category_theory.equivalence.ess_surj_induced_functor CategoryTheory.Equivalence.essSurjInducedFunctor
+instance ess_surj_induced_functor {C' : Type _} (e : C' ≃ D) : EssSurj (inducedFunctor e)
+    where mem_essImage Y := 
+      ⟨e.symm Y, by simp only [inducedFunctor_obj,Equiv.apply_symm_apply]; exact ⟨default⟩⟩ 
+#align category_theory.equivalence.ess_surj_induced_functor 
+  CategoryTheory.Equivalence.ess_surj_induced_functor
 
 noncomputable instance inducedFunctorOfEquiv {C' : Type _} (e : C' ≃ D) :
     IsEquivalence (inducedFunctor e) :=
   Equivalence.ofFullyFaithfullyEssSurj _
-#align category_theory.equivalence.induced_functor_of_equiv CategoryTheory.Equivalence.inducedFunctorOfEquiv
+#align category_theory.equivalence.induced_functor_of_equiv 
+  CategoryTheory.Equivalence.inducedFunctorOfEquiv
 
 noncomputable instance fullyFaithfulToEssImage (F : C ⥤ D) [Full F] [Faithful F] :
     IsEquivalence F.toEssImage :=
   ofFullyFaithfullyEssSurj F.toEssImage
-#align category_theory.equivalence.fully_faithful_to_ess_image CategoryTheory.Equivalence.fullyFaithfulToEssImage
+#align category_theory.equivalence.fully_faithful_to_ess_image 
+  CategoryTheory.Equivalence.fullyFaithfulToEssImage
 
 end Equivalence
 
diff --git a/Mathlib/CategoryTheory/Equivalence.lean.orig b/Mathlib/CategoryTheory/Equivalence.lean.orig
new file mode 100644
index 0000000000000..5d3e6dc2db975
--- /dev/null
+++ b/Mathlib/CategoryTheory/Equivalence.lean.orig
@@ -0,0 +1,813 @@
+/-
+Copyright (c) 2017 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tim Baumann, Stephen Morgan, Scott Morrison, Floris van Doorn
+
+! This file was ported from Lean 3 source module category_theory.equivalence
+! leanprover-community/mathlib commit 9aba7801eeecebb61f58a5763c2b6dd1b47dc6ef
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Functor.FullyFaithful
+import Mathlib.CategoryTheory.FullSubcategory
+import Mathlib.CategoryTheory.Whiskering
+import Mathlib.CategoryTheory.EssentialImage
+import Mathlib.Tactic.Slice
+import Mathlib.Tactic.Relation.Rfl
+import Mathlib.Tactic.Relation.Trans
+-- TODO: remove
+set_option autoImplicit false
+/-!
+# Equivalence of categories
+
+An equivalence of categories `C` and `D` is a pair of functors `F : C ⥤ D` and `G : D ⥤ C` such
+that `η : 𝟭 C ≅ F ⋙ G` and `ε : G ⋙ F ≅ 𝟭 D`. In many situations, equivalences are a better
+notion of "sameness" of categories than the stricter isomorphims of categories.
+
+Recall that one way to express that two functors `F : C ⥤ D` and `G : D ⥤ C` are adjoint is using
+two natural transformations `η : 𝟭 C ⟶ F ⋙ G` and `ε : G ⋙ F ⟶ 𝟭 D`, called the unit and the
+counit, such that the compositions `F ⟶ FGF ⟶ F` and `G ⟶ GFG ⟶ G` are the identity. Unfortunately,
+it is not the case that the natural isomorphisms `η` and `ε` in the definition of an equivalence
+automatically give an adjunction. However, it is true that
+* if one of the two compositions is the identity, then so is the other, and
+* given an equivalence of categories, it is always possible to refine `η` in such a way that the
+  identities are satisfied.
+
+For this reason, in mathlib we define an equivalence to be a "half-adjoint equivalence", which is
+a tuple `(F, G, η, ε)` as in the first paragraph such that the composite `F ⟶ FGF ⟶ F` is the
+identity. By the remark above, this already implies that the tuple is an "adjoint equivalence",
+i.e., that the composite `G ⟶ GFG ⟶ G` is also the identity.
+
+We also define essentially surjective functors and show that a functor is an equivalence if and only
+if it is full, faithful and essentially surjective.
+
+## Main definitions
+
+* `Equivalence`: bundled (half-)adjoint equivalences of categories
+* `IsEquivalence`: type class on a functor `F` containing the data of the inverse `G` as well as
+  the natural isomorphisms `η` and `ε`.
+* `EssSurj`: type class on a functor `F` containing the data of the preimages and the isomorphisms
+  `F.obj (preimage d) ≅ d`.
+
+## Main results
+
+* `Equivalence.mk`: upgrade an equivalence to a (half-)adjoint equivalence
+* `IsEquivalence.equiv_of_iso`: when `F` and `G` are isomorphic functors, `F` is an equivalence
+iff `G` is.
+* `Equivalence.of_fully_faithfully_essSurj`: a fully faithful essentially surjective functor is an
+  equivalence.
+
+## Notations
+
+We write `C ≌ D` (`\backcong`, not to be confused with `≅`/`\cong`) for a bundled equivalence.
+
+-/
+
+namespace CategoryTheory
+
+open CategoryTheory.Functor NatIso Category
+
+-- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
+universe v₁ v₂ v₃ u₁ u₂ u₃
+
+/-- We define an equivalence as a (half)-adjoint equivalence, a pair of functors with
+  a unit and counit which are natural isomorphisms and the triangle law `Fη ≫ εF = 1`, or in other
+  words the composite `F ⟶ FGF ⟶ F` is the identity.
+
+  In `unit_inverse_comp`, we show that this is actually an adjoint equivalence, i.e., that the
+  composite `G ⟶ GFG ⟶ G` is also the identity.
+
+  The triangle equation is written as a family of equalities between morphisms, it is more
+  complicated if we write it as an equality of natural transformations, because then we would have
+  to insert natural transformations like `F ⟶ F1`.
+
+See <https://stacks.math.columbia.edu/tag/001J>
+-/
+structure Equivalence (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D] where mk' ::
+  functor : C ⥤ D
+  inverse : D ⥤ C
+  unitIso : 𝟭 C ≅ functor ⋙ inverse
+  counitIso : inverse ⋙ functor ≅ 𝟭 D
+  functor_unit_iso_comp' : ∀ X : C, functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 𝟙 (functor.obj X) := by aesop_cat
+#align category_theory.equivalence CategoryTheory.Equivalence
+
+restate_axiom Equivalence.functor_unit_iso_comp'
+
+-- mathport name: «expr ≌ »
+infixr:10 " ≌ " => Equivalence
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+
+namespace Equivalence
+
+/-- The unit of an equivalence of categories. -/
+abbrev unit (e : C ≌ D) : 𝟭 C ⟶ e.functor ⋙ e.inverse :=
+  e.unitIso.hom
+#align category_theory.equivalence.unit CategoryTheory.Equivalence.unit
+
+/-- The counit of an equivalence of categories. -/
+abbrev counit (e : C ≌ D) : e.inverse ⋙ e.functor ⟶ 𝟭 D :=
+  e.counitIso.hom
+#align category_theory.equivalence.counit CategoryTheory.Equivalence.counit
+
+/-- The inverse of the unit of an equivalence of categories. -/
+abbrev unitInv (e : C ≌ D) : e.functor ⋙ e.inverse ⟶ 𝟭 C :=
+  e.unitIso.inv
+#align category_theory.equivalence.unit_inv CategoryTheory.Equivalence.unitInv
+
+/-- The inverse of the counit of an equivalence of categories. -/
+abbrev counitInv (e : C ≌ D) : 𝟭 D ⟶ e.inverse ⋙ e.functor :=
+  e.counitIso.inv
+#align category_theory.equivalence.counit_inv CategoryTheory.Equivalence.counitInv
+
+/- While these abbreviations are convenient, they also cause some trouble,
+preventing structure projections from unfolding. -/
+@[simp]
+theorem equivalence_mk'_unit (functor inverse unit_iso counit_iso f) :
+    (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unit = unit_iso.hom :=
+  rfl
+#align
+  category_theory.equivalence.equivalence_mk'_unit CategoryTheory.Equivalence.equivalence_mk'_unit
+
+@[simp]
+theorem equivalence_mk'_counit (functor inverse unit_iso counit_iso f) :
+    (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counit = counit_iso.hom :=
+  rfl
+#align
+  category_theory.equivalence.equivalence_mk'_counit CategoryTheory.Equivalence.equivalence_mk'_counit
+
+@[simp]
+theorem equivalence_mk'_unitInv (functor inverse unit_iso counit_iso f) :
+    (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).unitInv = unit_iso.inv :=
+  rfl
+#align
+  category_theory.equivalence.equivalence_mk'_unit_inv CategoryTheory.Equivalence.equivalence_mk'_unitInv
+
+@[simp]
+theorem equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) :
+    (⟨functor, inverse, unit_iso, counit_iso, f⟩ : C ≌ D).counitInv = counit_iso.inv :=
+  rfl
+#align
+  category_theory.equivalence.equivalence_mk'_counit_inv CategoryTheory.Equivalence.equivalence_mk'_counitInv
+
+@[simp]
+theorem functor_unit_comp (e : C ≌ D) (X : C) :
+    e.functor.map (e.unit.app X) ≫ e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X) :=
+  e.functor_unit_iso_comp X
+#align category_theory.equivalence.functor_unit_comp CategoryTheory.Equivalence.functor_unit_comp
+
+@[simp]
+theorem counitInv_functor_comp (e : C ≌ D) (X : C) :
+    e.counitInv.app (e.functor.obj X) ≫ e.functor.map (e.unitInv.app X) = 𝟙 (e.functor.obj X) :=
+  by
+  erw [Iso.inv_eq_inv (e.functor.mapIso (e.unitIso.app X) ≪≫ e.counitIso.app (e.functor.obj X))
+      (Iso.refl _)]
+  exact e.functor_unit_comp X
+#align
+  category_theory.equivalence.counit_inv_functor_comp CategoryTheory.Equivalence.counitInv_functor_comp
+
+theorem counit_inv_app_functor (e : C ≌ D) (X : C) :
+    e.counitInv.app (e.functor.obj X) = e.functor.map (e.unit.app X) :=
+  by
+  symm
+  erw [← Iso.comp_hom_eq_id (e.counitIso.app _), functor_unit_comp]
+  rfl
+#align
+  category_theory.equivalence.counit_inv_app_functor CategoryTheory.Equivalence.counit_inv_app_functor
+
+theorem counit_app_functor (e : C ≌ D) (X : C) :
+    e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X) :=
+  by
+  erw [← Iso.hom_comp_eq_id (e.functor.mapIso (e.unitIso.app X)), functor_unit_comp]
+  rfl
+#align category_theory.equivalence.counit_app_functor CategoryTheory.Equivalence.counit_app_functor
+
+/-- The other triangle equality. The proof follows the following proof in Globular:
+  http://globular.science/1905.001 -/
+@[simp]
+theorem unit_inverse_comp (e : C ≌ D) (Y : D) :
+    e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y) :=
+  by
+  rw [← id_comp (e.inverse.map _), ← map_id e.inverse, ← counitInv_functor_comp, map_comp]
+  dsimp
+  rw [← Iso.hom_inv_id_assoc (e.unitIso.app _) (e.inverse.map (e.functor.map _)), app_hom, app_inv]
+  sliceLHS 2 3 => erw [e.unit.naturality]
+  sliceLHS 1 2 => erw [e.unit.naturality]
+  sliceLHS 4 4 =>
+    rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]
+  sliceLHS 3 4 =>
+    erw [← map_comp e.inverse, e.counit.naturality]
+    erw [(e.counitIso.app _).hom_inv_id, map_id]
+  erw [id_comp]
+  sliceLHS 2 3 => erw [← map_comp e.inverse, e.counitIso.inv.naturality, map_comp]
+  sliceLHS 3 4 => erw [e.unitInv.naturality]
+  sliceLHS 4 5 => erw [← map_comp (e.functor ⋙ e.inverse), (e.unitIso.app _).hom_inv_id, map_id]
+  erw [id_comp]
+  sliceLHS 3 4 => erw [← e.unitInv.naturality]
+  sliceLHS 2 3 =>
+    erw [← map_comp e.inverse, ← e.counitIso.inv.naturality, (e.counitIso.app _).hom_inv_id,
+      map_id]
+  erw [id_comp, (e.unitIso.app _).hom_inv_id]; rfl
+#align category_theory.equivalence.unit_inverse_comp CategoryTheory.Equivalence.unit_inverse_comp
+
+@[simp]
+theorem inverse_counit_inv_comp (e : C ≌ D) (Y : D) :
+    e.inverse.map (e.counitInv.app Y) ≫ e.unitInv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) :=
+  by
+  erw [Iso.inv_eq_inv (e.unitIso.app (e.inverse.obj Y) ≪≫ e.inverse.mapIso (e.counitIso.app Y))
+      (Iso.refl _)]
+  exact e.unit_inverse_comp Y
+#align
+  category_theory.equivalence.inverse_counit_inv_comp CategoryTheory.Equivalence.inverse_counit_inv_comp
+
+theorem unit_app_inverse (e : C ≌ D) (Y : D) :
+    e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y) := by
+  erw [← Iso.comp_hom_eq_id (e.inverse.mapIso (e.counitIso.app Y)), unit_inverse_comp]
+  dsimp
+#align category_theory.equivalence.unit_app_inverse CategoryTheory.Equivalence.unit_app_inverse
+
+theorem unit_inv_app_inverse (e : C ≌ D) (Y : D) :
+    e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y) := by
+  symm
+  erw [← Iso.hom_comp_eq_id (e.unitIso.app _), unit_inverse_comp]
+  rfl
+#align
+  category_theory.equivalence.unit_inv_app_inverse CategoryTheory.Equivalence.unit_inv_app_inverse
+
+@[simp]
+theorem fun_inv_map (e : C ≌ D) (X Y : D) (f : X ⟶ Y) :
+    e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counitInv.app Y :=
+  (NatIso.naturality_2 e.counitIso f).symm
+#align category_theory.equivalence.fun_inv_map CategoryTheory.Equivalence.fun_inv_map
+
+@[simp]
+theorem inv_fun_map (e : C ≌ D) (X Y : C) (f : X ⟶ Y) :
+    e.inverse.map (e.functor.map f) = e.unitInv.app X ≫ f ≫ e.unit.app Y :=
+  (NatIso.naturality_1 e.unitIso f).symm
+#align category_theory.equivalence.inv_fun_map CategoryTheory.Equivalence.inv_fun_map
+
+section
+
+-- In this section we convert an arbitrary equivalence to a half-adjoint equivalence.
+variable {F : C ⥤ D} {G : D ⥤ C} (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D)
+
+/-- If `η : 𝟭 C ≅ F ⋙ G` is part of a (not necessarily half-adjoint) equivalence, we can upgrade it
+to a refined natural isomorphism `adjointify_η η : 𝟭 C ≅ F ⋙ G` which exhibits the properties
+required for a half-adjoint equivalence. See `equivalence.mk`. -/
+def adjointifyη : 𝟭 C ≅ F ⋙ G := by 
+  calc
+    𝟭 C ≅ F ⋙ G := η
+    _ ≅ F ⋙ 𝟭 D ⋙ G := isoWhiskerLeft F (leftUnitor G).symm
+    _ ≅ F ⋙ (G ⋙ F) ⋙ G := isoWhiskerLeft F (isoWhiskerRight ε.symm G)
+    _ ≅ F ⋙ G ⋙ F ⋙ G := isoWhiskerLeft F (associator G F G)
+    _ ≅ (F ⋙ G) ⋙ F ⋙ G := (associator F G (F ⋙ G)).symm
+    _ ≅ 𝟭 C ⋙ F ⋙ G := isoWhiskerRight η.symm (F ⋙ G)
+    _ ≅ F ⋙ G := leftUnitor (F ⋙ G)
+    
+#align category_theory.equivalence.adjointify_η CategoryTheory.Equivalence.adjointifyη
+
+theorem adjointify_η_ε (X : C) :
+    F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X) :=
+  by
+  dsimp [adjointifyη,Trans.trans]
+  simp
+  have := ε.hom.naturality (F.map (η.inv.app X)); dsimp at this; rw [this]; clear this
+  rw [← assoc _ _ (F.map _)]
+  have := ε.hom.naturality (ε.inv.app <| F.obj X); dsimp at this; rw [this]; clear this
+  have := (ε.app <| F.obj X).hom_inv_id; dsimp at this; rw [this]; clear this
+  rw [id_comp]; have := (F.mapIso <| η.app X).hom_inv_id; dsimp at this; rw [this]
+#align category_theory.equivalence.adjointify_η_ε CategoryTheory.Equivalence.adjointify_η_ε
+
+end
+
+/-- Every equivalence of categories consisting of functors `F` and `G` such that `F ⋙ G` and
+    `G ⋙ F` are naturally isomorphic to identity functors can be transformed into a half-adjoint
+    equivalence without changing `F` or `G`. -/
+protected def mk (F : C ⥤ D) (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) : C ≌ D :=
+  ⟨F, G, adjointifyη η ε, ε, adjointify_η_ε η ε⟩
+#align category_theory.equivalence.mk CategoryTheory.Equivalence.mk
+
+/-- Equivalence of categories is reflexive. -/
+@[refl, simps]
+def refl : C ≌ C :=
+  ⟨𝟭 C, 𝟭 C, Iso.refl _, Iso.refl _, fun X => Category.id_comp _⟩
+#align category_theory.equivalence.refl CategoryTheory.Equivalence.refl
+
+instance : Inhabited (C ≌ C) :=
+  ⟨refl⟩
+
+/-- Equivalence of categories is symmetric. -/
+@[symm, simps]
+def symm (e : C ≌ D) : D ≌ C :=
+  ⟨e.inverse, e.functor, e.counitIso.symm, e.unitIso.symm, e.inverse_counit_inv_comp⟩
+#align category_theory.equivalence.symm CategoryTheory.Equivalence.symm
+
+variable {E : Type u₃} [Category.{v₃} E]
+
+/-- Equivalence of categories is transitive. -/
+@[trans, simps]
+def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E
+    where
+  functor := e.functor ⋙ f.functor
+  inverse := f.inverse ⋙ e.inverse
+  unitIso := by
+    refine' Iso.trans e.unitIso _
+    exact isoWhiskerLeft e.functor (isoWhiskerRight f.unitIso e.inverse)
+  counitIso := by
+    refine' Iso.trans _ f.counitIso
+    exact isoWhiskerLeft f.inverse (isoWhiskerRight e.counitIso f.functor)
+  -- We wouldn't have needed to give this proof if we'd used `equivalence.mk`,
+  -- but we choose to avoid using that here, for the sake of good structure projection `simp`
+  -- lemmas.
+  functor_unit_iso_comp' X := by
+    dsimp
+    rw [← f.functor.map_comp_assoc, e.functor.map_comp, ← counit_inv_app_functor, fun_inv_map,
+      Iso.inv_hom_id_app_assoc, assoc, Iso.inv_hom_id_app, counit_app_functor, ← Functor.map_comp]
+    erw [comp_id, Iso.hom_inv_id_app, Functor.map_id]
+#align category_theory.equivalence.trans CategoryTheory.Equivalence.trans
+
+/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
+functor. -/
+def funInvIdAssoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F ≅ F :=
+  (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight e.unitIso.symm F ≪≫ F.leftUnitor
+#align category_theory.equivalence.fun_inv_id_assoc CategoryTheory.Equivalence.funInvIdAssoc
+
+@[simp]
+theorem fun_inv_id_assoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
+    (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X) :=
+  by
+  dsimp [funInvIdAssoc]
+  aesop_cat
+#align
+  category_theory.equivalence.fun_inv_id_assoc_hom_app CategoryTheory.Equivalence.fun_inv_id_assoc_hom_app
+
+@[simp]
+theorem fun_inv_id_assoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
+    (funInvIdAssoc e F).inv.app X = F.map (e.unit.app X) :=
+  by
+  dsimp [funInvIdAssoc]
+  aesop_cat
+#align
+  category_theory.equivalence.fun_inv_id_assoc_inv_app CategoryTheory.Equivalence.fun_inv_id_assoc_inv_app
+
+/-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
+functor. -/
+def invFunIdAssoc (e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ F ≅ F :=
+  (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight e.counitIso F ≪≫ F.leftUnitor
+#align category_theory.equivalence.inv_fun_id_assoc CategoryTheory.Equivalence.invFunIdAssoc
+
+@[simp]
+theorem inv_fun_id_assoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
+    (invFunIdAssoc e F).hom.app X = F.map (e.counit.app X) :=
+  by
+  dsimp [invFunIdAssoc]
+  aesop_cat
+#align
+  category_theory.equivalence.inv_fun_id_assoc_hom_app CategoryTheory.Equivalence.inv_fun_id_assoc_hom_app
+
+@[simp]
+theorem inv_fun_id_assoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
+    (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X) :=
+  by
+  dsimp [invFunIdAssoc]
+  aesop_cat
+#align
+  category_theory.equivalence.inv_fun_id_assoc_inv_app CategoryTheory.Equivalence.inv_fun_id_assoc_inv_app
+
+/-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`. -/
+@[simps! functor inverse unitIso counitIso]
+def congrLeft (e : C ≌ D) : C ⥤ E ≌ D ⥤ E :=
+  Equivalence.mk ((whiskeringLeft _ _ _).obj e.inverse) ((whiskeringLeft _ _ _).obj e.functor)
+    (NatIso.ofComponents (fun F => (e.funInvIdAssoc F).symm) (by aesop_cat))
+    (NatIso.ofComponents (fun F => e.invFunIdAssoc F) (by aesop_cat))
+#align category_theory.equivalence.congr_left CategoryTheory.Equivalence.congrLeft
+
+/-- If `C` is equivalent to `D`, then `E ⥤ C` is equivalent to `E ⥤ D`. -/
+@[simps! functor inverse unitIso counitIso]
+def congrRight (e : C ≌ D) : E ⥤ C ≌ E ⥤ D :=
+  Equivalence.mk ((whiskeringRight _ _ _).obj e.functor) ((whiskeringRight _ _ _).obj e.inverse)
+    (NatIso.ofComponents
+      (fun F => F.rightUnitor.symm ≪≫ isoWhiskerLeft F e.unitIso ≪≫ Functor.associator _ _ _)
+      (by aesop_cat))
+    (NatIso.ofComponents
+      (fun F => Functor.associator _ _ _ ≪≫ isoWhiskerLeft F e.counitIso ≪≫ F.rightUnitor)
+      (by aesop_cat))
+#align category_theory.equivalence.congr_right CategoryTheory.Equivalence.congrRight
+
+section CancellationLemmas
+
+variable (e : C ≌ D)
+
+/- We need special forms of `cancel_nat_iso_hom_right(_assoc)` and
+`cancel_nat_iso_inv_right(_assoc)` for units and counits, because neither `simp` or `rw` will apply
+those lemmas in this setting without providing `e.unit_iso` (or similar) as an explicit argument.
+We also provide the lemmas for length four compositions, since they're occasionally useful.
+(e.g. in proving that equivalences take monos to monos) -/
+@[simp]
+theorem cancel_unit_right {X Y : C} (f f' : X ⟶ Y) :
+    f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f' := by simp only [cancel_mono]
+#align category_theory.equivalence.cancel_unit_right CategoryTheory.Equivalence.cancel_unit_right
+
+@[simp]
+theorem cancel_unit_inv_right {X Y : C} (f f' : X ⟶ e.inverse.obj (e.functor.obj Y)) :
+    f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f' := by simp only [cancel_mono]
+#align
+  category_theory.equivalence.cancel_unit_inv_right CategoryTheory.Equivalence.cancel_unit_inv_right
+
+@[simp]
+theorem cancel_counit_right {X Y : D} (f f' : X ⟶ e.functor.obj (e.inverse.obj Y)) :
+    f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f' := by simp only [cancel_mono]
+#align
+  category_theory.equivalence.cancel_counit_right CategoryTheory.Equivalence.cancel_counit_right
+
+@[simp]
+theorem cancel_counit_inv_right {X Y : D} (f f' : X ⟶ Y) :
+    f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f' := by simp only [cancel_mono]
+#align
+  category_theory.equivalence.cancel_counit_inv_right CategoryTheory.Equivalence.cancel_counit_inv_right
+
+@[simp]
+theorem cancel_unit_right_assoc {W X X' Y : C} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X') (g' : X' ⟶ Y) :
+    f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g' := by
+  simp only [← Category.assoc, cancel_mono]
+#align
+  category_theory.equivalence.cancel_unit_right_assoc CategoryTheory.Equivalence.cancel_unit_right_assoc
+
+@[simp]
+theorem cancel_counit_inv_right_assoc {W X X' Y : D} (f : W ⟶ X) (g : X ⟶ Y) (f' : W ⟶ X')
+    (g' : X' ⟶ Y) : f ≫ g ≫ e.counitInv.app Y = f' ≫ g' ≫ e.counitInv.app Y ↔ f ≫ g = f' ≫ g' := by
+  simp only [← Category.assoc, cancel_mono]
+#align
+  category_theory.equivalence.cancel_counit_inv_right_assoc CategoryTheory.Equivalence.cancel_counit_inv_right_assoc
+
+@[simp]
+theorem cancel_unit_right_assoc' {W X X' Y Y' Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
+    (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
+    f ≫ g ≫ h ≫ e.unit.app Z = f' ≫ g' ≫ h' ≫ e.unit.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' := by
+  simp only [← Category.assoc, cancel_mono]
+#align
+  category_theory.equivalence.cancel_unit_right_assoc' CategoryTheory.Equivalence.cancel_unit_right_assoc'
+
+@[simp]
+theorem cancel_counit_inv_right_assoc' {W X X' Y Y' Z : D} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z)
+    (f' : W ⟶ X') (g' : X' ⟶ Y') (h' : Y' ⟶ Z) :
+    f ≫ g ≫ h ≫ e.counitInv.app Z = f' ≫ g' ≫ h' ≫ e.counitInv.app Z ↔ f ≫ g ≫ h = f' ≫ g' ≫ h' :=
+  by simp only [← Category.assoc, cancel_mono]
+#align
+  category_theory.equivalence.cancel_counit_inv_right_assoc' CategoryTheory.Equivalence.cancel_counit_inv_right_assoc'
+
+end CancellationLemmas
+
+section
+
+-- There's of course a monoid structure on `C ≌ C`,
+-- but let's not encourage using it.
+-- The power structure is nevertheless useful.
+/-- Natural number powers of an auto-equivalence.  Use `(^)` instead. -/
+def powNat (e : C ≌ C) : ℕ → (C ≌ C)
+  | 0 => Equivalence.refl
+  | 1 => e
+  | n + 2 => e.trans (powNat e (n + 1))
+#align category_theory.equivalence.pow_nat CategoryTheory.Equivalence.powNat
+
+/-- Powers of an auto-equivalence.  Use `(^)` instead. -/
+def pow (e : C ≌ C) : ℤ → (C ≌ C)
+  | Int.ofNat n => e.powNat n
+  | Int.negSucc n => e.symm.powNat (n + 1)
+#align category_theory.equivalence.pow CategoryTheory.Equivalence.pow
+
+instance : Pow (C ≌ C) ℤ :=
+  ⟨pow⟩
+
+@[simp]
+theorem pow_zero (e : C ≌ C) : e ^ (0 : ℤ) = Equivalence.refl :=
+  rfl
+#align category_theory.equivalence.pow_zero CategoryTheory.Equivalence.pow_zero
+
+@[simp]
+theorem pow_one (e : C ≌ C) : e ^ (1 : ℤ) = e :=
+  rfl
+#align category_theory.equivalence.pow_one CategoryTheory.Equivalence.pow_one
+
+@[simp]
+theorem pow_neg_one (e : C ≌ C) : e ^ (-1 : ℤ) = e.symm :=
+  rfl
+#align category_theory.equivalence.pow_neg_one CategoryTheory.Equivalence.pow_neg_one
+
+-- TODO as necessary, add the natural isomorphisms `(e^a).trans e^b ≅ e^(a+b)`.
+-- At this point, we haven't even defined the category of equivalences.
+end
+
+end Equivalence
+
+/-- A functor that is part of a (half) adjoint equivalence -/
+class IsEquivalence (F : C ⥤ D) where mk' ::
+  inverse : D ⥤ C
+  unitIso : 𝟭 C ≅ F ⋙ inverse
+  counitIso : inverse ⋙ F ≅ 𝟭 D
+  functor_unit_iso_comp' :
+    ∀ X : C,
+      F.map ((unitIso.hom : 𝟭 C ⟶ F ⋙ inverse).app X) ≫ counitIso.hom.app (F.obj X) =
+        𝟙 (F.obj X) := by
+    aesop_cat
+#align category_theory.is_equivalence CategoryTheory.IsEquivalence
+
+restate_axiom IsEquivalence.functor_unit_iso_comp'
+
+attribute [reassoc (attr := simp)] IsEquivalence.functor_unit_iso_comp
+
+namespace IsEquivalence
+
+instance ofEquivalence (F : C ≌ D) : IsEquivalence F.functor :=
+  { F with }
+#align category_theory.is_equivalence.of_equivalence CategoryTheory.IsEquivalence.ofEquivalence
+
+instance ofEquivalenceInverse (F : C ≌ D) : IsEquivalence F.inverse :=
+  IsEquivalence.ofEquivalence F.symm
+#align
+  category_theory.is_equivalence.of_equivalence_inverse CategoryTheory.IsEquivalence.ofEquivalenceInverse
+
+open Equivalence
+
+/-- To see that a functor is an equivalence, it suffices to provide an inverse functor `G` such that
+    `F ⋙ G` and `G ⋙ F` are naturally isomorphic to identity functors. -/
+protected def mk {F : C ⥤ D} (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) : IsEquivalence F :=
+  ⟨G, adjointifyη η ε, ε, adjointify_η_ε η ε⟩
+#align category_theory.is_equivalence.mk CategoryTheory.IsEquivalence.mk
+
+end IsEquivalence
+
+namespace Functor
+
+/-- Interpret a functor that is an equivalence as an equivalence. -/
+def asEquivalence (F : C ⥤ D) [IsEquivalence F] : C ≌ D :=
+  ⟨F, IsEquivalence.inverse F, IsEquivalence.unitIso, IsEquivalence.counitIso,
+    IsEquivalence.functor_unit_iso_comp⟩
+#align category_theory.functor.as_equivalence CategoryTheory.Functor.asEquivalence
+
+instance isEquivalenceRefl : IsEquivalence (𝟭 C) :=
+  IsEquivalence.ofEquivalence Equivalence.refl
+#align category_theory.functor.is_equivalence_refl CategoryTheory.Functor.isEquivalenceRefl
+
+/-- The inverse functor of a functor that is an equivalence. -/
+def inv (F : C ⥤ D) [IsEquivalence F] : D ⥤ C :=
+  IsEquivalence.inverse F
+#align category_theory.functor.inv CategoryTheory.Functor.inv
+
+instance isEquivalenceInv (F : C ⥤ D) [IsEquivalence F] : IsEquivalence F.inv :=
+  IsEquivalence.ofEquivalence F.asEquivalence.symm
+#align category_theory.functor.is_equivalence_inv CategoryTheory.Functor.isEquivalenceInv
+
+@[simp]
+theorem as_equivalence_functor (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.functor = F :=
+  rfl
+#align category_theory.functor.as_equivalence_functor CategoryTheory.Functor.as_equivalence_functor
+
+@[simp]
+theorem as_equivalence_inverse (F : C ⥤ D) [IsEquivalence F] : F.asEquivalence.inverse = inv F :=
+  rfl
+#align category_theory.functor.as_equivalence_inverse CategoryTheory.Functor.as_equivalence_inverse
+
+@[simp]
+theorem as_equivalence_unit {F : C ⥤ D} [IsEquivalence F] :
+    F.asEquivalence.unitIso = IsEquivalence.unitIso :=
+  rfl
+#align category_theory.functor.as_equivalence_unit CategoryTheory.Functor.as_equivalence_unit
+
+@[simp]
+theorem as_equivalence_counit {F : C ⥤ D} [IsEquivalence F] :
+    F.asEquivalence.counitIso = IsEquivalence.counitIso :=
+  rfl
+#align category_theory.functor.as_equivalence_counit CategoryTheory.Functor.as_equivalence_counit
+
+@[simp]
+theorem inv_inv (F : C ⥤ D) [IsEquivalence F] : inv (inv F) = F :=
+  rfl
+#align category_theory.functor.inv_inv CategoryTheory.Functor.inv_inv
+
+variable {E : Type u₃} [Category.{v₃} E]
+
+instance isEquivalenceTrans (F : C ⥤ D) (G : D ⥤ E) [IsEquivalence F] [IsEquivalence G] :
+    IsEquivalence (F ⋙ G) :=
+  IsEquivalence.ofEquivalence (Equivalence.trans (asEquivalence F) (asEquivalence G))
+#align category_theory.functor.is_equivalence_trans CategoryTheory.Functor.isEquivalenceTrans
+
+end Functor
+
+namespace Equivalence
+
+@[simp]
+theorem functor_inv (E : C ≌ D) : E.functor.inv = E.inverse :=
+  rfl
+#align category_theory.equivalence.functor_inv CategoryTheory.Equivalence.functor_inv
+
+@[simp]
+theorem inverse_inv (E : C ≌ D) : E.inverse.inv = E.functor :=
+  rfl
+#align category_theory.equivalence.inverse_inv CategoryTheory.Equivalence.inverse_inv
+
+@[simp]
+theorem functor_as_equivalence (E : C ≌ D) : E.functor.asEquivalence = E :=
+  by
+  cases E
+  congr
+#align
+  category_theory.equivalence.functor_as_equivalence CategoryTheory.Equivalence.functor_as_equivalence
+
+@[simp]
+theorem inverse_as_equivalence (E : C ≌ D) : E.inverse.asEquivalence = E.symm :=
+  by
+  cases E
+  congr
+#align
+  category_theory.equivalence.inverse_as_equivalence CategoryTheory.Equivalence.inverse_as_equivalence
+
+end Equivalence
+
+namespace IsEquivalence
+
+@[simp]
+theorem fun_inv_map (F : C ⥤ D) [IsEquivalence F] (X Y : D) (f : X ⟶ Y) :
+    F.map (F.inv.map f) = F.asEquivalence.counit.app X ≫ f ≫ F.asEquivalence.counitInv.app Y :=
+  by
+  erw [NatIso.naturality_2]
+  rfl
+#align category_theory.is_equivalence.fun_inv_map CategoryTheory.IsEquivalence.fun_inv_map
+
+@[simp]
+theorem inv_fun_map (F : C ⥤ D) [IsEquivalence F] (X Y : C) (f : X ⟶ Y) :
+    F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y :=
+  by
+  erw [NatIso.naturality_1]
+  rfl
+#align category_theory.is_equivalence.inv_fun_map CategoryTheory.IsEquivalence.inv_fun_map
+
+/-- When a functor `F` is an equivalence of categories, and `G` is isomorphic to `F`, then
+`G` is also an equivalence of categories. -/
+@[simps]
+def ofIso {F G : C ⥤ D} (e : F ≅ G) (hF : IsEquivalence F) : IsEquivalence G
+    where
+  inverse := hF.inverse
+  unitIso := hF.unitIso ≪≫ NatIso.hcomp e (Iso.refl hF.inverse)
+  counitIso := NatIso.hcomp (Iso.refl hF.inverse) e.symm ≪≫ hF.counitIso
+  functor_unit_iso_comp' X := by
+    dsimp [NatIso.hcomp]
+    erw [id_comp, F.map_id, comp_id]
+    apply (cancel_epi (e.hom.app X)).mp
+    sliceLHS 1 2 => rw [← e.hom.naturality]
+    sliceLHS 2 3 => rw [← NatTrans.vcomp_app', e.hom_inv_id]
+    simp only [NatTrans.id_app, id_comp, comp_id, F.map_comp, assoc]
+    erw [hF.counitIso.hom.naturality]
+    sliceLHS 1 2 => rw [functor_unit_iso_comp]
+    simp only [Functor.id_map, id_comp]
+#align category_theory.is_equivalence.of_iso CategoryTheory.IsEquivalence.ofIso
+
+/-- Compatibility of `of_iso` with the composition of isomorphisms of functors -/
+theorem of_iso_trans {F G H : C ⥤ D} (e : F ≅ G) (e' : G ≅ H) (hF : IsEquivalence F) :
+    ofIso e' (ofIso e hF) = ofIso (e ≪≫ e') hF :=
+  by
+  dsimp [ofIso]
+  congr 1 <;> ext X <;> dsimp [NatIso.hcomp]
+  · simp only [id_comp, assoc, Functor.map_comp]
+  · simp only [Functor.map_id, comp_id, id_comp, assoc]
+#align category_theory.is_equivalence.of_iso_trans CategoryTheory.IsEquivalence.of_iso_trans
+
+/-- Compatibility of `of_iso` with identity isomorphisms of functors -/
+theorem of_iso_refl (F : C ⥤ D) (hF : IsEquivalence F) : ofIso (Iso.refl F) hF = hF :=
+  by
+  rcases hF with ⟨Finv, Funit, Fcounit, Fcomp⟩
+  dsimp [ofIso]
+  congr 1 <;> ext X <;> dsimp [NatIso.hcomp]
+  · simp only [comp_id, map_id]
+  · simp only [id_comp, map_id]
+#align category_theory.is_equivalence.of_iso_refl CategoryTheory.IsEquivalence.of_iso_refl
+
+/-- When `F` and `G` are two isomorphic functors, then `F` is an equivalence iff `G` is. -/
+@[simps]
+def equivOfIso {F G : C ⥤ D} (e : F ≅ G) : IsEquivalence F ≃ IsEquivalence G
+    where
+  toFun := ofIso e
+  invFun := ofIso e.symm
+  left_inv hF := by rw [of_iso_trans, Iso.self_symm_id, of_iso_refl]
+  right_inv hF := by rw [of_iso_trans, Iso.symm_self_id, of_iso_refl]
+#align category_theory.is_equivalence.equiv_of_iso CategoryTheory.IsEquivalence.equivOfIso
+
+/-- If `G` and `F ⋙ G` are equivalence of categories, then `F` is also an equivalence. -/
+@[simp]
+def cancelCompRight {E : Type _} [Category E] (F : C ⥤ D) (G : D ⥤ E) (hG : IsEquivalence G)
+    (_ : IsEquivalence (F ⋙ G)) : IsEquivalence F :=
+  ofIso (Functor.associator F G G.inv ≪≫ NatIso.hcomp (Iso.refl F) hG.unitIso.symm ≪≫ rightUnitor F)
+    (Functor.isEquivalenceTrans (F ⋙ G) G.inv)
+#align category_theory.is_equivalence.cancel_comp_right CategoryTheory.IsEquivalence.cancelCompRight
+
+/-- If `F` and `F ⋙ G` are equivalence of categories, then `G` is also an equivalence. -/
+@[simp]
+def cancelCompLeft {E : Type _} [Category E] (F : C ⥤ D) (G : D ⥤ E) (hF : IsEquivalence F)
+    (_ : IsEquivalence (F ⋙ G)) : IsEquivalence G :=
+  ofIso
+    ((Functor.associator F.inv F G).symm ≪≫ NatIso.hcomp hF.counitIso (Iso.refl G) ≪≫ leftUnitor G)
+    (Functor.isEquivalenceTrans F.inv (F ⋙ G))
+#align category_theory.is_equivalence.cancel_comp_left CategoryTheory.IsEquivalence.cancelCompLeft
+
+end IsEquivalence
+
+namespace Equivalence
+
+/-- An equivalence is essentially surjective.
+
+See <https://stacks.math.columbia.edu/tag/02C3>.
+-/
+theorem ess_surj_of_equivalence (F : C ⥤ D) [IsEquivalence F] : EssSurj F :=
+  ⟨fun Y => ⟨F.inv.obj Y, ⟨F.asEquivalence.counitIso.app Y⟩⟩⟩
+#align
+  category_theory.equivalence.ess_surj_of_equivalence CategoryTheory.Equivalence.ess_surj_of_equivalence
+
+-- see Note [lower instance priority]
+/-- An equivalence is faithful.
+
+See <https://stacks.math.columbia.edu/tag/02C3>.
+-/
+instance (priority := 100) faithful_of_equivalence (F : C ⥤ D) [IsEquivalence F] : Faithful F where
+  map_injective := @fun X Y f g h => by
+    have p : F.inv.map (F.map f) = F.inv.map (F.map g) := congrArg F.inv.map h  
+    simpa only [cancel_epi, cancel_mono, IsEquivalence.inv_fun_map] using p
+#align
+  category_theory.equivalence.faithful_of_equivalence CategoryTheory.Equivalence.faithful_of_equivalence
+
+-- see Note [lower instance priority]
+/-- An equivalence is full.
+
+See <https://stacks.math.columbia.edu/tag/02C3>.
+-/
+instance (priority := 100) fullOfEquivalence (F : C ⥤ D) [IsEquivalence F] : Full F
+    where
+  preimage := @fun X Y f => F.asEquivalence.unit.app X ≫ F.inv.map f ≫ F.asEquivalence.unitInv.app Y
+  witness := @fun X Y f => 
+    F.inv.map_injective <| by
+      simpa only [IsEquivalence.inv_fun_map, assoc, Iso.inv_hom_id_app_assoc,
+        Iso.inv_hom_id_app] using comp_id _
+#align category_theory.equivalence.full_of_equivalence CategoryTheory.Equivalence.fullOfEquivalence
+
+@[simps]
+private noncomputable def equivalenceInverse (F : C ⥤ D) [Full F] [Faithful F] [EssSurj F] : D ⥤ C
+    where
+  obj X := F.objPreimage X
+  map := @fun X Y f => F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
+  map_id X := by apply F.map_injective; aesop_cat
+  map_comp := @fun X Y Z f g => by apply F.map_injective; simp 
+-- #align
+--   category_theory.equivalence.equivalence_inverse CategoryTheory.Equivalence.equivalenceInverse
+/- Porting note: this is a private def in mathlib -/
+
+--
+/-- A functor which is full, faithful, and essentially surjective is an equivalence.
+
+See <https://stacks.math.columbia.edu/tag/02C3>.
+-/
+noncomputable def ofFullyFaithfullyEssSurj (F : C ⥤ D) [Full F] [Faithful F] [EssSurj F] :
+    IsEquivalence F :=
+  IsEquivalence.mk (equivalenceInverse F)
+    (NatIso.ofComponents (fun X => (F.preimageIso <| F.objObjPreimageIso <| F.obj X).symm)
+      @fun X Y f => by
+      apply F.map_injective
+      aesop_cat)
+    (NatIso.ofComponents F.objObjPreimageIso (by aesop_cat))
+#align
+  category_theory.equivalence.of_fully_faithfully_ess_surj CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj
+
+@[simp]
+theorem functor_map_inj_iff (e : C ≌ D) {X Y : C} (f g : X ⟶ Y) :
+    e.functor.map f = e.functor.map g ↔ f = g :=
+  ⟨fun h => e.functor.map_injective h, fun h => h ▸ rfl⟩
+#align
+  category_theory.equivalence.functor_map_inj_iff CategoryTheory.Equivalence.functor_map_inj_iff
+
+@[simp]
+theorem inverse_map_inj_iff (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) :
+    e.inverse.map f = e.inverse.map g ↔ f = g :=
+  functor_map_inj_iff e.symm f g
+#align
+  category_theory.equivalence.inverse_map_inj_iff CategoryTheory.Equivalence.inverse_map_inj_iff
+
+instance ess_surj_induced_functor {C' : Type _} (e : C' ≃ D) : EssSurj (inducedFunctor e)
+    where mem_essImage Y := 
+      ⟨e.symm Y, by simp only [inducedFunctor_obj,Equiv.apply_symm_apply]; exact ⟨default⟩⟩ 
+#align
+  category_theory.equivalence.ess_surj_induced_functor CategoryTheory.Equivalence.ess_surj_induced_functor
+
+noncomputable instance inducedFunctorOfEquiv {C' : Type _} (e : C' ≃ D) :
+    IsEquivalence (inducedFunctor e) :=
+  Equivalence.ofFullyFaithfullyEssSurj _
+#align
+  category_theory.equivalence.induced_functor_of_equiv CategoryTheory.Equivalence.inducedFunctorOfEquiv
+
+noncomputable instance fullyFaithfulToEssImage (F : C ⥤ D) [Full F] [Faithful F] :
+    IsEquivalence F.toEssImage :=
+  ofFullyFaithfullyEssSurj F.toEssImage
+#align
+  category_theory.equivalence.fully_faithful_to_ess_image CategoryTheory.Equivalence.fullyFaithfulToEssImage
+
+end Equivalence
+
+end CategoryTheory
+
diff --git a/Mathlib/CategoryTheory/Functor/Currying.lean b/Mathlib/CategoryTheory/Functor/Currying.lean
index 8c747e20a3e04..3eec08d7ff1f3 100644
--- a/Mathlib/CategoryTheory/Functor/Currying.lean
+++ b/Mathlib/CategoryTheory/Functor/Currying.lean
@@ -116,8 +116,8 @@ def uncurryObjFlip (F : C ⥤ D ⥤ E) : uncurry.obj F.flip ≅ Prod.swap _ _ 
 
 variable (B C D E)
 
-/-- A version of `CategoryTheory.whiskeringRight` for bifunctors, obtained by uncurrying,
-applying `whiskeringRight` and currying back
+/-- A version of `category_theory.whiskering_right` for bifunctors, obtained by uncurrying,
+applying `whiskering_right` and currying back
 -/
 @[simps!]
 def whiskeringRight₂ : (C ⥤ D ⥤ E) ⥤ (B ⥤ C) ⥤ (B ⥤ D) ⥤ B ⥤ E :=
diff --git a/Mathlib/CategoryTheory/Groupoid.lean b/Mathlib/CategoryTheory/Groupoid.lean
index 02333aed46bec..8ebf75d278f76 100644
--- a/Mathlib/CategoryTheory/Groupoid.lean
+++ b/Mathlib/CategoryTheory/Groupoid.lean
@@ -17,7 +17,7 @@ import Mathlib.Combinatorics.Quiver.ConnectedComponent
 /-!
 # Groupoids
 
-We define `Groupoid` as a typeclass extending `category`,
+We define `groupoid` as a typeclass extending `category`,
 asserting that all morphisms have inverses.
 
 The instance `IsIso.ofGroupoid (f : X ⟶ Y) : IsIso f` means that you can then write
@@ -40,7 +40,7 @@ namespace CategoryTheory
 universe v v₂ u u₂
 
 -- morphism levels before object levels. See note [CategoryTheory universes].
-/-- A `Groupoid` is a category such that all morphisms are isomorphisms. -/
+/-- A `groupoid` is a category such that all morphisms are isomorphisms. -/
 class Groupoid (obj : Type u) extends Category.{v} obj : Type max u (v + 1) where
   /-- The inverse morphism -/ 
   inv : ∀ {X Y : obj}, (X ⟶ Y) → (Y ⟶ X)
@@ -78,7 +78,7 @@ theorem Groupoid.inv_eq_inv (f : X ⟶ Y) : Groupoid.inv f = CategoryTheory.inv
   IsIso.eq_inv_of_hom_inv_id <| Groupoid.comp_inv f
 #align category_theory.groupoid.inv_eq_inv CategoryTheory.Groupoid.inv_eq_inv
 
-/-- `Groupoid.inv` is involutive. -/
+/-- `groupoid.inv` is involutive. -/
 @[simps]
 def Groupoid.invEquiv : (X ⟶ Y) ≃ (Y ⟶ X) :=
   ⟨Groupoid.inv, Groupoid.inv, fun f => by simp, fun f => by simp⟩
diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean
index acc0ac8f88af6..3c4a7a7de8990 100644
--- a/Mathlib/CategoryTheory/Iso.lean
+++ b/Mathlib/CategoryTheory/Iso.lean
@@ -142,7 +142,7 @@ def refl (X : C) : X ≅ X where
 
 instance : Inhabited (X ≅ X) := ⟨Iso.refl X⟩
 
-theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩
+theorem nonempty_iso_refl (X : C) : Nonempty (X ≅ X) := ⟨default⟩ 
 
 @[simp]
 theorem refl_symm (X : C) : (Iso.refl X).symm = Iso.refl X := rfl
@@ -159,9 +159,8 @@ def trans (α : X ≅ Y) (β : Y ≅ Z) : X ≅ Z where
 #align category_theory.iso.trans_hom CategoryTheory.Iso.trans_hom
 #align category_theory.iso.trans_inv CategoryTheory.Iso.trans_inv
 
-@[simps]
-instance : Trans (α := C) (· ≅ ·) (· ≅ ·) (· ≅ ·) where
-  trans := trans
+instance : Trans (· ≅ ·) (· ≅ ·) ((·:C) ≅ ·) where 
+  trans := trans 
 
 /-- Notation for composition of isomorphisms. -/
 infixr:80 " ≪≫ " => Iso.trans -- type as `\ll \gg`.
diff --git a/Mathlib/CategoryTheory/Limits/Cones.lean b/Mathlib/CategoryTheory/Limits/Cones.lean
index 158e8eb08eb8a..abf5a7c42648a 100644
--- a/Mathlib/CategoryTheory/Limits/Cones.lean
+++ b/Mathlib/CategoryTheory/Limits/Cones.lean
@@ -19,13 +19,13 @@ import Mathlib.CategoryTheory.Functor.ReflectsIso
 We define `Cone F`, a cone over a functor `F`,
 and `F.cones : Cᵒᵖ ⥤ Type`, the functor associating to `X` the cones over `F` with cone point `X`.
 
-A cone `c` is defined by specifying its cone point `c.pt` and a natural transformation `c.π`
-from the constant `c.pt` valued functor to `F`.
+A cone `c` is defined by specifying its cone point `c.X` and a natural transformation `c.π`
+from the constant `c.X` valued functor to `F`.
 
 We provide `c.w f : c.π.app j ≫ F.map f = c.π.app j'` for any `f : j ⟶ j'`
 as a wrapper for `c.π.naturality f` avoiding unneeded identity morphisms.
 
-We define `c.extend f`, where `c : cone F` and `f : Y ⟶ c.pt` for some other `Y`,
+We define `c.extend f`, where `c : cone F` and `f : Y ⟶ c.X` for some other `Y`,
 which replaces the cone point by `Y` and inserts `f` into each of the components of the cone.
 Similarly we have `c.whisker F` producing a `Cone (E ⋙ F)`
 
@@ -115,20 +115,20 @@ namespace Limits
 section
 
 /-- A `c : Cone F` is:
-* an object `c.pt` and
-* a natural transformation `c.π : c.pt ⟶ F` from the constant `c.pt` functor to `F`.
+* an object `c.X` and
+* a natural transformation `c.π : c.X ⟶ F` from the constant `c.X` functor to `F`.
 
 `Cone F` is equivalent, via `cone.equiv` below, to `Σ X, F.cones.obj X`.
 -/
 structure Cone (F : J ⥤ C) where
   /-- An object of `C` -/
-  pt : C
+  X : C
   /-- A natural transformation from the constant functor at `X` to `F` -/
-  π : (const J).obj pt ⟶ F
+  π : (const J).obj X ⟶ F
 #align category_theory.limits.cone CategoryTheory.Limits.Cone
 
 instance inhabitedCone (F : Discrete PUnit ⥤ C) : Inhabited (Cone F) :=
-  ⟨{  pt := F.obj ⟨⟨⟩⟩
+  ⟨{  X := F.obj ⟨⟨⟩⟩
       π := { app := fun ⟨⟨⟩⟩ => 𝟙 _ 
              naturality := by 
               intro X Y f
@@ -147,20 +147,20 @@ theorem Cone.w {F : J ⥤ C} (c : Cone F) {j j' : J} (f : j ⟶ j') :
 #align category_theory.limits.cone.w CategoryTheory.Limits.Cone.w
 
 /-- A `c : Cocone F` is
-* an object `c.pt` and
-* a natural transformation `c.ι : F ⟶ c.pt` from `F` to the constant `c.pt` functor.
+* an object `c.X` and
+* a natural transformation `c.ι : F ⟶ c.X` from `F` to the constant `c.X` functor.
 
 `Cocone F` is equivalent, via `cone.equiv` below, to `Σ X, F.cocones.obj X`.
 -/
 structure Cocone (F : J ⥤ C) where
   /-- An object of `C` -/
-  pt : C
+  X : C
   /-- A natural transformation from `F` to the constant functor at `X` -/
-  ι : F ⟶ (const J).obj pt
+  ι : F ⟶ (const J).obj X
 #align category_theory.limits.cocone CategoryTheory.Limits.Cocone
 
 instance inhabitedCocone (F : Discrete PUnit ⥤ C) : Inhabited (Cocone F) :=
-  ⟨{  pt := F.obj ⟨⟨⟩⟩
+  ⟨{  X := F.obj ⟨⟨⟩⟩
       ι := { app := fun ⟨⟨⟩⟩ => 𝟙 _  
              naturality := by 
               intro X Y f
@@ -188,9 +188,9 @@ namespace Cone
 @[simps!]
 def equiv (F : J ⥤ C) : Cone F ≅ ΣX, F.cones.obj X
     where
-  hom c := ⟨op c.pt, c.π⟩
+  hom c := ⟨op c.X, c.π⟩
   inv c :=
-    { pt := c.1.unop
+    { X := c.1.unop
       π := c.2 }
   hom_inv_id := by
     funext X
@@ -204,7 +204,7 @@ def equiv (F : J ⥤ C) : Cone F ≅ ΣX, F.cones.obj X
 
 /-- A map to the vertex of a cone naturally induces a cone by composition. -/
 @[simps]
-def extensions (c : Cone F) : yoneda.obj c.pt ⋙ uliftFunctor.{u₁} ⟶ F.cones where 
+def extensions (c : Cone F) : yoneda.obj c.X ⋙ uliftFunctor.{u₁} ⟶ F.cones where 
   app X f := (const J).map f.down ≫ c.π
   naturality := by 
     intros X Y f
@@ -215,8 +215,8 @@ def extensions (c : Cone F) : yoneda.obj c.pt ⋙ uliftFunctor.{u₁} ⟶ F.cone
 
 /-- A map to the vertex of a cone induces a cone by composition. -/
 @[simps]
-def extend (c : Cone F) {X : C} (f : X ⟶ c.pt) : Cone F :=
-  { pt := X 
+def extend (c : Cone F) {X : C} (f : X ⟶ c.X) : Cone F :=
+  { X := X 
     π := c.extensions.app (op X) ⟨f⟩ }
 #align category_theory.limits.cone.extend CategoryTheory.Limits.Cone.extend
 
@@ -224,7 +224,7 @@ def extend (c : Cone F) {X : C} (f : X ⟶ c.pt) : Cone F :=
 @[simps]
 def whisker (E : K ⥤ J) (c : Cone F) : Cone (E ⋙ F)
     where
-  pt := c.pt
+  X := c.X
   π := whiskerLeft E c.π
 #align category_theory.limits.cone.whisker CategoryTheory.Limits.Cone.whisker
 
@@ -235,9 +235,9 @@ namespace Cocone
 /-- The isomorphism between a cocone on `F` and an element of the functor `F.cocones`. -/
 def equiv (F : J ⥤ C) : Cocone F ≅ ΣX, F.cocones.obj X
     where
-  hom c := ⟨c.pt, c.ι⟩
+  hom c := ⟨c.X, c.ι⟩
   inv c :=
-    { pt := c.1
+    { X := c.1
       ι := c.2 }
   hom_inv_id := by
     funext X
@@ -251,7 +251,7 @@ def equiv (F : J ⥤ C) : Cocone F ≅ ΣX, F.cocones.obj X
 
 /-- A map from the vertex of a cocone naturally induces a cocone by composition. -/
 @[simps]
-def extensions (c : Cocone F) : coyoneda.obj (op c.pt) ⋙ uliftFunctor.{u₁} ⟶ F.cocones where 
+def extensions (c : Cocone F) : coyoneda.obj (op c.X) ⋙ uliftFunctor.{u₁} ⟶ F.cocones where 
   app X f := c.ι ≫ (const J).map f.down
   naturality := fun {X} {Y} f => by 
     dsimp [coyoneda,const]
@@ -261,8 +261,8 @@ def extensions (c : Cocone F) : coyoneda.obj (op c.pt) ⋙ uliftFunctor.{u₁} 
 
 /-- A map from the vertex of a cocone induces a cocone by composition. -/
 @[simps]
-def extend (c : Cocone F) {Y : C} (f : c.pt ⟶ Y) : Cocone F where 
-  pt := Y 
+def extend (c : Cocone F) {Y : C} (f : c.X ⟶ Y) : Cocone F where 
+  X := Y 
   ι := c.extensions.app Y ⟨f⟩
 #align category_theory.limits.cocone.extend CategoryTheory.Limits.Cocone.extend
 
@@ -272,7 +272,7 @@ version.
 @[simps]
 def whisker (E : K ⥤ J) (c : Cocone F) : Cocone (E ⋙ F)
     where
-  pt := c.pt
+  X := c.X
   ι := whiskerLeft E c.ι
 #align category_theory.limits.cocone.whisker CategoryTheory.Limits.Cocone.whisker
 
@@ -283,7 +283,7 @@ commutes with the cone legs. -/
 @[ext]
 structure ConeMorphism (A B : Cone F) where
   /-- A morphism between the two vertex objects of the cones -/
-  Hom : A.pt ⟶ B.pt
+  Hom : A.X ⟶ B.X
   /-- The triangle consisting of the two natural tranformations and `Hom` commutes -/
   w : ∀ j : J, Hom ≫ B.π.app j = A.π.app j := by aesop_cat
 #align category_theory.limits.cone_morphism CategoryTheory.Limits.ConeMorphism
@@ -300,7 +300,7 @@ instance inhabitedConeMorphism (A : Cone F) : Inhabited (ConeMorphism A A) :=
 instance Cone.category : Category (Cone F) where
   Hom A B := ConeMorphism A B
   comp f g := { Hom := f.Hom ≫ g.Hom }
-  id B := { Hom := 𝟙 B.pt }
+  id B := { Hom := 𝟙 B.X }
 #align category_theory.limits.cone.category CategoryTheory.Limits.Cone.category
 
 namespace Cones
@@ -310,7 +310,7 @@ namespace Cones
   maps. -/
 -- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule
 @[aesop apply safe (rule_sets [CategoryTheory]), simps]
-def ext {c c' : Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ j, c.π.app j = φ.hom ≫ c'.π.app j) : c ≅ c' where
+def ext {c c' : Cone F} (φ : c.X ≅ c'.X) (w : ∀ j, c.π.app j = φ.hom ≫ c'.π.app j) : c ≅ c' where
   hom := { Hom := φ.hom }
   inv :=
     { Hom := φ.inv
@@ -319,7 +319,7 @@ def ext {c c' : Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ j, c.π.app j = φ.hom 
 
 /-- Eta rule for cones. -/
 @[simps!]
-def eta (c : Cone F) : c ≅ ⟨c.pt, c.π⟩ :=
+def eta (c : Cone F) : c ≅ ⟨c.X, c.π⟩ :=
   Cones.ext (Iso.refl _) (by aesop_cat)
 #align category_theory.limits.cones.eta CategoryTheory.Limits.Cones.eta
 
@@ -338,7 +338,7 @@ Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to
 def postcompose {G : J ⥤ C} (α : F ⟶ G) : Cone F ⥤ Cone G
     where
   obj c :=
-    { pt := c.pt
+    { X := c.X
       π := c.π ≫ α }
   map f := { Hom := f.Hom }
 #align category_theory.limits.cones.postcompose CategoryTheory.Limits.Cones.postcompose
@@ -413,7 +413,7 @@ variable (F)
 /-- Forget the cone structure and obtain just the cone point. -/
 @[simps]
 def forget : Cone F ⥤ C where
-  obj t := t.pt
+  obj t := t.X
   map f := f.Hom
 #align category_theory.limits.cones.forget CategoryTheory.Limits.Cones.forget
 
@@ -423,7 +423,7 @@ variable (G : C ⥤ D)
 @[simps]
 def functoriality : Cone F ⥤ Cone (F ⋙ G) where
   obj A :=
-    { pt := G.obj A.pt
+    { X := G.obj A.X
       π :=
         { app := fun j => G.map (A.π.app j)
           naturality := by intros; erw [← G.map_comp]; aesop_cat } }
@@ -483,7 +483,7 @@ which commutes with the cocone legs. -/
 @[ext]
 structure CoconeMorphism (A B : Cocone F) where
   /-- A morphism between the (co)vertex objects in `C` -/
-  Hom : A.pt ⟶ B.pt
+  Hom : A.X ⟶ B.X
   /-- The triangle made from the two natural transformations and `Hom` commutes -/
   w : ∀ j : J, A.ι.app j ≫ Hom = B.ι.app j := by aesop_cat
 #align category_theory.limits.cocone_morphism CategoryTheory.Limits.CoconeMorphism
@@ -499,7 +499,7 @@ attribute [reassoc (attr := simp)] CoconeMorphism.w
 instance Cocone.category : Category (Cocone F) where
   Hom A B := CoconeMorphism A B
   comp f g := { Hom := f.Hom ≫ g.Hom }
-  id B := { Hom := 𝟙 B.pt }
+  id B := { Hom := 𝟙 B.X }
 #align category_theory.limits.cocone.category CategoryTheory.Limits.Cocone.category
 
 namespace Cocones
@@ -509,7 +509,7 @@ namespace Cocones
   maps. -/
 -- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule
 @[aesop apply safe (rule_sets [CategoryTheory]), simps]
-def ext {c c' : Cocone F} (φ : c.pt ≅ c'.pt) (w : ∀ j, c.ι.app j ≫ φ.hom = c'.ι.app j) 
+def ext {c c' : Cocone F} (φ : c.X ≅ c'.X) (w : ∀ j, c.ι.app j ≫ φ.hom = c'.ι.app j) 
     : c ≅ c' where
   hom := { Hom := φ.hom }
   inv :=
@@ -519,7 +519,7 @@ def ext {c c' : Cocone F} (φ : c.pt ≅ c'.pt) (w : ∀ j, c.ι.app j ≫ φ.ho
 
 /-- Eta rule for cocones. -/
 @[simps!]
-def eta (c : Cocone F) : c ≅ ⟨c.pt, c.ι⟩ :=
+def eta (c : Cocone F) : c ≅ ⟨c.X, c.ι⟩ :=
   Cocones.ext (Iso.refl _) (by aesop_cat)
 #align category_theory.limits.cocones.eta CategoryTheory.Limits.Cocones.eta
 
@@ -537,7 +537,7 @@ for `G`. -/
 @[simps]
 def precompose {G : J ⥤ C} (α : G ⟶ F) : Cocone F ⥤ Cocone G where
   obj c :=
-    { pt := c.pt
+    { X := c.X
       ι := α ≫ c.ι }
   map f := { Hom := f.Hom }
 #align category_theory.limits.cocones.precompose CategoryTheory.Limits.Cocones.precompose
@@ -613,7 +613,7 @@ variable (F)
 /-- Forget the cocone structure and obtain just the cocone point. -/
 @[simps]
 def forget : Cocone F ⥤ C where
-  obj t := t.pt
+  obj t := t.X
   map f := f.Hom
 #align category_theory.limits.cocones.forget CategoryTheory.Limits.Cocones.forget
 
@@ -623,7 +623,7 @@ variable (G : C ⥤ D)
 @[simps]
 def functoriality : Cocone F ⥤ Cocone (F ⋙ G) where
   obj A :=
-    { pt := G.obj A.pt
+    { X := G.obj A.X
       ι :=
         { app := fun j => G.map (A.ι.app j)
           naturality := by intros; erw [← G.map_comp]; aesop_cat } }
@@ -701,6 +701,7 @@ variable {F : J ⥤ C} {G : J ⥤ C} (H : C ⥤ D)
 
 open CategoryTheory.Limits
 
+/- Porting note: dot notation on the functor is broken for `mapCone` -/
 /-- The image of a cone in C under a functor G : C ⥤ D is a cone in D. -/
 @[simps!]
 def mapCone (c : Cone F) : Cone (F ⋙ H) :=
@@ -713,7 +714,6 @@ def mapCocone (c : Cocone F) : Cocone (F ⋙ H) :=
   (Cocones.functoriality F H).obj c
 #align category_theory.functor.map_cocone CategoryTheory.Functor.mapCocone
 
-/- Porting note: dot notation on the functor is broken for `mapCone` -/
 /-- Given a cone morphism `c ⟶ c'`, construct a cone morphism on the mapped cones functorially.  -/
 def mapConeMorphism {c c' : Cone F} (f : c ⟶ c') : mapCone H c ⟶ mapCone _ c' :=
   (Cones.functoriality F H).map f
@@ -866,14 +866,14 @@ variable {F : J ⥤ C}
 /-- Change a `Cocone F` into a `Cone F.op`. -/
 @[simps]
 def Cocone.op (c : Cocone F) : Cone F.op where
-  pt := Opposite.op c.pt
+  X := Opposite.op c.X
   π := NatTrans.op c.ι
 #align category_theory.limits.cocone.op CategoryTheory.Limits.Cocone.op
 
 /-- Change a `Cone F` into a `Cocone F.op`. -/
 @[simps]
 def Cone.op (c : Cone F) : Cocone F.op where
-  pt := Opposite.op c.pt
+  X := Opposite.op c.X
   ι := NatTrans.op c.π
 #align category_theory.limits.cone.op CategoryTheory.Limits.Cone.op
 
@@ -881,7 +881,7 @@ def Cone.op (c : Cone F) : Cocone F.op where
 @[simps]
 def Cocone.unop (c : Cocone F.op) : Cone F
     where
-  pt := Opposite.unop c.pt
+  X := Opposite.unop c.X
   π := NatTrans.removeOp c.ι
 #align category_theory.limits.cocone.unop CategoryTheory.Limits.Cocone.unop
 
@@ -889,7 +889,7 @@ def Cocone.unop (c : Cocone F.op) : Cone F
 @[simps]
 def Cone.unop (c : Cone F.op) : Cocone F
     where
-  pt := Opposite.unop c.pt
+  X := Opposite.unop c.X
   ι := NatTrans.removeOp c.π
 #align category_theory.limits.cone.unop CategoryTheory.Limits.Cone.unop
 
@@ -970,7 +970,7 @@ and replace with `@[simps]`-/
 @[simps!]
 def coneOfCoconeLeftOp (c : Cocone F.leftOp) : Cone F
     where
-  pt := op c.pt
+  X := op c.X
   π := NatTrans.removeLeftOp c.ι
 #align category_theory.limits.cone_of_cocone_left_op CategoryTheory.Limits.coneOfCoconeLeftOp
 
@@ -978,7 +978,7 @@ def coneOfCoconeLeftOp (c : Cocone F.leftOp) : Cone F
 @[simps!]
 def coconeLeftOpOfCone (c : Cone F) : Cocone F.leftOp
     where
-  pt := unop c.pt
+  X := unop c.X
   ι := NatTrans.leftOp c.π
 #align category_theory.limits.cocone_left_op_of_cone CategoryTheory.Limits.coconeLeftOpOfCone
 
@@ -986,10 +986,10 @@ def coconeLeftOpOfCone (c : Cone F) : Cocone F.leftOp
   reduce the RHS using `expr.dsimp` and `expr.simp`, but for some reason the expression is not
   being simplified properly. -/
 /-- Change a cone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/
-@[simps pt]
+@[simps X]
 def coconeOfConeLeftOp (c : Cone F.leftOp) : Cocone F
     where
-  pt := op c.pt
+  X := op c.X
   ι := NatTrans.removeLeftOp c.π
 #align category_theory.limits.cocone_of_cone_left_op CategoryTheory.Limits.coconeOfConeLeftOp
 
@@ -1004,7 +1004,7 @@ theorem coconeOfConeLeftOp_ι_app (c : Cone F.leftOp) (j) :
 @[simps!]
 def coneLeftOpOfCocone (c : Cocone F) : Cone F.leftOp
     where
-  pt := unop c.pt
+  X := unop c.X
   π := NatTrans.leftOp c.ι
 #align category_theory.limits.cone_left_op_of_cocone CategoryTheory.Limits.coneLeftOpOfCocone
 
@@ -1018,7 +1018,7 @@ variable {F : Jᵒᵖ ⥤ C}
 @[simps]
 def coneOfCoconeRightOp (c : Cocone F.rightOp) : Cone F
     where
-  pt := unop c.pt
+  X := unop c.X
   π := NatTrans.removeRightOp c.ι
 #align category_theory.limits.cone_of_cocone_right_op CategoryTheory.Limits.coneOfCoconeRightOp
 
@@ -1026,7 +1026,7 @@ def coneOfCoconeRightOp (c : Cocone F.rightOp) : Cone F
 @[simps]
 def coconeRightOpOfCone (c : Cone F) : Cocone F.rightOp
     where
-  pt := op c.pt
+  X := op c.X
   ι := NatTrans.rightOp c.π
 #align category_theory.limits.cocone_right_op_of_cone CategoryTheory.Limits.coconeRightOpOfCone
 
@@ -1034,7 +1034,7 @@ def coconeRightOpOfCone (c : Cone F) : Cocone F.rightOp
 @[simps]
 def coconeOfConeRightOp (c : Cone F.rightOp) : Cocone F
     where
-  pt := unop c.pt
+  X := unop c.X
   ι := NatTrans.removeRightOp c.π
 #align category_theory.limits.cocone_of_cone_right_op CategoryTheory.Limits.coconeOfConeRightOp
 
@@ -1042,7 +1042,7 @@ def coconeOfConeRightOp (c : Cone F.rightOp) : Cocone F
 @[simps]
 def coneRightOpOfCocone (c : Cocone F) : Cone F.rightOp
     where
-  pt := op c.pt
+  X := op c.X
   π := NatTrans.rightOp c.ι
 #align category_theory.limits.cone_right_op_of_cocone CategoryTheory.Limits.coneRightOpOfCocone
 
@@ -1056,7 +1056,7 @@ variable {F : Jᵒᵖ ⥤ Cᵒᵖ}
 @[simps]
 def coneOfCoconeUnop (c : Cocone F.unop) : Cone F
     where
-  pt := op c.pt
+  X := op c.X
   π := NatTrans.removeUnop c.ι
 #align category_theory.limits.cone_of_cocone_unop CategoryTheory.Limits.coneOfCoconeUnop
 
@@ -1064,7 +1064,7 @@ def coneOfCoconeUnop (c : Cocone F.unop) : Cone F
 @[simps]
 def coconeUnopOfCone (c : Cone F) : Cocone F.unop
     where
-  pt := unop c.pt
+  X := unop c.X
   ι := NatTrans.unop c.π
 #align category_theory.limits.cocone_unop_of_cone CategoryTheory.Limits.coconeUnopOfCone
 
@@ -1072,7 +1072,7 @@ def coconeUnopOfCone (c : Cone F) : Cocone F.unop
 @[simps]
 def coconeOfConeUnop (c : Cone F.unop) : Cocone F
     where
-  pt := op c.pt
+  X := op c.X
   ι := NatTrans.removeUnop c.π
 #align category_theory.limits.cocone_of_cone_unop CategoryTheory.Limits.coconeOfConeUnop
 
@@ -1080,7 +1080,7 @@ def coconeOfConeUnop (c : Cone F.unop) : Cocone F
 @[simps]
 def coneUnopOfCocone (c : Cocone F) : Cone F.unop
     where
-  pt := unop c.pt
+  X := unop c.X
   π := NatTrans.unop c.ι
 #align category_theory.limits.cone_unop_of_cocone CategoryTheory.Limits.coneUnopOfCocone
 
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
index bbca9360e49ce..7cb7a4bdef199 100644
--- a/Mathlib/CategoryTheory/Limits/HasLimits.lean
+++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -8,8 +8,8 @@ Authors: Reid Barton, Mario Carneiro, Scott Morrison, Floris van Doorn
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.CategoryTheory.Limits.IsLimit
-import Mathbin.CategoryTheory.Category.Ulift
+import Mathlib.CategoryTheory.Limits.IsLimit
+import Mathlib.CategoryTheory.Category.Ulift
 
 /-!
 # Existence of limits and colimits
@@ -245,16 +245,14 @@ def limit.isoLimitCone {F : J ⥤ C} [HasLimit F] (t : LimitCone F) : limit F 
 
 @[simp, reassoc.1]
 theorem limit.isoLimitCone_hom_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
-    (limit.isoLimitCone t).Hom ≫ t.Cone.π.app j = limit.π F j :=
-  by
+    (limit.isoLimitCone t).Hom ≫ t.Cone.π.app j = limit.π F j := by
   dsimp [limit.iso_limit_cone, is_limit.cone_point_unique_up_to_iso]
   tidy
 #align category_theory.limits.limit.iso_limit_cone_hom_π CategoryTheory.Limits.limit.isoLimitCone_hom_π
 
 @[simp, reassoc.1]
 theorem limit.isoLimitCone_inv_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
-    (limit.isoLimitCone t).inv ≫ limit.π F j = t.Cone.π.app j :=
-  by
+    (limit.isoLimitCone t).inv ≫ limit.π F j = t.Cone.π.app j := by
   dsimp [limit.iso_limit_cone, is_limit.cone_point_unique_up_to_iso]
   tidy
 #align category_theory.limits.limit.iso_limit_cone_inv_π CategoryTheory.Limits.limit.isoLimitCone_inv_π
@@ -267,8 +265,7 @@ theorem limit.hom_ext {F : J ⥤ C} [HasLimit F] {X : C} {f f' : X ⟶ limit F}
 
 @[simp]
 theorem limit.lift_map {F G : J ⥤ C} [HasLimit F] [HasLimit G] (c : Cone F) (α : F ⟶ G) :
-    limit.lift F c ≫ limMap α = limit.lift G ((Cones.postcompose α).obj c) :=
-  by
+    limit.lift F c ≫ limMap α = limit.lift G ((Cones.postcompose α).obj c) := by
   ext
   rw [assoc, lim_map_π, limit.lift_π_assoc, limit.lift_π]
   rfl
@@ -383,8 +380,7 @@ def HasLimit.isoOfEquivalence {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit
 theorem HasLimit.isoOfEquivalence_hom_π {F : J ⥤ C} [HasLimit F] {G : K ⥤ C} [HasLimit G]
     (e : J ≌ K) (w : e.Functor ⋙ G ≅ F) (k : K) :
     (HasLimit.isoOfEquivalence e w).Hom ≫ limit.π G k =
-      limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k) :=
-  by
+      limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k) := by
   simp only [has_limit.iso_of_equivalence, is_limit.cone_points_iso_of_equivalence_hom]
   dsimp
   simp
@@ -411,8 +407,7 @@ def limit.pre : limit F ⟶ limit (E ⋙ F) :=
 #align category_theory.limits.limit.pre CategoryTheory.Limits.limit.pre
 
 @[simp, reassoc.1]
-theorem limit.pre_π (k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k) :=
-  by
+theorem limit.pre_π (k : K) : limit.pre F E ≫ limit.π (E ⋙ F) k = limit.π F (E.obj k) := by
   erw [is_limit.fac]
   rfl
 #align category_theory.limits.limit.pre_π CategoryTheory.Limits.limit.pre_π
@@ -458,16 +453,14 @@ def limit.post : G.obj (limit F) ⟶ limit (F ⋙ G) :=
 #align category_theory.limits.limit.post CategoryTheory.Limits.limit.post
 
 @[simp, reassoc.1]
-theorem limit.post_π (j : J) : limit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j) :=
-  by
+theorem limit.post_π (j : J) : limit.post F G ≫ limit.π (F ⋙ G) j = G.map (limit.π F j) := by
   erw [is_limit.fac]
   rfl
 #align category_theory.limits.limit.post_π CategoryTheory.Limits.limit.post_π
 
 @[simp]
 theorem limit.lift_post (c : Cone F) :
-    G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (G.mapCone c) :=
-  by
+    G.map (limit.lift F c) ≫ limit.post F G = limit.lift (F ⋙ G) (G.mapCone c) := by
   ext
   rw [assoc, limit.post_π, ← G.map_comp, limit.lift_π, limit.lift_π]
   rfl
@@ -493,8 +486,7 @@ theorem limit.pre_post {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤
             G.map
           (limit.pre F E) ≫
         limit.post (E ⋙ F) G =
-      limit.post F G ≫ limit.pre (F ⋙ G) E :=
-  by
+      limit.post F G ≫ limit.pre (F ⋙ G) E := by
   ext <;> erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π] <;>
     rfl
 #align category_theory.limits.limit.pre_post CategoryTheory.Limits.limit.pre_post
@@ -512,8 +504,7 @@ attribute [local elab_without_expected_type] inv_fun_id_assoc
 -- not entirely sure why this is needed
 /-- If a `E ⋙ F` has a limit, and `E` is an equivalence, we can construct a limit of `F`.
 -/
-theorem hasLimitOfEquivalenceComp (e : K ≌ J) [HasLimit (e.Functor ⋙ F)] : HasLimit F :=
-  by
+theorem hasLimitOfEquivalenceComp (e : K ≌ J) [HasLimit (e.Functor ⋙ F)] : HasLimit F := by
   haveI : has_limit (e.inverse ⋙ e.functor ⋙ F) := limits.has_limit_equivalence_comp e.symm
   apply has_limit_of_iso (e.inv_fun_id_assoc F)
 #align category_theory.limits.has_limit_of_equivalence_comp CategoryTheory.Limits.hasLimitOfEquivalenceComp
@@ -549,8 +540,7 @@ theorem limMap_eq_limMap : lim.map α = limMap α :=
 #align category_theory.limits.lim_map_eq_lim_map CategoryTheory.Limits.limMap_eq_limMap
 
 theorem limit.map_pre [HasLimitsOfShape K C] (E : K ⥤ J) :
-    lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whiskerLeft E α) :=
-  by
+    lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whiskerLeft E α) := by
   ext
   simp
 #align category_theory.limits.limit.map_pre CategoryTheory.Limits.limit.map_pre
@@ -569,8 +559,7 @@ theorem limit.map_post {D : Type u'} [Category.{v'} D] [HasLimitsOfShape J D]
             H.map
           (limMap α) ≫
         limit.post G H =
-      limit.post F H ≫ limMap (whiskerRight α H) :=
-  by
+      limit.post F H ≫ limMap (whiskerRight α H) := by
   ext
   simp only [whisker_right_app, lim_map_π, assoc, limit.post_π_assoc, limit.post_π, ← H.map_comp]
 #align category_theory.limits.limit.map_post CategoryTheory.Limits.limit.map_post
@@ -626,8 +615,7 @@ instance limMap_mono {F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) [
 /-- We can transport limits of shape `J` along an equivalence `J ≌ J'`.
 -/
 theorem hasLimitsOfShapeOfEquivalence {J' : Type u₂} [Category.{v₂} J'] (e : J ≌ J')
-    [HasLimitsOfShape J C] : HasLimitsOfShape J' C :=
-  by
+    [HasLimitsOfShape J C] : HasLimitsOfShape J' C := by
   constructor
   intro F
   apply has_limit_of_equivalence_comp e
@@ -838,16 +826,14 @@ def colimit.isoColimitCocone {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F)
 
 @[simp, reassoc.1]
 theorem colimit.isoColimitCocone_ι_hom {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
-    colimit.ι F j ≫ (colimit.isoColimitCocone t).Hom = t.Cocone.ι.app j :=
-  by
+    colimit.ι F j ≫ (colimit.isoColimitCocone t).Hom = t.Cocone.ι.app j := by
   dsimp [colimit.iso_colimit_cocone, is_colimit.cocone_point_unique_up_to_iso]
   tidy
 #align category_theory.limits.colimit.iso_colimit_cocone_ι_hom CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom
 
 @[simp, reassoc.1]
 theorem colimit.isoColimitCocone_ι_inv {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
-    t.Cocone.ι.app j ≫ (colimit.isoColimitCocone t).inv = colimit.ι F j :=
-  by
+    t.Cocone.ι.app j ≫ (colimit.isoColimitCocone t).inv = colimit.ι F j := by
   dsimp [colimit.iso_colimit_cocone, is_colimit.cocone_point_unique_up_to_iso]
   tidy
 #align category_theory.limits.colimit.iso_colimit_cocone_ι_inv CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv
@@ -968,8 +954,7 @@ def HasColimit.isoOfEquivalence {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasC
 theorem HasColimit.isoOfEquivalence_hom_π {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G]
     (e : J ≌ K) (w : e.Functor ⋙ G ≅ F) (j : J) :
     colimit.ι F j ≫ (HasColimit.isoOfEquivalence e w).Hom =
-      F.map (e.Unit.app j) ≫ w.inv.app _ ≫ colimit.ι G _ :=
-  by
+      F.map (e.Unit.app j) ≫ w.inv.app _ ≫ colimit.ι G _ := by
   simp [has_colimit.iso_of_equivalence, is_colimit.cocone_points_iso_of_equivalence_inv]
   dsimp
   simp
@@ -979,8 +964,7 @@ theorem HasColimit.isoOfEquivalence_hom_π {F : J ⥤ C} [HasColimit F] {G : K 
 theorem HasColimit.isoOfEquivalence_inv_π {F : J ⥤ C} [HasColimit F] {G : K ⥤ C} [HasColimit G]
     (e : J ≌ K) (w : e.Functor ⋙ G ≅ F) (k : K) :
     colimit.ι G k ≫ (HasColimit.isoOfEquivalence e w).inv =
-      G.map (e.counitInv.app k) ≫ w.Hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k) :=
-  by
+      G.map (e.counitInv.app k) ≫ w.Hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k) := by
   simp [has_colimit.iso_of_equivalence, is_colimit.cocone_points_iso_of_equivalence_inv]
   dsimp
   simp
@@ -997,8 +981,7 @@ def colimit.pre : colimit (E ⋙ F) ⟶ colimit F :=
 #align category_theory.limits.colimit.pre CategoryTheory.Limits.colimit.pre
 
 @[simp, reassoc.1]
-theorem colimit.ι_pre (k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) :=
-  by
+theorem colimit.ι_pre (k : K) : colimit.ι (E ⋙ F) k ≫ colimit.pre F E = colimit.ι F (E.obj k) := by
   erw [is_colimit.fac]
   rfl
 #align category_theory.limits.colimit.ι_pre CategoryTheory.Limits.colimit.ι_pre
@@ -1014,8 +997,7 @@ variable {L : Type u₃} [Category.{v₃} L]
 variable (D : L ⥤ K) [HasColimit (D ⋙ E ⋙ F)]
 
 @[simp]
-theorem colimit.pre_pre : colimit.pre (E ⋙ F) D ≫ colimit.pre F E = colimit.pre F (D ⋙ E) :=
-  by
+theorem colimit.pre_pre : colimit.pre (E ⋙ F) D ≫ colimit.pre F E = colimit.pre F (D ⋙ E) := by
   ext j
   rw [← assoc, colimit.ι_pre, colimit.ι_pre]
   letI : has_colimit ((D ⋙ E) ⋙ F) := show has_colimit (D ⋙ E ⋙ F) by infer_instance
@@ -1059,8 +1041,7 @@ theorem colimit.ι_post (j : J) : colimit.ι (F ⋙ G) j ≫ colimit.post F G =
 
 @[simp]
 theorem colimit.post_desc (c : Cocone F) :
-    colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.mapCocone c) :=
-  by
+    colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.mapCocone c) := by
   ext
   rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_desc, colimit.ι_desc]
   rfl
@@ -1074,8 +1055,7 @@ theorem colimit.post_post {E : Type u''} [Category.{v''} E] (H : D ⥤ E)
           colimit.post
           (F ⋙ G) H ≫
         H.map (colimit.post F G) =
-      colimit.post F (G ⋙ H) :=
-  by
+      colimit.post F (G ⋙ H) := by
   ext
   rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]
   exact (colimit.ι_post F (G ⋙ H) j).symm
@@ -1091,8 +1071,7 @@ theorem colimit.pre_post {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J 
           colimit.post
           (E ⋙ F) G ≫
         G.map (colimit.pre F E) =
-      (@colimit.pre _ _ _ (F ⋙ G) _ E H ≫ colimit.post F G : _) :=
-  by
+      (@colimit.pre _ _ _ (F ⋙ G) _ E H ≫ colimit.post F G : _) := by
   ext
   rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_pre, ← assoc]
   letI : has_colimit (E ⋙ F ⋙ G) := show has_colimit ((E ⋙ F) ⋙ G) by infer_instance
@@ -1109,8 +1088,7 @@ instance hasColimitEquivalenceComp (e : K ≌ J) [HasColimit F] : HasColimit (e.
 
 /-- If a `E ⋙ F` has a colimit, and `E` is an equivalence, we can construct a colimit of `F`.
 -/
-theorem hasColimitOfEquivalenceComp (e : K ≌ J) [HasColimit (e.Functor ⋙ F)] : HasColimit F :=
-  by
+theorem hasColimitOfEquivalenceComp (e : K ≌ J) [HasColimit (e.Functor ⋙ F)] : HasColimit F := by
   haveI : has_colimit (e.inverse ⋙ e.functor ⋙ F) := limits.has_colimit_equivalence_comp e.symm
   apply has_colimit_of_iso (e.inv_fun_id_assoc F).symm
 #align category_theory.limits.has_colimit_of_equivalence_comp CategoryTheory.Limits.hasColimitOfEquivalenceComp
@@ -1174,8 +1152,7 @@ theorem colimit.map_post {D : Type u'} [Category.{v'} D] [HasColimitsOfShape J D
           colimit.post
           F H ≫
         H.map (colim.map α) =
-      colim.map (whiskerRight α H) ≫ colimit.post G H :=
-  by
+      colim.map (whiskerRight α H) ≫ colimit.post G H := by
   ext
   rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]
   rw [← assoc, colimit.ι_map, assoc, colimit.ι_post]
@@ -1235,8 +1212,7 @@ instance colimMap_epi {F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶
 /-- We can transport colimits of shape `J` along an equivalence `J ≌ J'`.
 -/
 theorem hasColimitsOfShapeOfEquivalence {J' : Type u₂} [Category.{v₂} J'] (e : J ≌ J')
-    [HasColimitsOfShape J C] : HasColimitsOfShape J' C :=
-  by
+    [HasColimitsOfShape J C] : HasColimitsOfShape J' C := by
   constructor
   intro F
   apply has_colimit_of_equivalence_comp e
diff --git a/Mathlib/CategoryTheory/Limits/IsLimit.lean b/Mathlib/CategoryTheory/Limits/IsLimit.lean
new file mode 100644
index 0000000000000..5d82793cc1c73
--- /dev/null
+++ b/Mathlib/CategoryTheory/Limits/IsLimit.lean
@@ -0,0 +1,1084 @@
+/-
+Copyright (c) 2018 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton, Mario Carneiro, Scott Morrison, Floris van Doorn
+
+! This file was ported from Lean 3 source module category_theory.limits.is_limit
+! leanprover-community/mathlib commit 740acc0e6f9adf4423f92a485d0456fc271482da
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.CategoryTheory.Adjunction.Basic
+import Mathlib.CategoryTheory.Limits.Cones
+
+/-!
+# Limits and colimits
+
+We set up the general theory of limits and colimits in a category.
+In this introduction we only describe the setup for limits;
+it is repeated, with slightly different names, for colimits.
+
+The main structures defined in this file is
+* `IsLimit c`, for `c : Cone F`, `F : J ⥤ C`, expressing that `c` is a limit cone,
+
+See also `CategoryTheory.Limits.HasLimits` which further builds:
+* `LimitCone F`, which consists of a choice of cone for `F` and the fact it is a limit cone, and
+* `HasLimit F`, asserting the mere existence of some limit cone for `F`.
+
+## Implementation
+At present we simply say everything twice, in order to handle both limits and colimits.
+It would be highly desirable to have some automation support,
+e.g. a `@[dualize]` attribute that behaves similarly to `@[to_additive]`.
+
+## References
+* [Stacks: Limits and colimits](https://stacks.math.columbia.edu/tag/002D)
+
+-/
+
+
+noncomputable section
+
+open CategoryTheory CategoryTheory.Category CategoryTheory.Functor Opposite
+
+namespace CategoryTheory.Limits
+
+-- declare the `v`'s first; see `CategoryTheory.Category` for an explanation
+universe v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
+
+variable {J : Type u₁} [Category.{v₁} J] {K : Type u₂} [Category.{v₂} K]
+
+variable {C : Type u₃} [Category.{v₃} C]
+
+variable {F : J ⥤ C}
+
+/-- A cone `t` on `F` is a limit cone if each cone on `F` admits a unique
+cone morphism to `t`.
+
+See <https://stacks.math.columbia.edu/tag/002E>.
+  -/
+-- Porting note: removed @[nolint has_nonempty_instance]
+structure IsLimit (t : Cone F) where
+  /-- There is a morphism from any cone vertex to `t.X` -/
+  lift : ∀ s : Cone F, s.X ⟶ t.X
+  /-- The map makes the triangle with the two natural transformations commute -/
+  fac : ∀ (s : Cone F) (j : J), lift s ≫ t.π.app j = s.π.app j := by aesop_cat
+  /-- It is the unique such map to do this -/
+  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
+
+-- Porting note: linter claimed it reduced but it did not
+attribute [nolint simpNF] IsLimit.mk.injEq
+
+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 ; 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 :=
+  P.lift ((Cones.postcompose α).obj s)
+#align category_theory.limits.is_limit.map CategoryTheory.Limits.IsLimit.map
+
+@[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 _ => id_comp _).symm
+#align category_theory.limits.is_limit.lift_self CategoryTheory.Limits.IsLimit.lift_self
+
+-- Repackaging the definition in terms of cone morphisms.
+/-- The universal morphism from any other cone to a limit cone. -/
+@[simps]
+def liftConeMorphism {t : Cone F} (h : IsLimit t) (s : Cone F) : s ⟶ t where Hom := h.lift s
+#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; 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 :=
+  ⟨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
+  choose s hs hs' using ht
+  exact ⟨s, hs, hs'⟩
+#align category_theory.limits.is_limit.of_exists_unique CategoryTheory.Limits.IsLimit.ofExistsUnique
+
+/-- Alternative constructor for `isLimit`,
+providing a morphism of cones rather than a morphism between the cone points
+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
+    where
+  lift s := (lift s).Hom
+  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
+  inv := P.liftConeMorphism t
+  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. -/
+theorem hom_isIso {s t : Cone F} (P : IsLimit s) (Q : IsLimit t) (f : s ⟶ t) : IsIso f :=
+  ⟨⟨P.liftConeMorphism t, ⟨P.uniq_cone_morphism, Q.uniq_cone_morphism⟩⟩⟩
+#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 :=
+  (Cones.forget F).mapIso (uniqueUpToIso P Q)
+#align category_theory.limits.is_limit.cone_point_unique_up_to_iso CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso
+
+@[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 _
+#align category_theory.limits.is_limit.cone_point_unique_up_to_iso_hom_comp CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
+
+@[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
+
+@[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 :=
+  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
+
+@[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)
+#align category_theory.limits.is_limit.lift_comp_cone_point_unique_up_to_iso_inv CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_inv
+
+/-- 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
+#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 :=
+  rfl
+#align category_theory.limits.is_limit.of_iso_limit_lift CategoryTheory.Limits.IsLimit.ofIsoLimit_lift
+
+/-- Isomorphism of cones preserves whether or not they are limiting cones. -/
+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 aesop_cat
+  right_inv := by aesop_cat
+#align category_theory.limits.is_limit.equiv_iso_limit CategoryTheory.Limits.IsLimit.equivIsoLimit
+
+@[simp]
+theorem equivIsoLimit_apply {r t : Cone F} (i : r ≅ t) (P : IsLimit r) :
+    equivIsoLimit i P = P.ofIsoLimit i :=
+  rfl
+#align category_theory.limits.is_limit.equiv_iso_limit_apply CategoryTheory.Limits.IsLimit.equivIsoLimit_apply
+
+@[simp]
+theorem equivIsoLimit_symm_apply {r t : Cone F} (i : r ≅ t) (P : IsLimit t) :
+    (equivIsoLimit i).symm P = P.ofIsoLimit i.symm :=
+  rfl
+#align category_theory.limits.is_limit.equiv_iso_limit_symm_apply CategoryTheory.Limits.IsLimit.equivIsoLimit_symm_apply
+
+/-- If the canonical morphism from a cone point to a limiting cone point is an iso, then the
+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 : IsIso (P.liftConeMorphism t).Hom := i
+      haveI : IsIso (P.liftConeMorphism t) := Cones.cone_iso_of_hom_iso _
+      symm
+      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) :
+    m =
+      h.lift
+        { X := W
+          π := { app := fun b => m ≫ t.π.app b } } :=
+  h.uniq
+    { 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
+#align category_theory.limits.is_limit.hom_ext CategoryTheory.Limits.IsLimit.hom_ext
+
+/-- Given a right adjoint functor between categories of cones,
+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 _ _ => (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
+    where
+  toFun P := ofIsoLimit (ofRightAdjoint h.inverse P) (h.unitIso.symm.app c)
+  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) :
+    (ofConeEquiv h P).lift s =
+      ((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
+
+@[simp]
+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 :=
+  rfl
+#align category_theory.limits.is_limit.of_cone_equiv_symm_apply_desc CategoryTheory.Limits.IsLimit.ofConeEquiv_symm_apply_desc
+
+/--
+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 :=
+  ofConeEquiv (Cones.postcomposeEquivalence α)
+#align category_theory.limits.is_limit.postcompose_hom_equiv CategoryTheory.Limits.IsLimit.postcomposeHomEquiv
+
+/-- A cone postcomposed with the inverse of a natural isomorphism is a limit cone if and only if
+the original cone is.
+-/
+def postcomposeInvEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cone G) :
+    IsLimit ((Cones.postcompose α.inv).obj c) ≃ IsLimit c :=
+  postcomposeHomEquiv α.symm c
+#align category_theory.limits.is_limit.postcompose_inv_equiv CategoryTheory.Limits.IsLimit.postcomposeInvEquiv
+
+/-- Constructing an equivalence `IsLimit c ≃ IsLimit d` from a natural isomorphism
+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 :=
+  (postcomposeHomEquiv α _).symm.trans (equivIsoLimit w)
+#align category_theory.limits.is_limit.equiv_of_nat_iso_of_iso CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
+
+/-- The cone points of two limit cones for naturally isomorphic functors
+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
+  inv := P.map t w.inv
+  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]
+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
+#align category_theory.limits.is_limit.cone_points_iso_of_nat_iso_hom_comp CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_hom_comp
+
+@[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]
+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 :=
+  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]
+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 :=
+  P.hom_ext (by simp)
+#align category_theory.limits.is_limit.lift_comp_cone_points_iso_of_nat_iso_inv CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv
+
+section Equivalence
+
+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
+#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 :=
+  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 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
+* both cones are limit cones
+* their indexing categories are equivalent via some `e : J ≌ K`,
+* the triangle of functors commutes up to a natural isomorphism: `e.functor ⋙ G ≅ F`.
+
+This is the most general form of uniqueness of cone points,
+allowing relabelling of both the indexing category (up to equivalence)
+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 :=
+  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
+      apply hom_ext P; intro j
+      dsimp
+      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
+      apply hom_ext Q
+      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).π
+  inv π :=
+    ⟨h.lift
+        { X := W
+          π }⟩
+  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).π :=
+  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 := 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 `homIso`.
+-/
+def homIso' (h : IsLimit t) (W : C) :
+    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 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 } }
+#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 (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
+      apply G.map_injective; rw [h]
+      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
+
+/-- If `F` and `G` are naturally isomorphic, then `F.mapCone c` being a limit implies
+`G.mapCone 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 (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 :=
+    { default := h.liftConeMorphism s
+      uniq := fun _ => h.uniq_cone_morphism }
+  inv h :=
+    { lift := fun s => (h s).default.Hom
+      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
+
+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⟩
+#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
+#align category_theory.limits.is_limit.of_nat_iso.hom_of_cone CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone
+
+@[simp]
+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_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. -/
+def limitCone : Cone F :=
+  coneOfHom h (𝟙 X)
+#align category_theory.limits.is_limit.of_nat_iso.limit_cone CategoryTheory.Limits.IsLimit.OfNatIso.limitCone
+
+/-- 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 [coneOfHom, limitCone, Cone.extend]
+  congr with j
+  have t := congrFun (h.hom.naturality f.op) ⟨𝟙 X⟩
+  dsimp at t
+  simp only [comp_id] at t
+  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 [← 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
+
+section
+
+open OfNatIso
+
+/-- If `F.cones` is representable, then the cone corresponding to the identity morphism on
+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
+    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 [← homOfCone_coneOfHom h m]
+    congr
+    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
+
+end IsLimit
+
+/-- A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique
+cocone morphism from `t`.
+
+See <https://stacks.math.columbia.edu/tag/002F>.
+-/
+-- Porting note: remove @[nolint has_nonempty_instance]
+structure IsColimit (t : Cocone F) where
+  /-- `t.X` maps to all other cocone covertices -/
+  desc : ∀ s : Cocone F, t.X ⟶ s.X
+  /-- The map `desc` makes the diagram with the natural transformations commute -/
+  fac : ∀ (s : Cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j := by aesop_cat
+  /-- `desc` is the unique such map -/
+  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
+
+attribute [reassoc (attr := simp)] IsColimit.fac
+
+-- Porting note: linter claimed it reduced but it did not
+attribute [nolint simpNF] IsColimit.mk.injEq
+
+namespace IsColimit
+
+instance subsingleton {t : Cocone F} : Subsingleton (IsColimit t) :=
+  ⟨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 :=
+  P.desc ((Cocones.precompose α).obj t)
+#align category_theory.limits.is_colimit.map CategoryTheory.Limits.IsColimit.map
+
+@[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 _ => comp_id _).symm
+#align category_theory.limits.is_colimit.desc_self CategoryTheory.Limits.IsColimit.desc_self
+
+-- Repackaging the definition in terms of cocone morphisms.
+/-- The universal morphism from a colimit cocone to any other cocone. -/
+@[simps]
+def descCoconeMorphism {t : Cocone F} (h : IsColimit t) (s : Cocone F) : t ⟶ s where Hom := h.desc 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; 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 :=
+  ⟨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
+  choose s hs hs' using ht
+  exact ⟨s, hs, hs'⟩
+#align category_theory.limits.is_colimit.of_exists_unique CategoryTheory.Limits.IsColimit.ofExistsUnique
+
+/-- Alternative constructor for `IsColimit`,
+providing a morphism of cocones rather than a morphism between the cocone points
+and separately the factorisation condition.
+-/
+@[simps]
+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 :=
+    have : CoconeMorphism.mk m w = desc s := by apply uniq'
+    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
+  inv := Q.descCoconeMorphism s
+  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. -/
+theorem hom_isIso {s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) (f : s ⟶ t) : IsIso f :=
+  ⟨⟨Q.descCoconeMorphism s, ⟨P.uniq_cocone_morphism, Q.uniq_cocone_morphism⟩⟩⟩
+#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 :=
+  (Cocones.forget F).mapIso (uniqueUpToIso P Q)
+#align category_theory.limits.is_colimit.cocone_point_unique_up_to_iso CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
+
+@[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 _
+#align category_theory.limits.is_colimit.comp_cocone_point_unique_up_to_iso_hom CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
+
+@[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
+
+@[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 :=
+  P.uniq _ _ (by simp)
+#align category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_hom_desc CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_hom_desc
+
+@[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)
+#align category_theory.limits.is_colimit.cocone_point_unique_up_to_iso_inv_desc CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso_inv_desc
+
+/-- 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
+#align category_theory.limits.is_colimit.of_iso_colimit CategoryTheory.Limits.IsColimit.ofIsoColimit
+
+@[simp]
+theorem ofIsoColimit_desc {r t : Cocone F} (P : IsColimit r) (i : r ≅ t) (s) :
+    (P.ofIsoColimit i).desc s = i.inv.Hom ≫ P.desc s :=
+  rfl
+#align category_theory.limits.is_colimit.of_iso_colimit_desc CategoryTheory.Limits.IsColimit.ofIsoColimit_desc
+
+/-- Isomorphism of cocones preserves whether or not they are colimiting cocones. -/
+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 aesop_cat
+  right_inv := by aesop_cat
+#align category_theory.limits.is_colimit.equiv_iso_colimit CategoryTheory.Limits.IsColimit.equivIsoColimit
+
+@[simp]
+theorem equivIsoColimit_apply {r t : Cocone F} (i : r ≅ t) (P : IsColimit r) :
+    equivIsoColimit i P = P.ofIsoColimit i :=
+  rfl
+#align category_theory.limits.is_colimit.equiv_iso_colimit_apply CategoryTheory.Limits.IsColimit.equivIsoColimit_apply
+
+@[simp]
+theorem equivIsoColimit_symm_apply {r t : Cocone F} (i : r ≅ t) (P : IsColimit t) :
+    (equivIsoColimit i).symm P = P.ofIsoColimit i.symm :=
+  rfl
+#align category_theory.limits.is_colimit.equiv_iso_colimit_symm_apply CategoryTheory.Limits.IsColimit.equivIsoColimit_symm_apply
+
+/-- If the canonical morphism to a cocone point from a colimiting cocone point is an iso, then the
+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 : 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) :
+    m =
+      h.desc
+        { X := W
+          ι :=
+            { app := fun b => t.ι.app b ≫ m
+              naturality := by intros; erw [← assoc, t.ι.naturality, comp_id, comp_id] } } :=
+  h.uniq
+    { X := W
+      ι :=
+        { app := fun b => t.ι.app b ≫ m
+          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}
+    (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
+#align category_theory.limits.is_colimit.hom_ext CategoryTheory.Limits.IsColimit.hom_ext
+
+/-- Given a left adjoint functor between categories of cocones,
+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 _ _ =>
+    (Adjunction.homEquiv_apply_eq _ _ _).1 t.uniq_cocone_morphism
+#align category_theory.limits.is_colimit.of_left_adjoint CategoryTheory.Limits.IsColimit.ofLeftAdjoint
+
+/-- Given two functors which have equivalent categories of cocones,
+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
+    where
+  toFun P := ofIsoColimit (ofLeftAdjoint h.inverse P) (h.unitIso.symm.app c)
+  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) :
+    (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 :=
+  rfl
+#align category_theory.limits.is_colimit.of_cocone_equiv_apply_desc CategoryTheory.Limits.IsColimit.ofCoconeEquiv_apply_desc
+
+@[simp]
+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 :=
+  rfl
+#align category_theory.limits.is_colimit.of_cocone_equiv_symm_apply_desc CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc
+
+/-- A cocone precomposed with a natural isomorphism is a colimit cocone
+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 :=
+  ofCoconeEquiv (Cocones.precomposeEquivalence α)
+#align category_theory.limits.is_colimit.precompose_hom_equiv CategoryTheory.Limits.IsColimit.precomposeHomEquiv
+
+/-- A cocone precomposed with the inverse of a natural isomorphism is a colimit cocone
+if and only if the original cocone is.
+-/
+def precomposeInvEquiv {F G : J ⥤ C} (α : F ≅ G) (c : Cocone F) :
+    IsColimit ((Cocones.precompose α.inv).obj c) ≃ IsColimit c :=
+  precomposeHomEquiv α.symm c
+#align category_theory.limits.is_colimit.precompose_inv_equiv CategoryTheory.Limits.IsColimit.precomposeInvEquiv
+
+/-- Constructing an equivalence `is_colimit c ≃ is_colimit d` from a natural isomorphism
+between the underlying functors, and then an isomorphism between `c` transported along this and `d`.
+-/
+def equivOfNatIsoOfIso {F G : J ⥤ C} (α : F ≅ G) (c : Cocone F) (d : Cocone G)
+    (w : (Cocones.precompose α.inv).obj c ≅ d) : IsColimit c ≃ IsColimit d :=
+  (precomposeInvEquiv α _).symm.trans (equivIsoColimit w)
+#align category_theory.limits.is_colimit.equiv_of_nat_iso_of_iso CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso
+
+/-- The cocone points of two colimit cocones for naturally isomorphic functors
+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
+    where
+  hom := P.map t w.hom
+  inv := Q.map s w.inv
+  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]
+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
+#align category_theory.limits.is_colimit.comp_cocone_points_iso_of_nat_iso_hom CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom
+
+@[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]
+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 :=
+  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]
+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 :=
+  Q.hom_ext (by simp)
+#align category_theory.limits.is_colimit.cocone_points_iso_of_nat_iso_inv_desc CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc
+
+section Equivalence
+
+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
+#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)) :
+    IsColimit s :=
+  equivIsoColimit ((Cocones.whiskeringEquivalence e).unitIso.app s).symm
+    (ofLeftAdjoint (Cocones.whiskeringEquivalence e).inverse P : _)
+#align category_theory.limits.is_colimit.of_whisker_equivalence CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence
+
+/-- 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 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
+* both cocones are colimit cocones
+* their indexing categories are equivalent via some `e : J ≌ K`,
+* the triangle of functors commutes up to a natural isomorphism: `e.functor ⋙ G ≅ F`.
+
+This is the most general form of uniqueness of cocone points,
+allowing relabelling of both the indexing category (up to equivalence)
+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 :=
+  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
+      apply hom_ext P; intro j
+      dsimp
+      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
+      apply hom_ext Q
+      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).ι
+  inv ι :=
+    ⟨h.desc
+        { X := W
+          ι }⟩
+  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).ι :=
+  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; 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 `homIso`.
+-/
+def homIso' (h : IsColimit t) (W : C) :
+    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⟩
+      inv := fun p =>
+        { app := fun j => p.1 j
+          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 (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
+      apply G.map_injective; rw [h]
+      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
+
+/-- If `F` and `G` are naturally isomorphic, then `F.mapCocone c` being a colimit implies
+`G.mapCocone 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 (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 :=
+    { default := h.descCoconeMorphism s
+      uniq := fun _ => h.uniq_cocone_morphism }
+  inv h :=
+    { desc := fun s => (h s).default.Hom
+      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
+
+variable {X : C} (h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁} ≅ F.cocones)
+
+/-- If `F.cocones` is corepresented by `X`, each morphism `f : X ⟶ Y` gives a cocone with cone
+point `Y`. -/
+def coconeOfHom {Y : C} (f : X ⟶ Y) : Cocone F
+    where
+  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
+#align category_theory.limits.is_colimit.of_nat_iso.hom_of_cocone CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone
+
+@[simp]
+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_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. -/
+def colimitCocone : Cocone F :=
+  coconeOfHom h (𝟙 X)
+#align category_theory.limits.is_colimit.of_nat_iso.colimit_cocone CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone
+
+/-- 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 [coconeOfHom, colimitCocone, Cocone.extend]
+  congr with j
+  have t := congrFun (h.hom.naturality f) ⟨𝟙 X⟩
+  dsimp at t
+  simp only [id_comp] at t
+  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 [← 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
+
+section
+
+open OfNatIso
+
+/-- If `F.cocones` is corepresentable, then the cocone corresponding to the identity morphism on
+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
+    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 [← homOfCocone_cooneOfHom h m]
+    congr
+    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
+
+end IsColimit
+
+end CategoryTheory.Limits
+
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean b/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
index ef32f913c8954..a71d94949664b 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
@@ -26,7 +26,7 @@ Besides the definition, we show that
 * if `f ≫ g` is a strong epimorphism, then so is `g`,
 * if `f` is both a strong epimorphism and a monomorphism, then it is an isomorphism
 
-We also define classes `StrongMonoCategory` and `StrongEpiCategory` for categories in which
+We also define classes `strong_mono_category` and `strong_epi_category` for categories in which
 every monomorphism or epimorphism is strong, and deduce that these categories are balanced.
 
 ## TODO
@@ -59,11 +59,11 @@ class StrongEpi (f : P ⟶ Q) : Prop where
 
 
 theorem StrongEpi.mk' {f : P ⟶ Q} [Epi f]
-    (hf : ∀ (X Y : C) (z : X ⟶ Y)
+    (hf : ∀ (X Y : C) (z : X ⟶ Y) 
       (_ : Mono z) (u : P ⟶ X) (v : Q ⟶ Y) (sq : CommSq u f z v), sq.HasLift) :
     StrongEpi f :=
   { epi := inferInstance
-    llp := fun {X Y} z hz => ⟨fun {u v} sq => hf X Y z hz u v sq⟩ }
+    llp := fun {X} {Y} z hz => ⟨fun {u} {v} sq => hf X Y z hz u v sq⟩ }
 #align category_theory.strong_epi.mk' CategoryTheory.StrongEpi.mk'
 
 /-- A strong monomorphism `f` is a monomorphism which has the right lifting property
@@ -76,10 +76,10 @@ class StrongMono (f : P ⟶ Q) : Prop where
 #align category_theory.strong_mono CategoryTheory.StrongMono
 
 theorem StrongMono.mk' {f : P ⟶ Q} [Mono f]
-    (hf : ∀ (X Y : C) (z : X ⟶ Y) (_ : Epi z) (u : X ⟶ P)
-      (v : Y ⟶ Q) (sq : CommSq u z f v), sq.HasLift) : StrongMono f where
+    (hf : ∀ (X Y : C) (z : X ⟶ Y) (_ : Epi z) (u : X ⟶ P) 
+    (v : Y ⟶ Q) (sq : CommSq u z f v), sq.HasLift) : StrongMono f where
   mono := inferInstance
-  rlp := fun {X Y} z hz => ⟨fun {u v} sq => hf X Y z hz u v sq⟩
+  rlp := fun {X} {Y} z hz => ⟨fun {u} {v} sq => hf X Y z hz u v sq⟩
 #align category_theory.strong_mono.mk' CategoryTheory.StrongMono.mk'
 
 attribute [instance] StrongEpi.llp
@@ -117,7 +117,7 @@ theorem strongMono_comp [StrongMono f] [StrongMono g] : StrongMono (f ≫ g) :=
 /-- If `f ≫ g` is a strong epimorphism, then so is `g`. -/
 theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g :=
   { epi := epi_of_epi f g
-    llp := fun {X Y} z _ => by
+    llp := fun {X} {Y} z _ => by
       constructor
       intro u v sq
       have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]
@@ -130,25 +130,27 @@ theorem strongEpi_of_strongEpi [StrongEpi (f ≫ g)] : StrongEpi g :=
 /-- If `f ≫ g` is a strong monomorphism, then so is `f`. -/
 theorem strongMono_of_strongMono [StrongMono (f ≫ g)] : StrongMono f :=
   { mono := mono_of_mono f g
-    rlp := fun {X Y} z => by
+    rlp := fun {X} {Y} z => by
       intros
       constructor
       intro u v sq
-      have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by
+      have h₀ : u ≫ f ≫ g = z ≫ v ≫ g := by 
         rw [←Category.assoc, eq_whisker sq.w, Category.assoc]
       exact CommSq.HasLift.mk' ⟨(CommSq.mk h₀).lift, by simp, by simp [← cancel_epi z, sq.w]⟩ }
 #align category_theory.strong_mono_of_strong_mono CategoryTheory.strongMono_of_strongMono
 
 /-- An isomorphism is in particular a strong epimorphism. -/
-instance (priority := 100) strongEpi_of_isIso [IsIso f] : StrongEpi f where
+instance (priority := 100) strongEpi_of_isIso [IsIso f] : StrongEpi f
+    where
   epi := by infer_instance
-  llp {X Y} z := HasLiftingProperty.of_left_iso _ _
+  llp {X} {Y} z := HasLiftingProperty.of_left_iso _ _
 #align category_theory.strong_epi_of_is_iso CategoryTheory.strongEpi_of_isIso
 
 /-- An isomorphism is in particular a strong monomorphism. -/
-instance (priority := 100) strongMono_of_isIso [IsIso f] : StrongMono f where
+instance (priority := 100) strongMono_of_isIso [IsIso f] : StrongMono f
+    where
   mono := by infer_instance
-  rlp {X Y} z := HasLiftingProperty.of_right_iso _ _
+  rlp {X} {Y} z := HasLiftingProperty.of_right_iso _ _
 #align category_theory.strong_mono_of_is_iso CategoryTheory.strongMono_of_isIso
 
 theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
@@ -157,7 +159,7 @@ theorem StrongEpi.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
       rw [Arrow.iso_w' e]
       haveI := epi_comp f e.hom.right
       apply epi_comp
-    llp := fun {X Y} z => by
+    llp := fun {X} {Y} z => by
       intro
       apply HasLiftingProperty.of_arrow_iso_left e z }
 #align category_theory.strong_epi.of_arrow_iso CategoryTheory.StrongEpi.of_arrow_iso
@@ -168,7 +170,7 @@ theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
       rw [Arrow.iso_w' e]
       haveI := mono_comp f e.hom.right
       apply mono_comp
-    rlp := fun {X Y} z => by
+    rlp := fun {X} {Y} z => by
       intro
       apply HasLiftingProperty.of_arrow_iso_right z e }
 #align category_theory.strong_mono.of_arrow_iso CategoryTheory.StrongMono.of_arrow_iso
@@ -176,13 +178,13 @@ theorem StrongMono.of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
 theorem StrongEpi.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
     (e : Arrow.mk f ≅ Arrow.mk g) : StrongEpi f ↔ StrongEpi g := by
   constructor <;> intro
-  exacts [StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]
+  exacts[StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]
 #align category_theory.strong_epi.iff_of_arrow_iso CategoryTheory.StrongEpi.iff_of_arrow_iso
 
 theorem StrongMono.iff_of_arrow_iso {A B A' B' : C} {f : A ⟶ B} {g : A' ⟶ B'}
     (e : Arrow.mk f ≅ Arrow.mk g) : StrongMono f ↔ StrongMono g := by
   constructor <;> intro
-  exacts [StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm]
+  exacts[StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm]
 #align category_theory.strong_mono.iff_of_arrow_iso CategoryTheory.StrongMono.iff_of_arrow_iso
 
 end
@@ -206,14 +208,12 @@ class StrongEpiCategory : Prop where
   /-- A strong epi category is a category in which every epimorphism is strong. -/
   strongEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], StrongEpi f
 #align category_theory.strong_epi_category CategoryTheory.StrongEpiCategory
-#align category_theory.strong_epi_category.strong_epi_of_epi CategoryTheory.StrongEpiCategory.strongEpi_of_epi
 
 /-- A strong mono category is a category in which every monomorphism is strong. -/
 class StrongMonoCategory : Prop where
   /-- A strong mono category is a category in which every monomorphism is strong. -/
   strongMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], StrongMono f
 #align category_theory.strong_mono_category CategoryTheory.StrongMonoCategory
-#align category_theory.strong_mono_category.strong_mono_of_mono CategoryTheory.StrongMonoCategory.strongMono_of_mono
 
 end
 
@@ -229,8 +229,8 @@ section
 
 attribute [local instance] strongEpi_of_epi
 
-instance (priority := 100) balanced_of_strongEpiCategory [StrongEpiCategory C] : Balanced C where
-  isIso_of_mono_of_epi _ _ _ := isIso_of_mono_of_strongEpi _
+instance (priority := 100) balanced_of_strongEpiCategory [StrongEpiCategory C] : Balanced C
+    where isIso_of_mono_of_epi _ _ _ := isIso_of_mono_of_strongEpi _
 #align category_theory.balanced_of_strong_epi_category CategoryTheory.balanced_of_strongEpiCategory
 
 end
@@ -239,10 +239,11 @@ section
 
 attribute [local instance] strongMono_of_mono
 
-instance (priority := 100) balanced_of_strongMonoCategory [StrongMonoCategory C] : Balanced C where
-  isIso_of_mono_of_epi _ _ _ := isIso_of_epi_of_strongMono _
+instance (priority := 100) balanced_of_strongMonoCategory [StrongMonoCategory C] : Balanced C
+    where isIso_of_mono_of_epi _ _ _ := isIso_of_epi_of_strongMono _
 #align category_theory.balanced_of_strong_mono_category CategoryTheory.balanced_of_strongMonoCategory
 
 end
 
 end CategoryTheory
+#lint
diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean
index dcb2885c5cd47..19d9e10022e0c 100644
--- a/Mathlib/CategoryTheory/Pi/Basic.lean
+++ b/Mathlib/CategoryTheory/Pi/Basic.lean
@@ -29,7 +29,8 @@ variable {I : Type w₀} {J : Type w₁} (C : I → Type u₁) [∀ i, Category.
 
 /-- `pi C` gives the cartesian product of an indexed family of categories.
 -/
-instance pi : Category.{max w₀ v₁} (∀ i, C i) where
+instance pi : Category.{max w₀ v₁} (∀ i, C i)
+    where
   Hom X Y := ∀ i, X i ⟶ Y i
   id X i := 𝟙 (X i)
   comp f g i := f i ≫ g i
@@ -70,17 +71,18 @@ section
 
 variable {J : Type w₁}
 
-/- Porting note: add this because Lean cannot see directly through the `∘` for
+/- Porting note: add this because Lean cannot see directly through the `∘` for 
 `Function.comp` -/
 
-instance (f : J → I) : (j : J) → Category ((C ∘ f) j) := by
+instance (f : J → I) : (j : J) → Category ((C ∘ f) j) := by 
   dsimp
-  infer_instance
+  infer_instance 
 
 /-- Pull back an `I`-indexed family of objects to an `J`-indexed family, along a function `J → I`.
 -/
 @[simps]
-def comap (h : J → I) : (∀ i, C i) ⥤  (∀ j, C (h j)) where
+def comap (h : J → I) : (∀ i, C i) ⥤  (∀ j, C (h j))
+    where
   obj f i := f (h i)
   map α i := α (h i)
 #align category_theory.pi.comap CategoryTheory.Pi.comap
@@ -91,12 +93,13 @@ variable (I)
 pulling back a grading along the identity function,
 and the identity functor. -/
 @[simps]
-def comapId : comap C (id : I → I) ≅ 𝟭 (∀ i, C i) where
+def comapId : comap C (id : I → I) ≅ 𝟭 (∀ i, C i)
+    where
   hom := { app := fun X => 𝟙 X, naturality := by simp only [comap]; aesop_cat}
   inv := { app := fun X => 𝟙 X }
 #align category_theory.pi.comap_id CategoryTheory.Pi.comapId
 
-example (g : J → I) : (j : J) → Category (C (g j)) := by infer_instance
+example (g : J → I) : (j : J) → Category (C (g j)) := by infer_instance 
 
 variable {I}
 
@@ -107,20 +110,21 @@ pulling back along two successive functions, and
 pulling back along their composition
 -/
 @[simps!]
-def comapComp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f) where
-  hom := {
-    app := fun X b => 𝟙 (X (g (f b)))
+def comapComp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅ comap C (g ∘ f)
+    where
+  hom := { 
+    app := fun X b => 𝟙 (X (g (f b))) 
     naturality := fun X Y f' => by simp only [comap,Function.comp]; funext; simp
     }
-  inv := {
+  inv := { 
     app := fun X b => 𝟙 (X (g (f b)))
     naturality := fun X Y f' => by simp only [comap,Function.comp]; funext; simp
     }
-  hom_inv_id := by
-    simp only [comap]
-    ext Y
+  hom_inv_id := by 
+    simp only [comap] 
+    ext Y 
     simp [CategoryStruct.comp,CategoryStruct.id]
-  inv_hom_id := by
+  inv_hom_id := by 
     simp only [comap]
     ext X
     simp [CategoryStruct.comp,CategoryStruct.id]
@@ -138,7 +142,23 @@ section
 
 variable {J : Type w₀} {D : J → Type u₁} [∀ j, Category.{v₁} (D j)]
 
-/- Porting note: maybe mixing up universes -/
+/- Porting note: We have the following warning but it just looks 
+to me to be permutation of the universe labels 
+
+warning: category_theory.pi.sum_elim_category ->
+\  CategoryTheory.Pi.sumElimCategory is a dubious translation:
+lean 3 declaration is forall {I : Type.{u1}} (C : I -> Type.{u3}) [_inst_1 :
+forall (i : I), CategoryTheory.Category.{u2, u3} (C i)] {J : Type.{u1}} {D : J
+-> Type.{u3}} [_inst_2 : forall (j : J), CategoryTheory.Category.{u2, u3} (D
+j)] (s : Sum.{u1, u1} I J), CategoryTheory.Category.{u2, u3} (Sum.elim.{u1, u1,
+succ (succ u3)} I J Type.{u3} C D s) but is expected to have type forall {I :
+Type.{u3}} (C : I -> Type.{u1}) [_inst_1 : forall (i : I),
+CategoryTheory.Category.{u2, u1} (C i)] {J : Type.{u3}} {D : J -> Type.{u1}}
+[_inst_2 : forall (j : J), CategoryTheory.Category.{u2, u1} (D j)] (s :
+Sum.{u3, u3} I J), CategoryTheory.Category.{u2, u1} (Sum.elim.{u3, u3, succ
+(succ u1)} I J Type.{u1} C D s) Case conversion may be inaccurate. Consider
+using '#align category_theory.pi.sum_elim_category
+CategoryTheory.Pi.sumElimCategoryₓ'. -/
 instance sumElimCategory : ∀ s : Sum I J, Category.{v₁} (Sum.elim C D s)
   | Sum.inl i => by
     dsimp
@@ -146,42 +166,43 @@ instance sumElimCategory : ∀ s : Sum I J, Category.{v₁} (Sum.elim C D s)
   | Sum.inr j => by
     dsimp
     infer_instance
-#align category_theory.pi.sum_elim_category CategoryTheory.Pi.sumElimCategoryₓ
+#align category_theory.pi.sum_elim_category CategoryTheory.Pi.sumElimCategory
 
-/- Porting note: replaced `Sum.rec` with `match`'s per the error about
-current state of code generation -/
+/- Porting note: replaced `Sum.rec` with `match`'s per the error about 
+current state of code generation -/ 
 
 /-- The bifunctor combining an `I`-indexed family of objects with a `J`-indexed family of objects
 to obtain an `I ⊕ J`-indexed family of objects.
 -/
 @[simps]
-def sum : (∀ i, C i) ⥤ (∀ j, D j) ⥤ ∀ s : Sum I J, Sum.elim C D s where
+def sum : (∀ i, C i) ⥤ (∀ j, D j) ⥤ ∀ s : Sum I J, Sum.elim C D s
+    where
   obj X :=
-    { obj := fun Y s =>
-        match s with
-        | .inl i => X i
+    { obj := fun Y s => 
+        match s with 
+        | .inl i => X i 
         | .inr j => Y j
-      map := fun {Y} {Y'} f s =>
-        match s with
-        | .inl i => 𝟙 (X i)
+      map := fun {Y} {Y'} f s => 
+        match s with 
+        | .inl i => 𝟙 (X i) 
         | .inr j => f j
-      map_id := fun Y => by
+      map_id := fun Y => by 
           dsimp
           simp only [CategoryStruct.id]
-          funext s
-          match s with
-          | .inl i => simp
-          | .inr j => simp
+          funext s 
+          match s with 
+          | .inl i => simp 
+          | .inr j => simp 
       map_comp := fun {Y₁} {Y₂} {Y₃} f g => by funext s; cases s; repeat {simp} }
-  map {X} {X'} f :=
-    { app := fun Y s =>
-        match s with
-        | .inl i => f i
-        | .inr j => 𝟙 (Y j)
+  map {X} {X'} f := 
+    { app := fun Y s => 
+        match s with 
+        | .inl i => f i 
+        | .inr j => 𝟙 (Y j) 
       naturality := fun {Y} {Y'} g => by funext s; cases s; repeat {simp} }
-  map_id := fun X => by
+  map_id := fun X => by 
     ext Y; dsimp; simp only [CategoryStruct.id]; funext s; cases s; repeat {simp}
-  map_comp := fun f g => by
+  map_comp := fun f g => by 
     ext Y; dsimp; simp only [CategoryStruct.comp]; funext s; cases s; repeat {simp}
 #align category_theory.pi.sum CategoryTheory.Pi.sum
 
@@ -228,7 +249,8 @@ variable {D : I → Type u₁} [∀ i, Category.{v₁} (D i)] {A : Type u₁} [C
 /-- Assemble an `I`-indexed family of functors into a functor between the pi types.
 -/
 @[simps]
-def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i where
+def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i
+    where
   obj f i := (F i).obj (f i)
   map α i := (F i).map (α i)
 #align category_theory.functor.pi CategoryTheory.Functor.pi
@@ -236,7 +258,8 @@ def pi (F : ∀ i, C i ⥤ D i) : (∀ i, C i) ⥤ ∀ i, D i where
 /-- Similar to `pi`, but all functors come from the same category `A`
 -/
 @[simps]
-def pi' (f : ∀ i, A ⥤ C i) : A ⥤ ∀ i, C i where
+def pi' (f : ∀ i, A ⥤ C i) : A ⥤ ∀ i, C i
+    where
   obj a i := (f i).obj a
   map h i := (f i).map h
 #align category_theory.functor.pi' CategoryTheory.Functor.pi'
@@ -256,15 +279,15 @@ end EqToHom
 -- how `Functor.pi` commutes with `Pi.eval` and `Pi.comap`.
 @[simp]
 theorem pi'_eval (f : ∀ i, A ⥤ C i) (i : I) : pi' f ⋙  Pi.eval C i = f i := by
-  apply Functor.ext
-  intro _ _ _
-  · simp
-  · intro _
-    rfl
+  apply Functor.ext 
+  intro _ _ _ 
+  · simp 
+  · intro _ 
+    rfl 
 #align category_theory.functor.pi'_eval CategoryTheory.Functor.pi'_eval
 
 /-- Two functors to a product category are equal iff they agree on every coordinate. -/
-theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' ⋙ (Pi.eval C i))
+theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙  (Pi.eval C i) = f' ⋙  (Pi.eval C i)) 
     : f = f' := by
   apply Functor.ext; rotate_left
   · intro X
@@ -273,7 +296,7 @@ theorem pi_ext (f f' : A ⥤ ∀ i, C i) (h : ∀ i, f ⋙ (Pi.eval C i) = f' 
     have := congr_obj h X
     simpa
   · intro X Y g
-    dsimp
+    dsimp 
     funext i
     specialize h i
     have := congr_hom h g
@@ -293,8 +316,8 @@ variable {F G : ∀ i, C i ⥤ D i}
 /-- Assemble an `I`-indexed family of natural transformations into a single natural transformation.
 -/
 @[simps!]
-def pi (α : ∀ i, F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G where
-  app f i := (α i).app (f i)
+def pi (α : ∀ i, F i ⟶ G i) : Functor.pi F ⟶ Functor.pi G where 
+  app f i := (α i).app (f i) 
   naturality := fun X Y f => by simp [Functor.pi,CategoryStruct.comp]
 #align category_theory.nat_trans.pi CategoryTheory.NatTrans.pi
 
diff --git a/Mathlib/CategoryTheory/Types.lean b/Mathlib/CategoryTheory/Types.lean
index aa3befe7b5b8c..63f7c04605930 100644
--- a/Mathlib/CategoryTheory/Types.lean
+++ b/Mathlib/CategoryTheory/Types.lean
@@ -88,7 +88,8 @@ abbrev asHom {α β : Type u} (f : α → β) : α ⟶ β :=
   f
 #align category_theory.as_hom CategoryTheory.asHom
 
-@[inherit_doc]
+-- If you don't mind some notation you can use fewer keystrokes:
+/-- Type as \upr in VScode -/
 scoped notation "↾" f:200 => CategoryTheory.asHom f
 
 section
diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
index 6d0fbd315294c..7773489921444 100644
--- a/Mathlib/CategoryTheory/Yoneda.lean
+++ b/Mathlib/CategoryTheory/Yoneda.lean
@@ -217,6 +217,24 @@ noncomputable def reprF : yoneda.obj F.reprX ⟶ F :=
   Representable.has_representation.choose_spec.choose
 #align category_theory.functor.repr_f CategoryTheory.Functor.reprF
 
+/- warning: category_theory.functor.repr_x clashes with
+\  category_theory.functor.repr_X -> CategoryTheory.Functor.reprX
+warning: category_theory.functor.repr_x -> CategoryTheory.Functor.reprX is a
+dubious translation: lean 3 declaration is forall {C : Type.{u2}} [_inst_1 :
+CategoryTheory.Category.{u1, u2} C] (F : CategoryTheory.Functor.{u1, u1, u2,
+succ u1} (Opposite.{succ u2} C) (CategoryTheory.Category.opposite.{u1, u2} C
+_inst_1) Type.{u1} CategoryTheory.types.{u1}) [_inst_2 :
+CategoryTheory.Functor.Representable.{u1, u2} C _inst_1 F],
+CategoryTheory.Functor.obj.{u1, u1, u2, succ u1} (Opposite.{succ u2} C)
+(CategoryTheory.Category.opposite.{u1, u2} C _inst_1) Type.{u1}
+CategoryTheory.types.{u1} F (Opposite.op.{succ u2} C
+(CategoryTheory.Functor.reprX.{u1, u2} C _inst_1 F _inst_2)) but is expected to
+have type forall {C : Type.{u2}} [_inst_1 : CategoryTheory.Category.{u1, u2} C]
+(F : CategoryTheory.Functor.{u1, u1, u2, succ u1} (Opposite.{succ u2} C)
+(CategoryTheory.Category.opposite.{u1, u2} C _inst_1) Type.{u1}
+CategoryTheory.types.{u1}) [_inst_2 : CategoryTheory.Functor.Representable.{u1,
+u2} C _inst_1 F], C Case conversion may be inaccurate. Consider using '#align
+category_theory.functor.repr_x CategoryTheory.Functor.reprXₓ'. -/
 /-- The representing element for the representable functor `F`, sometimes called the universal
 element of the functor.
 -/
@@ -266,6 +284,21 @@ noncomputable def coreprF : coyoneda.obj (op F.coreprX) ⟶ F :=
   Corepresentable.has_corepresentation.choose_spec.choose
 #align category_theory.functor.corepr_f CategoryTheory.Functor.coreprF
 
+/- warning: category_theory.functor.corepr_x clashes with
+\  category_theory.functor.corepr_X -> CategoryTheory.Functor.coreprX
+warning: category_theory.functor.corepr_x -> CategoryTheory.Functor.coreprX is
+a dubious translation: lean 3 declaration is forall {C : Type.{u2}} [_inst_1 :
+CategoryTheory.Category.{u1, u2} C] (F : CategoryTheory.Functor.{u1, u1, u2,
+succ u1} C _inst_1 Type.{u1} CategoryTheory.types.{u1}) [_inst_2 :
+CategoryTheory.Functor.Corepresentable.{u1, u2} C _inst_1 F],
+CategoryTheory.Functor.obj.{u1, u1, u2, succ u1} C _inst_1 Type.{u1}
+CategoryTheory.types.{u1} F (CategoryTheory.Functor.coreprX.{u1, u2} C _inst_1
+F _inst_2) but is expected to have type forall {C : Type.{u2}} [_inst_1 :
+CategoryTheory.Category.{u1, u2} C] (F : CategoryTheory.Functor.{u1, u1, u2,
+succ u1} C _inst_1 Type.{u1} CategoryTheory.types.{u1}) [_inst_2 :
+CategoryTheory.Functor.Corepresentable.{u1, u2} C _inst_1 F], C Case conversion
+may be inaccurate. Consider using '#align category_theory.functor.corepr_x
+CategoryTheory.Functor.coreprXₓ'. -/
 /-- The representing element for the corepresentable functor `F`, sometimes called the universal
 element of the functor.
 -/
diff --git a/Mathlib/Tactic/Core.lean b/Mathlib/Tactic/Core.lean
index d240a76eb102c..0aa9edc66aae9 100644
--- a/Mathlib/Tactic/Core.lean
+++ b/Mathlib/Tactic/Core.lean
@@ -102,39 +102,6 @@ end Lean
 
 namespace Lean.Elab.Tactic
 
-/-- Given a local context and an array of `FVarIds` assumed to be in that local context, remove all
-implementation details. -/
-def filterOutImplementationDetails (lctx : LocalContext) (fvarIds : Array FVarId) : Array FVarId :=
-  fvarIds.filter (fun fvar => ! (lctx.fvarIdToDecl.find! fvar).isImplementationDetail)
-
-/-- Elaborate syntax for an `FVarId` in the local context of the given goal. -/
-def getFVarIdAt (goal : MVarId) (id : Syntax) : TacticM FVarId := withRef id do
-  -- use apply-like elaboration to suppress insertion of implicit arguments
-  let e ← goal.withContext do
-    elabTermForApply id (mayPostpone := false)
-  match e with
-  | Expr.fvar fvarId => return fvarId
-  | _                => throwError "unexpected term '{e}'; expected single reference to variable"
-
-/-- Get the array of `FVarId`s in the local context of the given `goal`.
-
-If `ids` is specified, elaborate them in the local context of the given goal to obtain the array of
-`FVarId`s.
-
-If `includeImplementationDetails` is `false` (the default), we filter out implementation details
-(`implDecl`s and `auxDecl`s) from the resulting list of `FVarId`s. -/
-def getFVarIdsAt (goal : MVarId) (ids : Option (Array Syntax) := none)
-    (includeImplementationDetails : Bool := false) : TacticM (Array FVarId) :=
-  goal.withContext do
-    let lctx := (← goal.getDecl).lctx
-    let fvarIds ← match ids with
-    | none => pure lctx.getFVarIds
-    | some ids => ids.mapM <| getFVarIdAt goal
-    if includeImplementationDetails then
-      return fvarIds
-    else
-      return filterOutImplementationDetails lctx fvarIds
-
 /--
 Run a tactic on all goals, and always succeeds.
 
diff --git a/lean-toolchain b/lean-toolchain
index d88e7bc6387b8..04ab6c3b09caa 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-23
+leanprover/lean4:nightly-2023-02-03
diff --git a/test/slice.lean b/test/slice.lean
index 6d9d47c7aee08..818c82d6eb420 100644
--- a/test/slice.lean
+++ b/test/slice.lean
@@ -3,24 +3,16 @@ import Mathlib.Tactic.Slice
 open CategoryTheory
 
 variable (C : Type) [Category C] (X Y Z W U : C)
-variable (f₁ f₂ : X ⟶ Y) (g g₁ g₂ : Y ⟶ Z) (h : Z ⟶ W) (l : W ⟶ U)
+variable (f₁ f₂ : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (l : W ⟶ U)
 
-example (hyp : f₁ ≫ g₁ = f₂ ≫ g₂) : f₁ ≫ g₁ ≫ h ≫ l = (f₂ ≫ g₂) ≫ (h ≫ l) := by
-  conv =>
-    rhs
-    slice 2 3
-  show f₁ ≫ g₁ ≫ h ≫ l = f₂ ≫ (g₂ ≫ h) ≫ l
+example (h₁ : f₁ = f₂) : f₁ ≫ g ≫ h ≫ l = ((f₂ ≫ g) ≫ h) ≫ l := by
   conv =>
     lhs
-    slice 1 2
-    rw [hyp]
-  show ((f₂ ≫ g₂) ≫ h) ≫ l = f₂ ≫ (g₂ ≫ h) ≫ l
+    slice 1 4
   conv =>
     lhs
-    slice 2 3
-
-example (hyp : f₁ ≫ g₁ = f₂ ≫ g₂) : f₁ ≫ g₁ ≫ h ≫ l = (f₂ ≫ g₂) ≫ (h ≫ l) := by
-  slice_lhs 1 2 => { rw [hyp] }; slice_rhs 1 2 => skip
+    slice 1 1
+    rw [h₁]
 
 example (h₁ : f₁ = f₂) : f₁ ≫ g ≫ h ≫ l = ((f₂ ≫ g) ≫ h) ≫ l := by
   slice_lhs 1 1 => rw [h₁]