From 82e25124b8f38e2494e781bf4c1fd0ab432effc0 Mon Sep 17 00:00:00 2001
From: adamtopaz <github@adamtopaz.com>
Date: Tue, 14 Feb 2023 22:06:54 -0700
Subject: [PATCH 01/14] feat: port CategoryTheory.DiscreteCategory


From 10bf4bb690318c385e5fa84948e4d987ad115bd9 Mon Sep 17 00:00:00 2001
From: adamtopaz <github@adamtopaz.com>
Date: Tue, 14 Feb 2023 22:06:54 -0700
Subject: [PATCH 02/14] Initial file copy from mathport

---
 Mathlib/CategoryTheory/DiscreteCategory.lean | 342 +++++++++++++++++++
 1 file changed, 342 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/DiscreteCategory.lean

diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
new file mode 100644
index 0000000000000..73f5bc502005e
--- /dev/null
+++ b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -0,0 +1,342 @@
+/-
+Copyright (c) 2017 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stephen Morgan, Scott Morrison, Floris van Doorn
+
+! This file was ported from Lean 3 source module category_theory.discrete_category
+! leanprover-community/mathlib commit 369525b73f229ccd76a6ec0e0e0bf2be57599768
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.CategoryTheory.EqToHom
+import Mathbin.Data.Ulift
+
+/-!
+# Discrete categories
+
+We define `discrete α` as a structure containing a term `a : α` for any type `α`,
+and use this type alias to provide a `small_category` instance
+whose only morphisms are the identities.
+
+There is an annoying technical difficulty that it has turned out to be inconvenient
+to allow categories with morphisms living in `Prop`,
+so instead of defining `X ⟶ Y` in `discrete α` as `X = Y`,
+one might define it as `plift (X = Y)`.
+In fact, to allow `discrete α` to be a `small_category`
+(i.e. with morphisms in the same universe as the objects),
+we actually define the hom type `X ⟶ Y` as `ulift (plift (X = Y))`.
+
+`discrete.functor` promotes a function `f : I → C` (for any category `C`) to a functor
+`discrete.functor f : discrete I ⥤ C`.
+
+Similarly, `discrete.nat_trans` and `discrete.nat_iso` promote `I`-indexed families of morphisms,
+or `I`-indexed families of isomorphisms to natural transformations or natural isomorphism.
+
+We show equivalences of types are the same as (categorical) equivalences of the corresponding
+discrete categories.
+-/
+
+
+namespace CategoryTheory
+
+-- morphism levels before object levels. See note [category_theory universes].
+universe v₁ v₂ v₃ u₁ u₁' u₂ u₃
+
+-- This is intentionally a structure rather than a type synonym
+-- to enforce using `discrete_equiv` (or `discrete.mk` and `discrete.as`) to move between
+-- `discrete α` and `α`. Otherwise there is too much API leakage.
+/-- A wrapper for promoting any type to a category,
+with the only morphisms being equalities.
+-/
+@[ext]
+structure Discrete (α : Type u₁) where
+  as : α
+#align category_theory.discrete CategoryTheory.Discrete
+
+@[simp]
+theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X :=
+  by
+  ext
+  rfl
+#align category_theory.discrete.mk_as CategoryTheory.Discrete.mk_as
+
+/-- `discrete α` is equivalent to the original type `α`.-/
+@[simps]
+def discreteEquiv {α : Type u₁} : Discrete α ≃ α
+    where
+  toFun := Discrete.as
+  invFun := Discrete.mk
+  left_inv := by tidy
+  right_inv := by tidy
+#align category_theory.discrete_equiv CategoryTheory.discreteEquiv
+
+instance {α : Type u₁} [DecidableEq α] : DecidableEq (Discrete α) :=
+  discreteEquiv.DecidableEq
+
+/-- The "discrete" category on a type, whose morphisms are equalities.
+
+Because we do not allow morphisms in `Prop` (only in `Type`),
+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
+  Hom X Y := ULift (PLift (X.as = Y.as))
+  id X := ULift.up (PLift.up rfl)
+  comp X Y Z g f := by
+    cases X
+    cases Y
+    cases Z
+    rcases f with ⟨⟨⟨⟩⟩⟩
+    exact g
+#align category_theory.discrete_category CategoryTheory.discreteCategory
+
+namespace Discrete
+
+variable {α : Type u₁}
+
+instance [Inhabited α] : Inhabited (Discrete α) :=
+  ⟨⟨default⟩⟩
+
+instance [Subsingleton α] : Subsingleton (Discrete α) :=
+  ⟨by
+    intros
+    ext
+    apply Subsingleton.elim⟩
+
+/- ./././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
+
+run_cmd
+  add_interactive [`` tactic.discrete_cases]
+
+attribute [local tidy] tactic.discrete_cases
+
+instance [Unique α] : Unique (Discrete α) :=
+  Unique.mk' (Discrete α)
+
+/-- Extract the equation from a morphism in a discrete category. -/
+theorem eq_of_hom {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as :=
+  i.down.down
+#align category_theory.discrete.eq_of_hom CategoryTheory.Discrete.eq_of_hom
+
+/-- Promote an equation between the wrapped terms in `X Y : discrete α` to a morphism `X ⟶ Y`
+in the discrete category. -/
+abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
+  eqToHom
+    (by
+      ext
+      exact h)
+#align category_theory.discrete.eq_to_hom CategoryTheory.Discrete.eqToHom
+
+/-- Promote an equation between the wrapped terms in `X Y : discrete α` to an isomorphism `X ≅ Y`
+in the discrete category. -/
+abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y :=
+  eqToIso
+    (by
+      ext
+      exact h)
+#align category_theory.discrete.eq_to_iso CategoryTheory.Discrete.eqToIso
+
+/-- 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 :=
+  eqToHom h
+#align category_theory.discrete.eq_to_hom' CategoryTheory.Discrete.eqToHom'
+
+/-- A variant of `eq_to_iso` that lifts terms to the discrete category. -/
+abbrev eqToIso' {a b : α} (h : a = b) : Discrete.mk a ≅ Discrete.mk b :=
+  eqToIso h
+#align category_theory.discrete.eq_to_iso' CategoryTheory.Discrete.eqToIso'
+
+@[simp]
+theorem id_def (X : Discrete α) : ULift.up (PLift.up (Eq.refl X.as)) = 𝟙 X :=
+  rfl
+#align category_theory.discrete.id_def CategoryTheory.Discrete.id_def
+
+variable {C : Type u₂} [Category.{v₂} C]
+
+instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f :=
+  ⟨⟨eqToHom (eq_of_hom f).symm, by tidy⟩⟩
+
+/- ./././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
+    trace
+      "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+    cases f
+    exact 𝟙 (F X)
+#align category_theory.discrete.functor CategoryTheory.Discrete.functor
+
+@[simp]
+theorem functor_obj {I : Type u₁} (F : I → C) (i : I) :
+    (Discrete.functor F).obj (Discrete.mk i) = F i :=
+  rfl
+#align category_theory.discrete.functor_obj CategoryTheory.Discrete.functor_obj
+
+theorem functor_map {I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i) :
+    (Discrete.functor F).map f = 𝟙 (F i.as) := by tidy
+#align category_theory.discrete.functor_map CategoryTheory.Discrete.functor_map
+
+/-- The discrete functor induced by a composition of maps can be written as a
+composition of two discrete functors.
+-/
+@[simps]
+def functorComp {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) :
+    Discrete.functor (f ∘ g) ≅ Discrete.functor (Discrete.mk ∘ g) ⋙ Discrete.functor f :=
+  NatIso.ofComponents (fun X => Iso.refl _) (by tidy)
+#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.
+-/
+@[simps]
+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' X Y g :=
+    by
+    trace
+      "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+    cases g
+    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 X Y g =>
+    by
+    trace
+      "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+    cases g
+    simp
+#align category_theory.discrete.nat_iso CategoryTheory.Discrete.natIso
+
+@[simp]
+theorem natIso_app {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i)
+    (i : Discrete I) : (Discrete.natIso f).app i = f i := by tidy
+#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]
+def natIsoFunctor {I : Type u₁} {F : Discrete I ⥤ C} : F ≅ Discrete.functor (F.obj ∘ Discrete.mk) :=
+  natIso fun i =>
+    by
+    trace
+      "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+    rfl
+#align category_theory.discrete.nat_iso_functor CategoryTheory.Discrete.natIsoFunctor
+
+/-- Composing `discrete.functor F` with another functor `G` amounts to composing `F` with `G.obj` -/
+@[simp]
+def compNatIsoDiscrete {I : Type u₁} {D : Type u₃} [Category.{v₃} D] (F : I → C) (G : C ⥤ D) :
+    Discrete.functor F ⋙ G ≅ Discrete.functor (G.obj ∘ F) :=
+  natIso fun i => Iso.refl _
+#align category_theory.discrete.comp_nat_iso_discrete CategoryTheory.Discrete.compNatIsoDiscrete
+
+/- ./././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
+  Functor := Discrete.functor (Discrete.mk ∘ (e : I → J))
+  inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I))
+  unitIso :=
+    Discrete.natIso fun i =>
+      eqToIso
+        (by
+          trace
+            "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+          simp)
+  counitIso :=
+    Discrete.natIso fun j =>
+      eqToIso
+        (by
+          trace
+            "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+          simp)
+#align category_theory.discrete.equivalence CategoryTheory.Discrete.equivalence
+
+/-- We can convert an equivalence of `discrete` categories to a type-level `equiv`. -/
+@[simps]
+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.unit_iso.app (discrete.mk a)).2
+  right_inv a := by simpa using eq_of_hom (h.counit_iso.app (discrete.mk a)).1
+#align category_theory.discrete.equiv_of_equivalence CategoryTheory.Discrete.equivOfEquivalence
+
+end Discrete
+
+namespace Discrete
+
+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 α :=
+  by
+  let F : Discrete α ⥤ (Discrete α)ᵒᵖ := Discrete.functor fun x => op (Discrete.mk x)
+  refine'
+    equivalence.mk (functor.left_op F) F _
+      (discrete.nat_iso fun X =>
+        by
+        trace
+          "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+        simp [F])
+  refine'
+    nat_iso.of_components
+      (fun X =>
+        by
+        run_tac
+          tactic.op_induction'
+        trace
+          "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+        simp [F])
+      _
+  tidy
+#align category_theory.discrete.opposite CategoryTheory.Discrete.opposite
+
+variable {C : Type u₂} [Category.{v₂} C]
+
+@[simp]
+theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F.map f = 𝟙 (F.obj j) :=
+  by
+  have h : f = 𝟙 j := by
+    cases f
+    cases f
+    ext
+  rw [h]
+  simp
+#align category_theory.discrete.functor_map_id CategoryTheory.Discrete.functor_map_id
+
+end Discrete
+
+end CategoryTheory
+

From 22034856ebc97b161fcc7b9d476049ebeeb8daca Mon Sep 17 00:00:00 2001
From: adamtopaz <github@adamtopaz.com>
Date: Tue, 14 Feb 2023 22:06:54 -0700
Subject: [PATCH 03/14] automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
---
 Mathlib.lean                                 |  1 +
 Mathlib/CategoryTheory/DiscreteCategory.lean | 10 ++++------
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 6aa0550bef09c..532844fa3acc7 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -225,6 +225,7 @@ import Mathlib.CategoryTheory.Category.KleisliCat
 import Mathlib.CategoryTheory.Category.RelCat
 import Mathlib.CategoryTheory.Comma
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
+import Mathlib.CategoryTheory.DiscreteCategory
 import Mathlib.CategoryTheory.EqToHom
 import Mathlib.CategoryTheory.Equivalence
 import Mathlib.CategoryTheory.EssentialImage
diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
index 73f5bc502005e..871c80e12f731 100644
--- a/Mathlib/CategoryTheory/DiscreteCategory.lean
+++ b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -8,8 +8,8 @@ Authors: Stephen Morgan, 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.EqToHom
-import Mathbin.Data.Ulift
+import Mathlib.CategoryTheory.EqToHom
+import Mathlib.Data.Ulift
 
 /-!
 # Discrete categories
@@ -54,8 +54,7 @@ structure Discrete (α : Type u₁) where
 #align category_theory.discrete CategoryTheory.Discrete
 
 @[simp]
-theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X :=
-  by
+theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X := by
   ext
   rfl
 #align category_theory.discrete.mk_as CategoryTheory.Discrete.mk_as
@@ -300,8 +299,7 @@ open Opposite
 /- ./././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 α :=
-  by
+protected def opposite (α : Type u₁) : (Discrete α)ᵒᵖ ≌ Discrete α := by
   let F : Discrete α ⥤ (Discrete α)ᵒᵖ := Discrete.functor fun x => op (Discrete.mk x)
   refine'
     equivalence.mk (functor.left_op F) F _

From 8860e0dbee2c5b58a3e890ba3447af0443052316 Mon Sep 17 00:00:00 2001
From: adamtopaz <github@adamtopaz.com>
Date: Thu, 16 Feb 2023 17:33:00 -0700
Subject: [PATCH 04/14] get file to build

---
 Mathlib/CategoryTheory/DiscreteCategory.lean | 148 ++++++++++---------
 1 file changed, 81 insertions(+), 67 deletions(-)

diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
index 871c80e12f731..eec8f2d961faf 100644
--- a/Mathlib/CategoryTheory/DiscreteCategory.lean
+++ b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -9,7 +9,10 @@ Authors: Stephen Morgan, Scott Morrison, Floris van Doorn
 ! if you have ported upstream changes.
 -/
 import Mathlib.CategoryTheory.EqToHom
-import Mathlib.Data.Ulift
+import Mathlib.Data.ULift
+import Mathlib.Tactic.CasesM
+
+open Lean Meta
 
 /-!
 # Discrete categories
@@ -65,12 +68,12 @@ def discreteEquiv {α : Type u₁} : Discrete α ≃ α
     where
   toFun := Discrete.as
   invFun := Discrete.mk
-  left_inv := by tidy
-  right_inv := by tidy
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
 #align category_theory.discrete_equiv CategoryTheory.discreteEquiv
 
 instance {α : Type u₁} [DecidableEq α] : DecidableEq (Discrete α) :=
-  discreteEquiv.DecidableEq
+  discreteEquiv.decidableEq
 
 /-- The "discrete" category on a type, whose morphisms are equalities.
 
@@ -83,7 +86,7 @@ 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
+  comp {X Y Z} g f := by
     cases X
     cases Y
     cases Z
@@ -106,14 +109,22 @@ instance [Subsingleton α] : Subsingleton (Discrete α) :=
 
 /- ./././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
+--unsafe def _root_.tactic.discrete_cases : tactic Unit :=
+--  sorry
+--#align tactic.discrete_cases tactic.discrete_cases
+
+
+--run_cmd
+--  add_interactive [`` tactic.discrete_cases]
 
-run_cmd
-  add_interactive [`` tactic.discrete_cases]
+--attribute [local tidy] tactic.discrete_cases
+--`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), plift _]]
 
-attribute [local tidy] tactic.discrete_cases
+--macro (name := discrete_cases) "discrete_cases" : tactic =>
+--  `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
+
+macro "discrete_cases": tactic =>
+  `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
 
 instance [Unique α] : Unique (Discrete α) :=
   Unique.mk' (Discrete α)
@@ -125,7 +136,7 @@ theorem eq_of_hom {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as :=
 
 /-- Promote an equation between the wrapped terms in `X Y : discrete α` to a morphism `X ⟶ Y`
 in the discrete category. -/
-abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
+protected abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
   eqToHom
     (by
       ext
@@ -134,7 +145,7 @@ abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
 
 /-- Promote an equation between the wrapped terms in `X Y : discrete α` to an isomorphism `X ≅ Y`
 in the discrete category. -/
-abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y :=
+protected abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y :=
   eqToIso
     (by
       ext
@@ -143,12 +154,12 @@ abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y :=
 
 /-- 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 :=
-  eqToHom h
+  Discrete.eqToHom h
 #align category_theory.discrete.eq_to_hom' CategoryTheory.Discrete.eqToHom'
 
 /-- A variant of `eq_to_iso` that lifts terms to the discrete category. -/
 abbrev eqToIso' {a b : α} (h : a = b) : Discrete.mk a ≅ Discrete.mk b :=
-  eqToIso h
+  Discrete.eqToIso h
 #align category_theory.discrete.eq_to_iso' CategoryTheory.Discrete.eqToIso'
 
 @[simp]
@@ -159,7 +170,7 @@ theorem id_def (X : Discrete α) : ULift.up (PLift.up (Eq.refl X.as)) = 𝟙 X :
 variable {C : Type u₂} [Category.{v₂} C]
 
 instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f :=
-  ⟨⟨eqToHom (eq_of_hom f).symm, by tidy⟩⟩
+  ⟨⟨Discrete.eqToHom (eq_of_hom f).symm, by aesop_cat⟩⟩
 
 /- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[] -/
 /-- Any function `I → C` gives a functor `discrete I ⥤ C`.
@@ -167,12 +178,14 @@ instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f :=
 def functor {I : Type u₁} (F : I → C) : Discrete I ⥤ C
     where
   obj := F ∘ Discrete.as
-  map X Y f :=
-    by
-    trace
-      "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
-    cases f
-    exact 𝟙 (F X)
+  map {X Y} f := by
+    dsimp
+    rcases f with ⟨⟨h⟩⟩
+    exact eqToHom (congrArg _ h)
+  map_id := by aesop_cat
+  map_comp := fun {X Y Z} f g => by
+    discrete_cases
+    aesop_cat
 #align category_theory.discrete.functor CategoryTheory.Discrete.functor
 
 @[simp]
@@ -182,7 +195,7 @@ theorem functor_obj {I : Type u₁} (F : I → C) (i : I) :
 #align category_theory.discrete.functor_obj CategoryTheory.Discrete.functor_obj
 
 theorem functor_map {I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i) :
-    (Discrete.functor F).map f = 𝟙 (F i.as) := by tidy
+    (Discrete.functor F).map f = 𝟙 (F i.as) := by aesop_cat
 #align category_theory.discrete.functor_map CategoryTheory.Discrete.functor_map
 
 /-- The discrete functor induced by a composition of maps can be written as a
@@ -191,7 +204,7 @@ composition of two discrete functors.
 @[simps]
 def functorComp {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) :
     Discrete.functor (f ∘ g) ≅ Discrete.functor (Discrete.mk ∘ g) ⋙ Discrete.functor f :=
-  NatIso.ofComponents (fun X => Iso.refl _) (by tidy)
+  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 #[] -/
@@ -203,11 +216,11 @@ 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' X Y g :=
-    by
-    trace
-      "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
-    cases g
+  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
 
@@ -218,17 +231,17 @@ 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 X Y g =>
-    by
-    trace
-      "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
-    cases g
+  NatIso.ofComponents f fun g => by
+    rcases g with ⟨⟨g⟩⟩
+    discrete_cases
+    rcases g
+    change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
     simp
 #align category_theory.discrete.nat_iso CategoryTheory.Discrete.natIso
 
 @[simp]
 theorem natIso_app {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F.obj i ≅ G.obj i)
-    (i : Discrete I) : (Discrete.natIso f).app i = f i := by tidy
+    (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 #[] -/
@@ -236,11 +249,7 @@ theorem natIso_app {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discret
   `discrete.functor (F.obj)`. -/
 @[simp]
 def natIsoFunctor {I : Type u₁} {F : Discrete I ⥤ C} : F ≅ Discrete.functor (F.obj ∘ Discrete.mk) :=
-  natIso fun i =>
-    by
-    trace
-      "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
-    rfl
+  natIso fun _ => Iso.refl _
 #align category_theory.discrete.nat_iso_functor CategoryTheory.Discrete.natIsoFunctor
 
 /-- Composing `discrete.functor F` with another functor `G` amounts to composing `F` with `G.obj` -/
@@ -258,21 +267,19 @@ an equivalence between the corresponding `discrete` categories.
 @[simps]
 def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J
     where
-  Functor := Discrete.functor (Discrete.mk ∘ (e : I → J))
+  functor := Discrete.functor (Discrete.mk ∘ (e : I → J))
   inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I))
   unitIso :=
     Discrete.natIso fun i =>
       eqToIso
         (by
-          trace
-            "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+          discrete_cases
           simp)
   counitIso :=
     Discrete.natIso fun j =>
       eqToIso
         (by
-          trace
-            "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
+          discrete_cases
           simp)
 #align category_theory.discrete.equivalence CategoryTheory.Discrete.equivalence
 
@@ -280,10 +287,10 @@ def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ D
 @[simps]
 def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β
     where
-  toFun := Discrete.as ∘ h.Functor.obj ∘ Discrete.mk
+  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.unit_iso.app (discrete.mk a)).2
-  right_inv a := by simpa using eq_of_hom (h.counit_iso.app (discrete.mk a)).1
+  left_inv a := by simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2
+  right_inv a := by simpa using eq_of_hom (h.counitIso.app (Discrete.mk a)).1
 #align category_theory.discrete.equiv_of_equivalence CategoryTheory.Discrete.equivOfEquivalence
 
 end Discrete
@@ -298,27 +305,36 @@ open Opposite
 /- ./././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 α := by
+@[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
+      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 _)
+/-
   refine'
-    equivalence.mk (functor.left_op F) F _
-      (discrete.nat_iso fun X =>
+    Equivalence.mk (F.leftOp) F _
+      (Discrete.natIso fun X =>
         by
-        trace
-          "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
-        simp [F])
+          discrete_cases
+          rfl)
   refine'
-    nat_iso.of_components
+    NatIso.ofComponents
       (fun X =>
         by
-        run_tac
-          tactic.op_induction'
-        trace
-          "./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[]"
-        simp [F])
-      _
-  tidy
+        discrete_cases
+        induction X using Opposite.rec
+        discrete_cases
+        exact Iso.refl _)
+-/
+
 #align category_theory.discrete.opposite CategoryTheory.Discrete.opposite
 
 variable {C : Type u₂} [Category.{v₂} C]
@@ -327,9 +343,8 @@ variable {C : Type u₂} [Category.{v₂} C]
 theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F.map f = 𝟙 (F.obj j) :=
   by
   have h : f = 𝟙 j := by
-    cases f
-    cases f
-    ext
+    rcases f with ⟨⟨f⟩⟩
+    rfl
   rw [h]
   simp
 #align category_theory.discrete.functor_map_id CategoryTheory.Discrete.functor_map_id
@@ -337,4 +352,3 @@ theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F
 end Discrete
 
 end CategoryTheory
-

From eb1464469358a6a9502a0b8ddaba399068e45293 Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Thu, 16 Feb 2023 20:14:21 -0500
Subject: [PATCH 05/14] lint

---
 Mathlib/CategoryTheory/DiscreteCategory.lean | 66 +++++++++++---------
 1 file changed, 38 insertions(+), 28 deletions(-)

diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
index eec8f2d961faf..c19ec36629f0c 100644
--- a/Mathlib/CategoryTheory/DiscreteCategory.lean
+++ b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -17,22 +17,22 @@ open Lean Meta
 /-!
 # Discrete categories
 
-We define `discrete α` as a structure containing a term `a : α` for any type `α`,
-and use this type alias to provide a `small_category` instance
+We define `Discrete α` as a structure containing a term `a : α` for any type `α`,
+and use this type alias to provide a `SmallCategory` instance
 whose only morphisms are the identities.
 
 There is an annoying technical difficulty that it has turned out to be inconvenient
 to allow categories with morphisms living in `Prop`,
-so instead of defining `X ⟶ Y` in `discrete α` as `X = Y`,
-one might define it as `plift (X = Y)`.
-In fact, to allow `discrete α` to be a `small_category`
+so instead of defining `X ⟶ Y` in `Discrete α` as `X = Y`,
+one might define it as `PLift (X = Y)`.
+In fact, to allow `Discrete α` to be a `SmallCategory`
 (i.e. with morphisms in the same universe as the objects),
-we actually define the hom type `X ⟶ Y` as `ulift (plift (X = Y))`.
+we actually define the hom type `X ⟶ Y` as `ULift (PLift (X = Y))`.
 
-`discrete.functor` promotes a function `f : I → C` (for any category `C`) to a functor
-`discrete.functor f : discrete I ⥤ C`.
+`Discrete.functor` promotes a function `f : I → C` (for any category `C`) to a functor
+`Discrete.functor f : Discrete I ⥤ C`.
 
-Similarly, `discrete.nat_trans` and `discrete.nat_iso` promote `I`-indexed families of morphisms,
+Similarly, `Discrete.natTrans` and `Discrete.natIso` promote `I`-indexed families of morphisms,
 or `I`-indexed families of isomorphisms to natural transformations or natural isomorphism.
 
 We show equivalences of types are the same as (categorical) equivalences of the corresponding
@@ -42,17 +42,20 @@ discrete categories.
 
 namespace CategoryTheory
 
--- morphism levels before object levels. See note [category_theory universes].
+-- morphism levels before object levels. See note [CategoryTheory universes].
 universe v₁ v₂ v₃ u₁ u₁' u₂ u₃
 
 -- This is intentionally a structure rather than a type synonym
--- to enforce using `discrete_equiv` (or `discrete.mk` and `discrete.as`) to move between
+-- to enforce using `DiscreteEquiv` (or `Discrete.mk` and `Discrete.as`) to move between
 -- `discrete α` and `α`. Otherwise there is too much API leakage.
 /-- A wrapper for promoting any type to a category,
 with the only morphisms being equalities.
 -/
 @[ext]
 structure Discrete (α : Type u₁) where
+  /-- A wrapper for promoting any type to a category,
+  with the only morphisms being equalities.
+  -/
   as : α
 #align category_theory.discrete CategoryTheory.Discrete
 
@@ -62,7 +65,7 @@ theorem Discrete.mk_as {α : Type u₁} (X : Discrete α) : Discrete.mk X.as = X
   rfl
 #align category_theory.discrete.mk_as CategoryTheory.Discrete.mk_as
 
-/-- `discrete α` is equivalent to the original type `α`.-/
+/-- `Discrete α` is equivalent to the original type `α`.-/
 @[simps]
 def discreteEquiv {α : Type u₁} : Discrete α ≃ α
     where
@@ -75,10 +78,10 @@ def discreteEquiv {α : Type u₁} : Discrete α ≃ α
 instance {α : Type u₁} [DecidableEq α] : DecidableEq (Discrete α) :=
   discreteEquiv.decidableEq
 
-/-- The "discrete" category on a type, whose morphisms are equalities.
+/-- The "Discrete" category on a type, whose morphisms are equalities.
 
 Because we do not allow morphisms in `Prop` (only in `Type`),
-somewhat annoyingly we have to define `X ⟶ Y` as `ulift (plift (X = Y))`.
+somewhat annoyingly we have to define `X ⟶ Y` as `ULift (PLift (X = Y))`.
 
 See <https://stacks.math.columbia.edu/tag/001A>
 -/
@@ -122,7 +125,7 @@ instance [Subsingleton α] : Subsingleton (Discrete α) :=
 
 --macro (name := discrete_cases) "discrete_cases" : tactic =>
 --  `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
-
+/- Porting note: rewrote `discrete_cases` tactic -/
 macro "discrete_cases": tactic =>
   `(tactic|casesm* Discrete _, (_ : Discrete _) ⟶ (_ : Discrete _), PLift _)
 
@@ -134,7 +137,7 @@ theorem eq_of_hom {X Y : Discrete α} (i : X ⟶ Y) : X.as = Y.as :=
   i.down.down
 #align category_theory.discrete.eq_of_hom CategoryTheory.Discrete.eq_of_hom
 
-/-- Promote an equation between the wrapped terms in `X Y : discrete α` to a morphism `X ⟶ Y`
+/-- Promote an equation between the wrapped terms in `X Y : Discrete α` to a morphism `X ⟶ Y`
 in the discrete category. -/
 protected abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
   eqToHom
@@ -143,7 +146,7 @@ protected abbrev eqToHom {X Y : Discrete α} (h : X.as = Y.as) : X ⟶ Y :=
       exact h)
 #align category_theory.discrete.eq_to_hom CategoryTheory.Discrete.eqToHom
 
-/-- Promote an equation between the wrapped terms in `X Y : discrete α` to an isomorphism `X ≅ Y`
+/-- Promote an equation between the wrapped terms in `X Y : Discrete α` to an isomorphism `X ≅ Y`
 in the discrete category. -/
 protected abbrev eqToIso {X Y : Discrete α} (h : X.as = Y.as) : X ≅ Y :=
   eqToIso
@@ -157,7 +160,7 @@ 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'
 
-/-- A variant of `eq_to_iso` that lifts terms to the discrete category. -/
+/-- A variant of `eqToIso` that lifts terms to the discrete category. -/
 abbrev eqToIso' {a b : α} (h : a = b) : Discrete.mk a ≅ Discrete.mk b :=
   Discrete.eqToIso h
 #align category_theory.discrete.eq_to_iso' CategoryTheory.Discrete.eqToIso'
@@ -172,8 +175,9 @@ 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⟩⟩
 
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[] -/
-/-- Any function `I → C` gives a functor `discrete I ⥤ C`.
+/- ./././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
@@ -201,13 +205,14 @@ theorem functor_map {I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i)
 /-- The discrete functor induced by a composition of maps can be written as a
 composition of two discrete functors.
 -/
-@[simps]
+@[simps!]
 def functorComp {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) :
     Discrete.functor (f ∘ g) ≅ Discrete.functor (Discrete.mk ∘ g) ⋙ Discrete.functor f :=
   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 #[] -/
+/- ./././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.
@@ -224,12 +229,13 @@ def natTrans {I : Type u₁} {F G : Discrete I ⥤ C} (f : ∀ i : Discrete I, F
     simp
 #align category_theory.discrete.nat_trans CategoryTheory.Discrete.natTrans
 
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[] -/
+/- ./././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]
+@[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
     rcases g with ⟨⟨g⟩⟩
@@ -244,7 +250,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 #[] -/
+/- ./././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]
@@ -256,11 +263,13 @@ def natIsoFunctor {I : Type u₁} {F : Discrete I ⥤ C} : F ≅ Discrete.functo
 @[simp]
 def compNatIsoDiscrete {I : Type u₁} {D : Type u₃} [Category.{v₃} D] (F : I → C) (G : C ⥤ D) :
     Discrete.functor F ⋙ G ≅ Discrete.functor (G.obj ∘ F) :=
-  natIso fun i => Iso.refl _
+  natIso fun _ => Iso.refl _
 #align category_theory.discrete.comp_nat_iso_discrete CategoryTheory.Discrete.compNatIsoDiscrete
 
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[] -/
-/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:76:14: unsupported tactic `discrete_cases #[] -/
+/- ./././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.
 -/
@@ -352,3 +361,4 @@ theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F
 end Discrete
 
 end CategoryTheory
+

From 38a89b87e6655d9e89c6b89032e22096d94d24b5 Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Thu, 16 Feb 2023 20:20:24 -0500
Subject: [PATCH 06/14] lint some more

---
 Mathlib/CategoryTheory/DiscreteCategory.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
index c19ec36629f0c..cac60eb13ddee 100644
--- a/Mathlib/CategoryTheory/DiscreteCategory.lean
+++ b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -12,8 +12,6 @@ import Mathlib.CategoryTheory.EqToHom
 import Mathlib.Data.ULift
 import Mathlib.Tactic.CasesM
 
-open Lean Meta
-
 /-!
 # Discrete categories
 
@@ -39,7 +37,6 @@ We show equivalences of types are the same as (categorical) equivalences of the
 discrete categories.
 -/
 
-
 namespace CategoryTheory
 
 -- morphism levels before object levels. See note [CategoryTheory universes].
@@ -310,9 +307,12 @@ 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 #[] -/
+/- ./././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 α :=

From 89d269be2e063336c71b9e3fd523f8e77656e40b Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Sat, 18 Feb 2023 17:51:44 -0500
Subject: [PATCH 07/14] feat: port CategoryTheory.Pempty


From 116924e15052f809f58f715a269e874e1d71796a Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Sat, 18 Feb 2023 17:51:45 -0500
Subject: [PATCH 08/14] Initial file copy from mathport

---
 Mathlib/CategoryTheory/Pempty.lean | 67 ++++++++++++++++++++++++++++++
 1 file changed, 67 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/Pempty.lean

diff --git a/Mathlib/CategoryTheory/Pempty.lean b/Mathlib/CategoryTheory/Pempty.lean
new file mode 100644
index 0000000000000..9d0c538b12753
--- /dev/null
+++ b/Mathlib/CategoryTheory/Pempty.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2018 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Bhavik Mehta
+
+! This file was ported from Lean 3 source module category_theory.pempty
+! leanprover-community/mathlib commit 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathbin.CategoryTheory.DiscreteCategory
+
+/-!
+# The empty category
+
+Defines a category structure on `pempty`, and the unique functor `pempty ⥤ C` for any category `C`.
+-/
+
+
+universe w v u
+
+-- morphism levels before object levels. See note [category_theory universes].
+namespace CategoryTheory
+
+namespace Functor
+
+variable (C : Type u) [Category.{v} C]
+
+/-- Equivalence between two empty categories. -/
+def emptyEquivalence : Discrete.{w} PEmpty ≌ Discrete.{v} PEmpty :=
+  Equivalence.mk
+    { obj := PEmpty.elim ∘ Discrete.as
+      map := fun x => x.as.elim }
+    { obj := PEmpty.elim ∘ Discrete.as
+      map := fun x => x.as.elim } (by tidy) (by tidy)
+#align category_theory.functor.empty_equivalence CategoryTheory.Functor.emptyEquivalence
+
+/-- The canonical functor out of the empty category. -/
+def empty : Discrete.{w} PEmpty ⥤ C :=
+  Discrete.functor PEmpty.elim
+#align category_theory.functor.empty CategoryTheory.Functor.empty
+
+variable {C}
+
+/-- Any two functors out of the empty category are isomorphic. -/
+def emptyExt (F G : Discrete.{w} PEmpty ⥤ C) : F ≅ G :=
+  Discrete.natIso fun x => x.as.elim
+#align category_theory.functor.empty_ext CategoryTheory.Functor.emptyExt
+
+/-- Any functor out of the empty category is isomorphic to the canonical functor from the empty
+category.
+-/
+def uniqueFromEmpty (F : Discrete.{w} PEmpty ⥤ C) : F ≅ empty C :=
+  emptyExt _ _
+#align category_theory.functor.unique_from_empty CategoryTheory.Functor.uniqueFromEmpty
+
+/-- Any two functors out of the empty category are *equal*. You probably want to use
+`empty_ext` instead of this.
+-/
+theorem empty_ext' (F G : Discrete.{w} PEmpty ⥤ C) : F = G :=
+  Functor.ext (fun x => x.as.elim) fun x _ _ => x.as.elim
+#align category_theory.functor.empty_ext' CategoryTheory.Functor.empty_ext'
+
+end Functor
+
+end CategoryTheory
+

From 8f265493a7b40a7ae57d7c68132e7b8def5ff01d Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Sat, 18 Feb 2023 17:51:45 -0500
Subject: [PATCH 09/14] automated fixes

Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
---
 Mathlib.lean                       | 1 +
 Mathlib/CategoryTheory/Pempty.lean | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index ec950a70e951a..c1934952df348 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -252,6 +252,7 @@ import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.NatTrans
 import Mathlib.CategoryTheory.Opposites
+import Mathlib.CategoryTheory.Pempty
 import Mathlib.CategoryTheory.Pi.Basic
 import Mathlib.CategoryTheory.Products.Associator
 import Mathlib.CategoryTheory.Products.Basic
diff --git a/Mathlib/CategoryTheory/Pempty.lean b/Mathlib/CategoryTheory/Pempty.lean
index 9d0c538b12753..d749cdd535783 100644
--- a/Mathlib/CategoryTheory/Pempty.lean
+++ b/Mathlib/CategoryTheory/Pempty.lean
@@ -8,7 +8,7 @@ Authors: Scott Morrison, Bhavik Mehta
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
-import Mathbin.CategoryTheory.DiscreteCategory
+import Mathlib.CategoryTheory.DiscreteCategory
 
 /-!
 # The empty category

From 6fc9d7741782f66c8916db018ec97a9cc8469ae6 Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Sat, 18 Feb 2023 18:39:33 -0500
Subject: [PATCH 10/14] fix errors; lint

---
 Mathlib/CategoryTheory/Pempty.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Pempty.lean b/Mathlib/CategoryTheory/Pempty.lean
index dfb04beb3c78d..d42280da79939 100644
--- a/Mathlib/CategoryTheory/Pempty.lean
+++ b/Mathlib/CategoryTheory/Pempty.lean
@@ -74,7 +74,7 @@ def uniqueFromEmpty (F : Discrete.{w} PEmpty ⥤ C) : F ≅ empty C :=
 #align category_theory.functor.unique_from_empty CategoryTheory.Functor.uniqueFromEmpty
 
 /-- Any two functors out of the empty category are *equal*. You probably want to use
-`empty_ext` instead of this.
+`emptyExt` instead of this.
 -/
 theorem empty_ext' (F G : Discrete.{w} PEmpty ⥤ C) : F = G :=
   Functor.ext (fun x => x.as.elim) fun x _ _ => x.as.elim

From 89f4cac03e62f4db31519157ab05b58d363bc876 Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Sat, 18 Feb 2023 18:44:25 -0500
Subject: [PATCH 11/14] remove extra porting script

---
 scripts/start_port-macos.sh | 86 -------------------------------------
 1 file changed, 86 deletions(-)
 delete mode 100755 scripts/start_port-macos.sh

diff --git a/scripts/start_port-macos.sh b/scripts/start_port-macos.sh
deleted file mode 100755
index da56887ff18fb..0000000000000
--- a/scripts/start_port-macos.sh
+++ /dev/null
@@ -1,86 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-if [ ! -d Mathlib ] ; then
-    echo "No Mathlib/ directory; are you at the root of the mathlib4 repo?"
-    exit 1
-fi
-
-if [ ! $1 ] ; then
-    echo "usage: ./scripts/start_port.sh Mathlib/Foo/Bar/Baz.lean"
-    exit 1
-fi
-
-case $1 in
-    Mathlib/*) true ;;
-    *) echo "argument must begin with Mathlib/"
-       exit 1 ;;
-esac
-
-if [ -f $1 ] ; then
-    echo "file already exists"
-    exit 1
-fi
-
-set -x
-set -o pipefail
-
-MATHLIB3PORT_BASE_URL=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master
-PORT_STATUS_YAML=https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
-TMP_FILE=start_port_tmp.lean
-
-mathlib4_path=$1
-mathlib4_mod=$(basename $(echo "$mathlib4_path" | tr / .) .lean)
-
-mathlib3port_url=$MATHLIB3PORT_BASE_URL/Mathbin/${1#Mathlib/}
-
-curl --silent --show-error --fail -o "$TMP_FILE" "$mathlib3port_url"
-
-mathlib3_module=$(grep '^! .*source module ' <"$TMP_FILE" | gsed 's/.*source module \(.*\)$/\1/')
-
-if curl --silent --show-error --fail "$PORT_STATUS_YAML" | grep -F "$mathlib3_module: " | grep "mathlib4#" ; then
-    set +x
-    echo "WARNING: The file is already in the process of being ported."
-    echo "(See line above for PR number.)"
-    rm "$TMP_FILE"
-    exit 1
-fi
-
-mkdir -p $(dirname "$mathlib4_path")
-mv "$TMP_FILE" "$mathlib4_path"
-
-git fetch
-mathlib4_mod_tail=${mathlib4_mod#Mathlib.}
-branch_name=port/${mathlib4_mod_tail}
-git checkout --no-track -b "$branch_name" origin/master
-
-# Empty commit with nice title. Ugsed by gh and hub to suggest PR title.
-git commit -m "feat: port $mathlib4_mod_tail" --allow-empty
-
-git add "$mathlib4_path"
-git commit -m 'Initial file copy from mathport'
-
-gsed -i 's/Mathbin\./Mathlib\./g' "$mathlib4_path"
-gsed -i '/^import/{s/[.]Gcd/.GCD/g; s/[.]Modeq/.ModEq/g; s/[.]Nary/.NAry/g; s/[.]Peq/.PEq/g; s/[.]Pfun/.PFun/g; s/[.]Pnat/.PNat/g; s/[.]Smul/.SMul/g; s/[.]Zmod/.ZMod/g}' "$mathlib4_path"
-
-# gawk script taken from https://github.com/leanprover-community/mathlib4/pull/1523
-gawk '{do {{if (match($0, "^  by$") && length(p) < 98 && (!(match(p, "^[ \t]*--.*$")))) {p=p " by";} else {if (NR!=1) {print p}; p=$0}}} while (getline == 1) if (getline==0) print p}' "$mathlib4_path" > "$mathlib4_path.tmp"
-mv "$mathlib4_path.tmp" "$mathlib4_path"
-
-(echo "import $mathlib4_mod" ; cat Mathlib.lean) | LC_ALL=C sort | uniq > Mathlib.lean.tmp
-mv -f Mathlib.lean.tmp Mathlib.lean
-
-git add Mathlib.lean "$mathlib4_path"
-git commit \
-	-m 'automated fixes' \
-	-m '' \
-	-m 'Mathbin -> Mathlib' \
-	-m 'fix certain import statements' \
-	-m 'move "by" to end of line' \
-	-m 'add import to Mathlib.lean'
-
-set +x
-
-echo "After pushing, you can open a PR at:"
-echo "https://github.com/leanprover-community/mathlib4/compare/$branch_name?expand=1&title=feat:+port+$mathlib4_mod_tail&labels=mathlib-port"

From 9bf1cef8ca50c511a2c060a0074f0342ba9c0a82 Mon Sep 17 00:00:00 2001
From: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
Date: Tue, 21 Feb 2023 14:23:24 -0500
Subject: [PATCH 12/14] Update Pempty.lean

---
 Mathlib/CategoryTheory/Pempty.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Pempty.lean b/Mathlib/CategoryTheory/Pempty.lean
index d42280da79939..f8808251bb3d1 100644
--- a/Mathlib/CategoryTheory/Pempty.lean
+++ b/Mathlib/CategoryTheory/Pempty.lean
@@ -16,9 +16,9 @@ import Mathlib.CategoryTheory.DiscreteCategory
 Defines a category structure on `PEmpty`, and the unique functor `PEmpty ⥤ C` for any category `C`.
 -/
 
+-- Porting note: this file stressed Lean a good deal despite its length
 
 universe w v u
-
 -- morphism levels before object levels. See note [CategoryTheory universes].
 namespace CategoryTheory
 

From 8d97fa33825ecd0cb3967b80a5175295c1d06403 Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Tue, 21 Feb 2023 14:34:51 -0500
Subject: [PATCH 13/14] fix casing on name step 1

---
 Mathlib/CategoryTheory/{Pempty.lean => MyPEmpty.lean} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename Mathlib/CategoryTheory/{Pempty.lean => MyPEmpty.lean} (100%)

diff --git a/Mathlib/CategoryTheory/Pempty.lean b/Mathlib/CategoryTheory/MyPEmpty.lean
similarity index 100%
rename from Mathlib/CategoryTheory/Pempty.lean
rename to Mathlib/CategoryTheory/MyPEmpty.lean

From ebe5c7a0df9febc383bcf05d1792d9e91056b2d6 Mon Sep 17 00:00:00 2001
From: Matthew Ballard <matt@mrb.email>
Date: Tue, 21 Feb 2023 14:35:33 -0500
Subject: [PATCH 14/14] fix casing issue step 2

---
 Mathlib/CategoryTheory/{MyPEmpty.lean => PEmpty.lean} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename Mathlib/CategoryTheory/{MyPEmpty.lean => PEmpty.lean} (100%)

diff --git a/Mathlib/CategoryTheory/MyPEmpty.lean b/Mathlib/CategoryTheory/PEmpty.lean
similarity index 100%
rename from Mathlib/CategoryTheory/MyPEmpty.lean
rename to Mathlib/CategoryTheory/PEmpty.lean