automated fixes

mattrobball · mattrobball · commit 2f2598496bc4 · 2023-02-24T20:50:25.000-05:00
Mathbin -&gt; Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -234,7 +234,7 @@ 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.Category.ULift
 import Mathlib.CategoryTheory.Comma
 import Mathlib.CategoryTheory.ConcreteCategory.Bundled
 import Mathlib.CategoryTheory.Equivalence
diff --git a/Mathlib/CategoryTheory/Category/ULift.lean b/Mathlib/CategoryTheory/Category/ULift.lean
@@ -11,110 +11,110 @@ Authors: Adam Topaz
 import Mathlib.CategoryTheory.Category.Basic
 import Mathlib.CategoryTheory.Equivalence
 import Mathlib.CategoryTheory.EqToHom
+import Mathlib.Data.ULift
 
 /-!
-# Basic API for ulift
+# 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.
+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`.
+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
+# ULiftHom
 
-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`.
+Given a type `C : Type u`, `ULiftHom.{w} C` is just an alias for `C`.
+If we have `category.{v} C`, then `ULiftHom.{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`.
+This is a category equivalent to `C`. The forward direction of the equivalence is `ULiftHom.up`,
+the backward direction is `ULiftHom.donw` and the equivalence is `ULiftHom.equiv`.
 
-# as_small
+# AsSmall
 
 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`.
+`AsSmall.{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`.
+The forward direction of the equivalence, `C ⥤ AsSmall C`, is denoted `AsSmall.up`
+and the backward direction is `AsSmall.down`. The equivalence itself is `AsSmall.equiv`.
 -/
 
-
 universe w₁ v₁ v₂ u₁ u₂
 
 namespace CategoryTheory
 
 variable {C : Type u₁} [Category.{v₁} C]
 
-/-- The functorial version of `ulift.up`. -/
+/-- The functorial version of `ULift.up`. -/
 @[simps]
 def Ulift.upFunctor : C ⥤ ULift.{u₂} C where
   obj := ULift.up
-  map X Y f := f
+  map f := f
 #align category_theory.ulift.up_functor CategoryTheory.Ulift.upFunctor
 
-/-- The functorial version of `ulift.down`. -/
+/-- 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 X Y f := f
+  map f := f
 #align category_theory.ulift.down_functor CategoryTheory.Ulift.downFunctor
 
-/-- The categorical equivalence between `C` and `ulift C`. -/
+/-- The categorical equivalence between `C` and `ULift C`. -/
 @[simps]
-def Ulift.equivalence : C ≌ ULift.{u₂} C
-    where
-  Functor := Ulift.upFunctor
+def Ulift.equivalence : C ≌ ULift.{u₂} C where
+  functor := Ulift.upFunctor
   inverse := Ulift.downFunctor
   unitIso :=
-    { Hom := 𝟙 _
+    { hom := 𝟙 _
       inv := 𝟙 _ }
   counitIso :=
-    { Hom :=
+    { hom :=
         { app := fun X => 𝟙 _
-          naturality' := fun X Y f => by
+          naturality := fun X Y f => by
             change f ≫ 𝟙 _ = 𝟙 _ ≫ f
             simp }
       inv :=
         { app := fun X => 𝟙 _
-          naturality' := fun X Y f => by
+          naturality := fun X Y f => by
             change f ≫ 𝟙 _ = 𝟙 _ ≫ f
             simp }
-      hom_inv_id' := by
+      hom_inv_id := by
         ext
         change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
         simp
-      inv_hom_id' := by
+      inv_hom_id := by
         ext
         change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
         simp }
-  functor_unitIso_comp' X := by
+  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`.
+/- 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) :=
+def UliftHom.{w,u} (C : Type u) : Type u := 
+  let _ := ULift.{w} C 
   C
 #align category_theory.ulift_hom CategoryTheory.UliftHom
 
 instance {C} [Inhabited C] : Inhabited (UliftHom C) :=
-  ⟨(Inhabited.default C : C)⟩
+  ⟨(default : C)⟩
 
-/-- The obvious function `ulift_hom C → C`. -/
+/-- The obvious function `ULiftHom 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`. -/
+/-- The obvious function `C → ULiftHom C`. -/
 def UliftHom.objUp {C} (A : C) : UliftHom C :=
   A
 #align category_theory.ulift_hom.obj_up CategoryTheory.UliftHom.objUp
@@ -129,91 +129,89 @@ 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 A B C f g := ⟨f.down ≫ g.down⟩
+  comp f g := ⟨f.down ≫ g.down⟩
 
-/-- One half of the quivalence between `C` and `ulift_hom C`. -/
+/-- One half of the quivalence between `C` and `ULiftHom C`. -/
 @[simps]
 def UliftHom.up : C ⥤ UliftHom C where
   obj := UliftHom.objUp
-  map X Y f := ⟨f⟩
+  map f := ⟨f⟩
 #align category_theory.ulift_hom.up CategoryTheory.UliftHom.up
 
-/-- One half of the quivalence between `C` and `ulift_hom C`. -/
+/-- One half of the quivalence between `C` and `ULiftHom C`. -/
 @[simps]
 def UliftHom.down : UliftHom C ⥤ C where
   obj := UliftHom.objDown
-  map X Y f := f.down
+  map 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
+/-- The equivalence between `C` and `ULiftHom 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)
+  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
 
 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
+/- 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. -/
+/-- `AsSmall C` is a small category equivalent to `C`.
+  More specifically, if `C : Type u` is endowed with `Category.{v} C`, then
+  `AsSmall.{w} C : Type (max w v u)` is endowed with an instance of a small category.
+
+  The objects and morphisms of `AsSmall 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
+@[nolint unusedArguments]
+def AsSmall.{w, v, u} (D : Type u) [Category.{v} D] := ULift.{max w v} D
 #align category_theory.as_small CategoryTheory.AsSmall
 
-instance : SmallCategory (AsSmall.{w₁} C)
-    where
+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⟩
+  comp f g := ⟨f.down ≫ g.down⟩
 
-/-- One half of the equivalence between `C` and `as_small C`. -/
+/-- One half of the equivalence between `C` and `AsSmall C`. -/
 @[simps]
 def AsSmall.up : C ⥤ AsSmall C where
   obj X := ⟨X⟩
-  map X Y f := ⟨f⟩
+  map f := ⟨f⟩
 #align category_theory.as_small.up CategoryTheory.AsSmall.up
 
-/-- One half of the equivalence between `C` and `as_small C`. -/
+/-- One half of the equivalence between `C` and `AsSmall C`. -/
 @[simps]
 def AsSmall.down : AsSmall C ⥤ C where
-  obj X := X.down
-  map X Y f := f.down
+  obj X := ULift.down X
+  map f := f.down
 #align category_theory.as_small.down CategoryTheory.AsSmall.down
 
-/-- The equivalence between `C` and `as_small C`. -/
+/-- The equivalence between `C` and `AsSmall C`. -/
 @[simps]
 def AsSmall.equiv : C ≌ AsSmall C where
-  Functor := AsSmall.up
+  functor := AsSmall.up
   inverse := AsSmall.down
-  unitIso := NatIso.ofComponents (fun X => eqToIso rfl) (by tidy)
+  unitIso := NatIso.ofComponents (fun X => eqToIso rfl) (by aesop_cat)
   counitIso :=
     NatIso.ofComponents
       (fun X =>
         eqToIso <| by
-          ext
+          apply ULift.ext
           rfl)
-      (by tidy)
+      (by aesop_cat)
 #align category_theory.as_small.equiv CategoryTheory.AsSmall.equiv
 
 instance [Inhabited C] : Inhabited (AsSmall C) :=
-  ⟨⟨Inhabited.default _⟩⟩
+  ⟨⟨default⟩⟩
 
-/-- The equivalence between `C` and `ulift_hom (ulift C)`. -/
+/-- 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
diff --git a/Mathlib/CategoryTheory/Equivalence.lean b/Mathlib/CategoryTheory/Equivalence.lean
@@ -89,8 +89,8 @@ 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_unit_iso_comp : 
-    ∀ X : C, functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 
+  functor_unitIso_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
 
@@ -124,7 +124,7 @@ 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
@@ -154,7 +154,7 @@ theorem equivalence_mk'_counitInv (functor inverse unit_iso counit_iso f) :
 @[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
+  e.functor_unitIso_comp X
 #align category_theory.equivalence.functor_unit_comp CategoryTheory.Equivalence.functor_unit_comp
 
 @[simp]
@@ -321,7 +321,7 @@ def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E
   -- 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
+  functor_unitIso_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]
@@ -511,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_unit_iso_comp :
+  functor_unitIso_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_unit_iso_comp
+attribute [reassoc (attr := simp)] IsEquivalence.functor_unitIso_comp
 
 namespace IsEquivalence
 
@@ -546,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_unit_iso_comp⟩
+    IsEquivalence.functor_unitIso_comp⟩
 #align category_theory.functor.as_equivalence CategoryTheory.Functor.asEquivalence
 
 instance isEquivalenceRefl : IsEquivalence (𝟭 C) :=
@@ -654,15 +654,15 @@ 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_unit_iso_comp X := by
+  functor_unitIso_comp X := by
     dsimp [NatIso.hcomp]
     erw [id_comp, F.map_id, comp_id]
     apply (cancel_epi (e.hom.app X)).mp
     slice_lhs 1 2 => rw [← e.hom.naturality]
     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_unit_iso_comp]
+    slice_lhs 1 2 => rw [functor_unitIso_comp]
     simp only [Functor.id_map, id_comp]
 #align category_theory.is_equivalence.of_iso CategoryTheory.IsEquivalence.ofIso
 
diff --git a/Mathlib/CategoryTheory/Products/Basic.lean b/Mathlib/CategoryTheory/Products/Basic.lean
@@ -353,7 +353,7 @@ def functorProdFunctorEquivCounitIso :
     (by aesop_cat)
 #align category_theory.functor_prod_functor_equiv_counit_iso CategoryTheory.functorProdFunctorEquivCounitIso
 
-/- Porting note: unlike with Lean 3, we needed to provide `functor_unitIso_comp` because
+/- Porting note: unlike with Lean 3, we needed to provide `functor_unitIso_comp` because 
 Lean 4 could not see through `functorProdFunctorEquivUnitIso` (or the co-unit version) 
 to run the auto tactic `by aesop_cat` -/
 
