chore: tidy various files (#2742)

Mathlib/Algebra/DirectSum/Basic.lean

@@ -20,7 +20,7 @@ This file defines the direct sum of abelian groups, indexed by a discrete type.
 ## Notation
 
 `⨁ i, β i` is the n-ary direct sum `DirectSum`.
-This notation is in the `DirectSum` locale, accessible after `open_locale DirectSum`.
+This notation is in the `DirectSum` locale, accessible after `open DirectSum`.
 
 ## References
 
@@ -35,7 +35,7 @@ variable (ι : Type v) [dec_ι : DecidableEq ι] (β : ι → Type w)
 
 /-- `DirectSum β` is the direct sum of a family of additive commutative monoids `β i`.
 
-Note: `open_locale DirectSum` will enable the notation `⨁ i, β i` for `DirectSum β`. -/
+Note: `open DirectSum` will enable the notation `⨁ i, β i` for `DirectSum β`. -/
 def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
   -- Porting note: Failed to synthesize
   -- Π₀ i, β i deriving AddCommMonoid, Inhabited

Mathlib/Algebra/Quandle.lean

@@ -69,7 +69,7 @@ The following notation is localized in `quandles`:
 * `x ◃⁻¹ y` is `Rack.inv_act x y`
 * `S →◃ S'` is `ShelfHom S S'`
 
-Use `open_locale quandles` to use these.
+Use `open quandles` to use these.
 
 ## Todo
 

Mathlib/CategoryTheory/Limits/Cones.lean

@@ -157,7 +157,7 @@ theorem Cone.w {F : J ⥤ C} (c : Cone F) {j j' : J} (f : j ⟶ j') :
 structure Cocone (F : J ⥤ C) where
   /-- An object of `C` -/
   pt : C
-  /-- A natural transformation from `F` to the constant functor at `X` -/
+  /-- A natural transformation from `F` to the constant functor at `pt` -/
   ι : F ⟶ (const J).obj pt
 #align category_theory.limits.cocone CategoryTheory.Limits.Cocone
 set_option linter.uppercaseLean3 false in
@@ -274,8 +274,7 @@ def extend (c : Cocone F) {Y : C} (f : c.pt ⟶ Y) : Cocone F where
 version.
 -/
 @[simps]
-def whisker (E : K ⥤ J) (c : Cocone F) : Cocone (E ⋙ F)
-    where
+def whisker (E : K ⥤ J) (c : Cocone F) : Cocone (E ⋙ F) where
   pt := c.pt
   ι := whiskerLeft E c.ι
 #align category_theory.limits.cocone.whisker CategoryTheory.Limits.Cocone.whisker
@@ -339,8 +338,7 @@ theorem cone_iso_of_hom_iso {K : J ⥤ C} {c d : Cone K} (f : c ⟶ d) [i : IsIs
 Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to give a cone for `G`.
 -/
 @[simps]
-def postcompose {G : J ⥤ C} (α : F ⟶ G) : Cone F ⥤ Cone G
-    where
+def postcompose {G : J ⥤ C} (α : F ⟶ G) : Cone F ⥤ Cone G where
   obj c :=
     { pt := c.pt
       π := c.π ≫ α }
@@ -365,8 +363,7 @@ def postcomposeId : postcompose (𝟙 F) ≅ 𝟭 (Cone F) :=
 cones.
 -/
 @[simps]
-def postcomposeEquivalence {G : J ⥤ C} (α : F ≅ G) : Cone F ≌ Cone G
-    where
+def postcomposeEquivalence {G : J ⥤ C} (α : F ≅ G) : Cone F ≌ Cone G where
   functor := postcompose α.hom
   inverse := postcompose α.inv
   unitIso := NatIso.ofComponents (fun s => Cones.ext (Iso.refl _) (by aesop_cat)) (by aesop_cat)
@@ -376,17 +373,15 @@ def postcomposeEquivalence {G : J ⥤ C} (α : F ≅ G) : Cone F ≌ Cone G
 /-- Whiskering on the left by `E : K ⥤ J` gives a functor from `Cone F` to `Cone (E ⋙ F)`.
 -/
 @[simps]
-def whiskering (E : K ⥤ J) : Cone F ⥤ Cone (E ⋙ F)
-    where
+def whiskering (E : K ⥤ J) : Cone F ⥤ Cone (E ⋙ F) where
   obj c := c.whisker E
   map f := { Hom := f.Hom }
 #align category_theory.limits.cones.whiskering CategoryTheory.Limits.Cones.whiskering
 
 /-- Whiskering by an equivalence gives an equivalence between categories of cones.
 -/
 @[simps]
-def whiskeringEquivalence (e : K ≌ J) : Cone F ≌ Cone (e.functor ⋙ F)
-    where
+def whiskeringEquivalence (e : K ≌ J) : Cone F ≌ Cone (e.functor ⋙ F) where
   functor := whiskering e.functor
   inverse := whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom
   unitIso := NatIso.ofComponents (fun s => Cones.ext (Iso.refl _) (by aesop_cat)) (by aesop_cat)
@@ -572,17 +567,15 @@ def precomposeEquivalence {G : J ⥤ C} (α : G ≅ F) : Cocone F ≌ Cocone G w
 /-- Whiskering on the left by `E : K ⥤ J` gives a functor from `Cocone F` to `Cocone (E ⋙ F)`.
 -/
 @[simps]
-def whiskering (E : K ⥤ J) : Cocone F ⥤ Cocone (E ⋙ F)
-    where
+def whiskering (E : K ⥤ J) : Cocone F ⥤ Cocone (E ⋙ F) where
   obj c := c.whisker E
   map f := { Hom := f.Hom }
 #align category_theory.limits.cocones.whiskering CategoryTheory.Limits.Cocones.whiskering
 
 /-- Whiskering by an equivalence gives an equivalence between categories of cones.
 -/
 @[simps]
-def whiskeringEquivalence (e : K ≌ J) : Cocone F ≌ Cocone (e.functor ⋙ F)
-    where
+def whiskeringEquivalence (e : K ≌ J) : Cocone F ≌ Cocone (e.functor ⋙ F) where
   functor := whiskering e.functor
   inverse :=
     whiskering e.inverse ⋙
@@ -902,8 +895,7 @@ variable (F)
 is equivalent to the opposite category of
 the category of cones on the opposite of `F`.
 -/
-def coconeEquivalenceOpConeOp : Cocone F ≌ (Cone F.op)ᵒᵖ
-    where
+def coconeEquivalenceOpConeOp : Cocone F ≌ (Cone F.op)ᵒᵖ where
   functor :=
     { obj := fun c => op (Cocone.op c)
       map := fun {X} {Y} f =>
@@ -971,16 +963,14 @@ and replace with `@[simps]`-/
 -- as we can write a simpler `rfl` lemma for the components of the natural transformation by hand.
 /-- Change a cocone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/
 @[simps!]
-def coneOfCoconeLeftOp (c : Cocone F.leftOp) : Cone F
-    where
+def coneOfCoconeLeftOp (c : Cocone F.leftOp) : Cone F where
   pt := op c.pt
   π := NatTrans.removeLeftOp c.ι
 #align category_theory.limits.cone_of_cocone_left_op CategoryTheory.Limits.coneOfCoconeLeftOp
 
 /-- Change a cone on `F : J ⥤ Cᵒᵖ` to a cocone on `F.leftOp : Jᵒᵖ ⥤ C`. -/
 @[simps!]
-def coconeLeftOpOfCone (c : Cone F) : Cocone F.leftOp
-    where
+def coconeLeftOpOfCone (c : Cone F) : Cocone F.leftOp where
   pt := unop c.pt
   ι := NatTrans.leftOp c.π
 #align category_theory.limits.cocone_left_op_of_cone CategoryTheory.Limits.coconeLeftOpOfCone
@@ -990,8 +980,7 @@ def coconeLeftOpOfCone (c : Cone F) : Cocone F.leftOp
   being simplified properly. -/
 /-- Change a cone on `F.leftOp : Jᵒᵖ ⥤ C` to a cocone on `F : J ⥤ Cᵒᵖ`. -/
 @[simps pt]
-def coconeOfConeLeftOp (c : Cone F.leftOp) : Cocone F
-    where
+def coconeOfConeLeftOp (c : Cone F.leftOp) : Cocone F where
   pt := op c.pt
   ι := NatTrans.removeLeftOp c.π
 #align category_theory.limits.cocone_of_cone_left_op CategoryTheory.Limits.coconeOfConeLeftOp
@@ -1005,8 +994,7 @@ theorem coconeOfConeLeftOp_ι_app (c : Cone F.leftOp) (j) :
 
 /-- Change a cocone on `F : J ⥤ Cᵒᵖ` to a cone on `F.leftOp : Jᵒᵖ ⥤ C`. -/
 @[simps!]
-def coneLeftOpOfCocone (c : Cocone F) : Cone F.leftOp
-    where
+def coneLeftOpOfCocone (c : Cocone F) : Cone F.leftOp where
   pt := unop c.pt
   π := NatTrans.leftOp c.ι
 #align category_theory.limits.cone_left_op_of_cocone CategoryTheory.Limits.coneLeftOpOfCocone
@@ -1019,32 +1007,28 @@ variable {F : Jᵒᵖ ⥤ C}
 
 /-- Change a cocone on `F.rightOp : J ⥤ Cᵒᵖ` to a cone on `F : Jᵒᵖ ⥤ C`. -/
 @[simps]
-def coneOfCoconeRightOp (c : Cocone F.rightOp) : Cone F
-    where
+def coneOfCoconeRightOp (c : Cocone F.rightOp) : Cone F where
   pt := unop c.pt
   π := NatTrans.removeRightOp c.ι
 #align category_theory.limits.cone_of_cocone_right_op CategoryTheory.Limits.coneOfCoconeRightOp
 
 /-- Change a cone on `F : Jᵒᵖ ⥤ C` to a cocone on `F.rightOp : Jᵒᵖ ⥤ C`. -/
 @[simps]
-def coconeRightOpOfCone (c : Cone F) : Cocone F.rightOp
-    where
+def coconeRightOpOfCone (c : Cone F) : Cocone F.rightOp where
   pt := op c.pt
   ι := NatTrans.rightOp c.π
 #align category_theory.limits.cocone_right_op_of_cone CategoryTheory.Limits.coconeRightOpOfCone
 
 /-- Change a cone on `F.rightOp : J ⥤ Cᵒᵖ` to a cocone on `F : Jᵒᵖ ⥤ C`. -/
 @[simps]
-def coconeOfConeRightOp (c : Cone F.rightOp) : Cocone F
-    where
+def coconeOfConeRightOp (c : Cone F.rightOp) : Cocone F where
   pt := unop c.pt
   ι := NatTrans.removeRightOp c.π
 #align category_theory.limits.cocone_of_cone_right_op CategoryTheory.Limits.coconeOfConeRightOp
 
 /-- Change a cocone on `F : Jᵒᵖ ⥤ C` to a cone on `F.rightOp : J ⥤ Cᵒᵖ`. -/
 @[simps]
-def coneRightOpOfCocone (c : Cocone F) : Cone F.rightOp
-    where
+def coneRightOpOfCocone (c : Cocone F) : Cone F.rightOp where
   pt := op c.pt
   π := NatTrans.rightOp c.ι
 #align category_theory.limits.cone_right_op_of_cocone CategoryTheory.Limits.coneRightOpOfCocone
@@ -1057,32 +1041,28 @@ variable {F : Jᵒᵖ ⥤ Cᵒᵖ}
 
 /-- Change a cocone on `F.unop : J ⥤ C` into a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/
 @[simps]
-def coneOfCoconeUnop (c : Cocone F.unop) : Cone F
-    where
+def coneOfCoconeUnop (c : Cocone F.unop) : Cone F where
   pt := op c.pt
   π := NatTrans.removeUnop c.ι
 #align category_theory.limits.cone_of_cocone_unop CategoryTheory.Limits.coneOfCoconeUnop
 
 /-- Change a cone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cocone on `F.unop : J ⥤ C`. -/
 @[simps]
-def coconeUnopOfCone (c : Cone F) : Cocone F.unop
-    where
+def coconeUnopOfCone (c : Cone F) : Cocone F.unop where
   pt := unop c.pt
   ι := NatTrans.unop c.π
 #align category_theory.limits.cocone_unop_of_cone CategoryTheory.Limits.coconeUnopOfCone
 
 /-- Change a cone on `F.unop : J ⥤ C` into a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ`. -/
 @[simps]
-def coconeOfConeUnop (c : Cone F.unop) : Cocone F
-    where
+def coconeOfConeUnop (c : Cone F.unop) : Cocone F where
   pt := op c.pt
   ι := NatTrans.removeUnop c.π
 #align category_theory.limits.cocone_of_cone_unop CategoryTheory.Limits.coconeOfConeUnop
 
 /-- Change a cocone on `F : Jᵒᵖ ⥤ Cᵒᵖ` into a cone on `F.unop : J ⥤ C`. -/
 @[simps]
-def coneUnopOfCocone (c : Cocone F) : Cone F.unop
-    where
+def coneUnopOfCocone (c : Cocone F) : Cone F.unop where
   pt := unop c.pt
   π := NatTrans.unop c.ι
 #align category_theory.limits.cone_unop_of_cocone CategoryTheory.Limits.coneUnopOfCocone

Mathlib/CategoryTheory/Limits/HasLimits.lean

@@ -1314,4 +1314,3 @@ def isColimitEquivIsLimitOp {t : Cocone F} : IsColimit t ≃ IsLimit t.op :=
 #align category_theory.limits.is_colimit_equiv_is_limit_op CategoryTheory.Limits.isColimitEquivIsLimitOp
 
 end Opposite
-#lint

Mathlib/CategoryTheory/Limits/IsLimit.lean

@@ -1074,4 +1074,3 @@ end
 end IsColimit
 
 end CategoryTheory.Limits
-#lint

Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean

@@ -69,13 +69,12 @@ theorem map_eq_zero_iff (F : C ⥤ D) [PreservesZeroMorphisms F] [Faithful F] {X
 #align category_theory.functor.map_eq_zero_iff CategoryTheory.Functor.map_eq_zero_iff
 
 instance (priority := 100) preservesZeroMorphisms_of_isLeftAdjoint (F : C ⥤ D) [IsLeftAdjoint F] :
-    PreservesZeroMorphisms F where 
+    PreservesZeroMorphisms F where
   map_zero X Y := by
     let adj := Adjunction.ofLeftAdjoint F
     dsimp
     calc
       F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
-        -- simp only [id_obj, comp_obj, Adjunction.left_triangle_components, Category.comp_id]
       _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
       _ = 0 := ?_
     · rw [Adjunction.left_triangle_components]
@@ -85,7 +84,7 @@ instance (priority := 100) preservesZeroMorphisms_of_isLeftAdjoint (F : C ⥤ D)
 #align category_theory.functor.preserves_zero_morphisms_of_is_left_adjoint CategoryTheory.Functor.preservesZeroMorphisms_of_isLeftAdjoint
 
 instance (priority := 100) preservesZeroMorphisms_of_isRightAdjoint (G : C ⥤ D) [IsRightAdjoint G] :
-    PreservesZeroMorphisms G where 
+    PreservesZeroMorphisms G where
   map_zero X Y := by
     let adj := Adjunction.ofRightAdjoint G
     calc
@@ -98,8 +97,8 @@ instance (priority := 100) preservesZeroMorphisms_of_isRightAdjoint (G : C ⥤ D
 #align category_theory.functor.preserves_zero_morphisms_of_is_right_adjoint CategoryTheory.Functor.preservesZeroMorphisms_of_isRightAdjoint
 
 instance (priority := 100) preservesZeroMorphisms_of_full (F : C ⥤ D) [Full F] :
-    PreservesZeroMorphisms F where 
-map_zero X Y :=
+    PreservesZeroMorphisms F where
+  map_zero X Y :=
     calc
       F.map (0 : X ⟶ Y) = F.map (0 ≫ F.preimage (0 : F.obj Y ⟶ F.obj Y)) := by rw [zero_comp]
       _ = 0 := by rw [F.map_comp, F.image_preimage, comp_zero]
@@ -117,8 +116,7 @@ variable [HasZeroMorphisms C] [HasZeroMorphisms D] (F : C ⥤ D)
 
 /-- A functor that preserves zero morphisms also preserves the zero object. -/
 @[simps]
-def mapZeroObject [PreservesZeroMorphisms F] : F.obj 0 ≅ 0
-    where
+def mapZeroObject [PreservesZeroMorphisms F] : F.obj 0 ≅ 0 where
   hom := 0
   inv := 0
   hom_inv_id := by rw [← F.map_id, id_zero, F.map_zero, zero_comp]
@@ -127,14 +125,12 @@ def mapZeroObject [PreservesZeroMorphisms F] : F.obj 0 ≅ 0
 
 variable {F}
 
-theorem preservesZeroMorphisms_of_map_zero_object (i : F.obj 0 ≅ 0) : PreservesZeroMorphisms F :=
-  {
-    map_zero := fun X Y =>
-      calc
-        F.map (0 : X ⟶ Y) = F.map (0 : X ⟶ 0) ≫ F.map 0 := by rw [← Functor.map_comp, comp_zero]
-        _ = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0 := by rw [Iso.hom_inv_id, Category.id_comp]
-        _ = 0 := by simp only [zero_of_to_zero i.hom, zero_comp, comp_zero]
-         }
+theorem preservesZeroMorphisms_of_map_zero_object (i : F.obj 0 ≅ 0) : PreservesZeroMorphisms F where
+  map_zero X Y :=
+    calc
+      F.map (0 : X ⟶ Y) = F.map (0 : X ⟶ 0) ≫ F.map 0 := by rw [← Functor.map_comp, comp_zero]
+      _ = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0 := by rw [Iso.hom_inv_id, Category.id_comp]
+      _ = 0 := by simp only [zero_of_to_zero i.hom, zero_comp, comp_zero]
 #align category_theory.functor.preserves_zero_morphisms_of_map_zero_object CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object
 
 instance (priority := 100) preservesZeroMorphisms_of_preserves_initial_object
@@ -171,4 +167,3 @@ def preservesInitialObjectOfPreservesZeroMorphisms [PreservesZeroMorphisms F] :
 end ZeroObject
 
 end CategoryTheory.Functor
-

Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean

@@ -125,14 +125,14 @@ attribute [instance] CoproductsDisjoint.CoproductDisjoint
 /-- If `C` has disjoint coproducts, any morphism out of initial is mono. Note it isn't true in
 general that `C` has strict initial objects, for instance consider the category of types and
 partial functions. -/
-theorem initialMonoClass_of_disjoint_coproducts [CoproductsDisjoint C] : InitialMonoClass C :=
-  { isInitial_mono_from := @fun _I X hI =>
-      CoproductDisjoint.mono_inl X (IsInitial.to hI X) (CategoryTheory.CategoryStruct.id X)
-        { desc := fun s : BinaryCofan _ _ => s.inr
-          fac := fun _s j =>
-            Discrete.casesOn j fun j => WalkingPair.casesOn j (hI.hom_ext _ _) (id_comp _)
-          uniq := fun (_s : BinaryCofan _ _) _m w =>
-            (id_comp _).symm.trans (w ⟨WalkingPair.right⟩) } }
+theorem initialMonoClass_of_disjoint_coproducts [CoproductsDisjoint C] : InitialMonoClass C where
+  isInitial_mono_from X hI :=
+    CoproductDisjoint.mono_inl X (IsInitial.to hI X) (CategoryTheory.CategoryStruct.id X)
+      { desc := fun s : BinaryCofan _ _ => s.inr
+        fac := fun _s j =>
+          Discrete.casesOn j fun j => WalkingPair.casesOn j (hI.hom_ext _ _) (id_comp _)
+        uniq := fun (_s : BinaryCofan _ _) _m w =>
+          (id_comp _).symm.trans (w ⟨WalkingPair.right⟩) }
 #align category_theory.limits.initial_mono_class_of_disjoint_coproducts CategoryTheory.Limits.initialMonoClass_of_disjoint_coproducts
 
 end Limits

Mathlib/CategoryTheory/Limits/Shapes/FiniteProducts.lean

@@ -32,7 +32,7 @@ variable (C : Type u) [Category.{v} C]
 with shape `Discrete J`, where we have `[Finite J]`.
 
 We require this condition only for `J = Fin n` in the definition, then deduce a version for any
-`J : Type*` as a corollary of this definition.
+`J : Type _` as a corollary of this definition.
 -/
 class HasFiniteProducts : Prop where
   /-- `C` has finite products -/
@@ -66,7 +66,7 @@ theorem hasFiniteProducts_of_hasProducts [HasProducts.{w} C] : HasFiniteProducts
 with shape `Discrete J`, where we have `[Fintype J]`.
 
 We require this condition only for `J = Fin n` in the definition, then deduce a version for any
-`J : Type*` as a corollary of this definition.
+`J : Type _` as a corollary of this definition.
 -/
 class HasFiniteCoproducts : Prop where
   /-- `C` has all finite coproducts -/
@@ -95,4 +95,3 @@ theorem hasFiniteCoproducts_of_hasCoproducts [HasCoproducts.{w} C] : HasFiniteCo
 #align category_theory.limits.has_finite_coproducts_of_has_coproducts CategoryTheory.Limits.hasFiniteCoproducts_of_hasCoproducts
 
 end CategoryTheory.Limits
-

Mathlib/CategoryTheory/Limits/Shapes/ZeroObjects.lean

@@ -193,13 +193,13 @@ section
 
 variable [HasZeroObject C]
 
-/-- Construct a `HasZero C` for a category with a zero object.
-This can not be a global instance as it will trigger for every `HasZero C` typeclass search.
+/-- Construct a `Zero C` for a category with a zero object.
+This can not be a global instance as it will trigger for every `Zero C` typeclass search.
 -/
-protected def HasZeroObject.hasZero : Zero C where zero := HasZeroObject.zero.choose
-#align category_theory.limits.has_zero_object.has_zero CategoryTheory.Limits.HasZeroObject.hasZero
+protected def HasZeroObject.zero' : Zero C where zero := HasZeroObject.zero.choose
+#align category_theory.limits.has_zero_object.has_zero CategoryTheory.Limits.HasZeroObject.zero'
 
-scoped[ZeroObject] attribute [instance] CategoryTheory.Limits.HasZeroObject.hasZero
+scoped[ZeroObject] attribute [instance] CategoryTheory.Limits.HasZeroObject.zero'
 
 open ZeroObject
 
@@ -315,9 +315,9 @@ def zeroIsoTerminal [HasTerminal C] : 0 ≅ ⊤_ C :=
   zeroIsTerminal.uniqueUpToIso terminalIsTerminal
 #align category_theory.limits.has_zero_object.zero_iso_terminal CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal
 
-instance (priority := 100) has_strict_initial : InitialMonoClass C :=
+instance (priority := 100) initialMonoClass : InitialMonoClass C :=
   InitialMonoClass.of_isInitial zeroIsInitial fun X => by infer_instance
-#align category_theory.limits.has_zero_object.has_strict_initial CategoryTheory.Limits.HasZeroObject.has_strict_initial
+#align category_theory.limits.has_zero_object.has_strict_initial CategoryTheory.Limits.HasZeroObject.initialMonoClass
 
 end HasZeroObject