add updated files

mattrobball · mattrobball · commit 9dfd1d9c229a · 2023-02-24T20:50:25.000-05:00
diff --git a/Mathlib/CategoryTheory/Category/ULift.lean b/Mathlib/CategoryTheory/Category/ULift.lean
@@ -51,23 +51,23 @@ variable {C : Type u₁} [Category.{v₁} C]
 
 /-- The functorial version of `ULift.up`. -/
 @[simps]
-def Ulift.upFunctor : C ⥤ ULift.{u₂} C where
+def ULift.upFunctor : C ⥤ ULift.{u₂} C where
   obj := ULift.up
   map f := f
-#align category_theory.ulift.up_functor CategoryTheory.Ulift.upFunctor
+#align category_theory.ulift.up_functor CategoryTheory.ULift.upFunctor
 
 /-- The functorial version of `ULift.down`. -/
 @[simps]
-def Ulift.downFunctor : ULift.{u₂} C ⥤ C where
+def ULift.downFunctor : ULift.{u₂} C ⥤ C where
   obj := ULift.down
   map f := f
-#align category_theory.ulift.down_functor CategoryTheory.Ulift.downFunctor
+#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
+def ULift.equivalence : C ≌ ULift.{u₂} C where
+  functor := ULift.upFunctor
+  inverse := ULift.downFunctor
   unitIso :=
     { hom := 𝟙 _
       inv := 𝟙 _ }
@@ -93,70 +93,70 @@ def Ulift.equivalence : C ≌ ULift.{u₂} C where
   functor_unitIso_comp X := by
     change 𝟙 X ≫ 𝟙 X = 𝟙 X
     simp
-#align category_theory.ulift.equivalence CategoryTheory.Ulift.equivalence
+#align category_theory.ulift.equivalence CategoryTheory.ULift.equivalence
 
-section UliftHom
+section ULiftHom
 /- Porting note: obviously we don't want code that looks like this long term 
 the ability to turn off unused universe parameter error is desirable -/
 /-- `ULiftHom.{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) : Type u := 
+def ULiftHom.{w,u} (C : Type u) : Type u := 
   let _ := ULift.{w} C 
   C
-#align category_theory.ulift_hom CategoryTheory.UliftHom
+#align category_theory.ulift_hom CategoryTheory.ULiftHom
 
-instance {C} [Inhabited C] : Inhabited (UliftHom C) :=
+instance {C} [Inhabited C] : Inhabited (ULiftHom C) :=
   ⟨(default : C)⟩
 
 /-- The obvious function `ULiftHom C → C`. -/
-def UliftHom.objDown {C} (A : UliftHom C) : C :=
+def ULiftHom.objDown {C} (A : ULiftHom C) : C :=
   A
-#align category_theory.ulift_hom.obj_down CategoryTheory.UliftHom.objDown
+#align category_theory.ulift_hom.obj_down CategoryTheory.ULiftHom.objDown
 
 /-- The obvious function `C → ULiftHom C`. -/
-def UliftHom.objUp {C} (A : C) : UliftHom C :=
+def ULiftHom.objUp {C} (A : C) : ULiftHom C :=
   A
-#align category_theory.ulift_hom.obj_up CategoryTheory.UliftHom.objUp
+#align category_theory.ulift_hom.obj_up CategoryTheory.ULiftHom.objUp
 
 @[simp]
-theorem objDown_objUp {C} (A : C) : (UliftHom.objUp A).objDown = A :=
+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 :=
+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
+instance : Category.{max v₂ v₁} (ULiftHom.{v₂} C) where
   Hom A B := ULift.{v₂} <| A.objDown ⟶ B.objDown
   id A := ⟨𝟙 _⟩
   comp f g := ⟨f.down ≫ g.down⟩
 
 /-- One half of the quivalence between `C` and `ULiftHom C`. -/
 @[simps]
-def UliftHom.up : C ⥤ UliftHom C where
-  obj := UliftHom.objUp
+def ULiftHom.up : C ⥤ ULiftHom C where
+  obj := ULiftHom.objUp
   map f := ⟨f⟩
-#align category_theory.ulift_hom.up CategoryTheory.UliftHom.up
+#align category_theory.ulift_hom.up CategoryTheory.ULiftHom.up
 
 /-- One half of the quivalence between `C` and `ULiftHom C`. -/
 @[simps]
-def UliftHom.down : UliftHom C ⥤ C where
-  obj := UliftHom.objDown
+def ULiftHom.down : ULiftHom C ⥤ C where
+  obj := ULiftHom.objDown
   map f := f.down
-#align category_theory.ulift_hom.down CategoryTheory.UliftHom.down
+#align category_theory.ulift_hom.down CategoryTheory.ULiftHom.down
 
 /-- The equivalence between `C` and `ULiftHom C`. -/
-def UliftHom.equiv : C ≌ UliftHom C where
-  functor := UliftHom.up
-  inverse := UliftHom.down
+def ULiftHom.equiv : C ≌ ULiftHom C where
+  functor := ULiftHom.up
+  inverse := ULiftHom.down
   unitIso := NatIso.ofComponents (fun A => eqToIso rfl) (by aesop_cat)
   counitIso := NatIso.ofComponents (fun A => eqToIso rfl) (by aesop_cat)
-#align category_theory.ulift_hom.equiv CategoryTheory.UliftHom.equiv
+#align category_theory.ulift_hom.equiv CategoryTheory.ULiftHom.equiv
 
-end UliftHom
+end ULiftHom
 /- Porting note: we want to keep around the category instance on `D` 
 so Lean can figure out things further down. So `AsSmall` has been 
 nolinted. -/
@@ -211,11 +211,11 @@ def AsSmall.equiv : C ≌ AsSmall C where
 instance [Inhabited C] : Inhabited (AsSmall C) :=
   ⟨⟨default⟩⟩
 
-/-- The equivalence between `C` and `ULiftHom (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
+/-- The equivalence between `C` and `ULiftHom (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
@@ -121,7 +121,7 @@ structure LiftStruct (sq : CommSq f i p g) where
 
 namespace LiftStruct
 
-/-- A `lift_struct` for a commutative square gives a `lift_struct` for the
+/-- A `LiftStruct` for a commutative square gives a `LiftStruct` 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 `lift_struct` for a commutative square in the opposite category
-gives a `lift_struct` for the corresponding square in the original category. -/
+/-- A `LiftStruct` for a commutative square in the opposite category
+gives a `LiftStruct` 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 `lift_struct` for a square and the corresponding square
+/-- Equivalences of `LiftStruct` 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 `lift_struct` for a square in the oppositive category and
+/-- Equivalences of `LiftStruct` 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,8 +171,7 @@ 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] :
@@ -186,9 +185,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 `lift_struct`. -/
+/-- The assertion that a square has a `LiftStruct`. -/
 class HasLift : Prop where
-  /-- Square has a `lift_struct`. -/
+  /-- Square has a `LiftStruct`. -/
   exists_lift : Nonempty sq.LiftStruct
 #align category_theory.comm_sq.has_lift CategoryTheory.CommSq.HasLift
 
@@ -220,7 +219,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 `lift_struct` when
+/-- A choice of a diagonal morphism that is part of a `LiftStruct` 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
@@ -107,22 +107,15 @@ instance [Subsingleton α] : Subsingleton (Discrete α) :=
     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]
+/-
+Porting note: It seems that `aesop` currently has no way to add lemmas locally.
 
---attribute [local tidy] tactic.discrete_cases
---`[cases_matching* [discrete _, (_ : discrete _) ⟶ (_ : discrete _), plift _]]
+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 _)
 
@@ -152,7 +145,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 `eq_to_hom` that lifts terms to the discrete category. -/
+/-- A variant of `eqToHom` 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'
@@ -172,10 +165,7 @@ 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`.
--/
+/-- 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
@@ -208,8 +198,6 @@ 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.
@@ -218,24 +206,20 @@ 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
-    rcases g with ⟨⟨g⟩⟩
+  naturality := fun {X Y} ⟨⟨g⟩⟩ => by
     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
-    rcases g with ⟨⟨g⟩⟩
+  NatIso.ofComponents f fun ⟨⟨g⟩⟩ => by
     discrete_cases
     rcases g
     change F.map (𝟙 _) ≫ _ = _ ≫ G.map (𝟙 _)
@@ -247,8 +231,6 @@ 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]
@@ -263,11 +245,7 @@ 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
 
-/- ./././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
+/-- We can promote a type-level `Equiv` to
 an equivalence between the corresponding `discrete` categories.
 -/
 @[simps]
@@ -289,7 +267,7 @@ 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
@@ -307,27 +285,23 @@ 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 =>
@@ -361,4 +335,3 @@ theorem functor_map_id (F : Discrete J ⥤ C) {j : Discrete J} (f : j ⟶ j) : F
 end Discrete
 
 end CategoryTheory
-
diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
