chore: tidy various files (#6382)

Mathlib/Algebra/Category/GroupCat/FilteredColimits.lean

@@ -14,14 +14,16 @@ import Mathlib.Algebra.Category.MonCat.FilteredColimits
 Forgetful functors from algebraic categories usually don't preserve colimits. However, they tend
 to preserve _filtered_ colimits.
 
-In this file, we start with a small filtered category `J` and a functor `F : J ⥤ Group`.
-We show that the colimit of `F ⋙ forget₂ Group Mon` (in `Mon`) carries the structure of a group,
-thereby showing that the forgetful functor `forget₂ Group Mon` preserves filtered colimits. In
-particular, this implies that `forget Group` preserves filtered colimits. Similarly for `AddGroup`,
-`CommGroup` and `AddCommGroup`.
+In this file, we start with a small filtered category `J` and a functor `F : J ⥤ GroupCat`.
+We show that the colimit of `F ⋙ forget₂ GroupCat MonCat` (in `MonCat`) carries the structure of a
+group,
+thereby showing that the forgetful functor `forget₂ GroupCat MonCat` preserves filtered colimits.
+In particular, this implies that `forget GroupCat` preserves filtered colimits.
+Similarly for `AddGroupCat`, `CommGroupCat` and `AddCommGroupCat`.
 
 -/
 
+set_option linter.uppercaseLean3 false
 
 universe v u
 
@@ -41,49 +43,41 @@ section
 
 open MonCat.FilteredColimits (colimit_one_eq colimit_mul_mk_eq)
 
--- We use parameters here, mainly so we can have the abbreviations `G` and `G.mk` below, without
--- passing around `F` all the time.
+-- Mathlib3 used parameters here, mainly so we could have the abbreviations `G` and `G.mk` below,
+-- without passing around `F` all the time.
 variable {J : Type v} [SmallCategory J] [IsFiltered J] (F : J ⥤ GroupCat.{max v u})
 
-/-- The colimit of `F ⋙ forget₂ Group Mon` in the category `Mon`.
+/-- The colimit of `F ⋙ forget₂ GroupCat MonCat` in the category `MonCat`.
 In the following, we will show that this has the structure of a group.
 -/
 @[to_additive
-  "The colimit of `F ⋙ forget₂ AddGroup AddMon` in the category `AddMon`.
+  "The colimit of `F ⋙ forget₂ AddGroupCat AddMonCat` in the category `AddMonCat`.
   In the following, we will show that this has the structure of an additive group."]
 noncomputable abbrev G : MonCat :=
   MonCat.FilteredColimits.colimit.{v, u} (F ⋙ forget₂ GroupCat MonCat.{max v u})
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.G GroupCat.FilteredColimits.G
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.G AddGroupCat.FilteredColimits.G
 
 /-- The canonical projection into the colimit, as a quotient type. -/
 @[to_additive "The canonical projection into the colimit, as a quotient type."]
 abbrev G.mk : (Σ j, F.obj j) → G.{v, u} F :=
   Quot.mk (Types.Quot.Rel.{v, u} (F ⋙ forget GroupCat.{max v u}))
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.G.mk GroupCat.FilteredColimits.G.mk
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.G.mk AddGroupCat.FilteredColimits.G.mk
 
 @[to_additive]
 theorem G.mk_eq (x y : Σ j, F.obj j)
     (h : ∃ (k : J) (f : x.1 ⟶ k) (g : y.1 ⟶ k), F.map f x.2 = F.map g y.2) :
     G.mk.{v, u} F x = G.mk F y :=
   Quot.EqvGen_sound (Types.FilteredColimit.eqvGen_quot_rel_of_rel (F ⋙ forget GroupCat) x y h)
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.G.mk_eq GroupCat.FilteredColimits.G.mk_eq
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.G.mk_eq AddGroupCat.FilteredColimits.G.mk_eq
 
 /-- The "unlifted" version of taking inverses in the colimit. -/
 @[to_additive "The \"unlifted\" version of negation in the colimit."]
 def colimitInvAux (x : Σ j, F.obj j) : G.{v, u} F :=
   G.mk F ⟨x.1, x.2⁻¹⟩
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.colimit_inv_aux GroupCat.FilteredColimits.colimitInvAux
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.colimit_neg_aux AddGroupCat.FilteredColimits.colimitNegAux
 
 @[to_additive]
@@ -95,31 +89,25 @@ theorem colimitInvAux_eq_of_rel (x y : Σ j, F.obj j)
   use k, f, g
   rw [MonoidHom.map_inv, MonoidHom.map_inv, inv_inj]
   exact hfg
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.colimit_inv_aux_eq_of_rel GroupCat.FilteredColimits.colimitInvAux_eq_of_rel
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.colimit_neg_aux_eq_of_rel AddGroupCat.FilteredColimits.colimitNegAux_eq_of_rel
 
-/-- Taking inverses in the colimit. See also `colimit_inv_aux`. -/
-@[to_additive "Negation in the colimit. See also `colimit_neg_aux`."]
+/-- Taking inverses in the colimit. See also `colimitInvAux`. -/
+@[to_additive "Negation in the colimit. See also `colimitNegAux`."]
 instance colimitInv : Inv (G.{v, u} F) where
   inv x := by
     refine' Quot.lift (colimitInvAux.{v, u} F) _ x
     intro x y h
     apply colimitInvAux_eq_of_rel
     apply Types.FilteredColimit.rel_of_quot_rel
     exact h
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.colimit_has_inv GroupCat.FilteredColimits.colimitInv
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.colimit_has_neg AddGroupCat.FilteredColimits.colimitNeg
 
 @[to_additive (attr := simp)]
 theorem colimit_inv_mk_eq (x : Σ j, F.obj j) : (G.mk.{v, u} F x)⁻¹ = G.mk F ⟨x.1, x.2⁻¹⟩ :=
   rfl
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.colimit_inv_mk_eq GroupCat.FilteredColimits.colimit_inv_mk_eq
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.colimit_neg_mk_eq AddGroupCat.FilteredColimits.colimit_neg_mk_eq
 
 @[to_additive]
@@ -133,31 +121,25 @@ noncomputable instance colimitGroup : Group (G.{v, u} F) :=
         colimit_one_eq (F ⋙ forget₂ GroupCat MonCat.{max v u}) j]
       dsimp
       erw [CategoryTheory.Functor.map_id, mul_left_inv] }
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.colimit_group GroupCat.FilteredColimits.colimitGroup
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.colimit_add_group AddGroupCat.FilteredColimits.colimitAddGroup
 
 /-- The bundled group giving the filtered colimit of a diagram. -/
 @[to_additive "The bundled additive group giving the filtered colimit of a diagram."]
 noncomputable def colimit : GroupCat.{max v u} :=
   GroupCat.of (G.{v, u} F)
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.colimit GroupCat.FilteredColimits.colimit
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.colimit AddGroupCat.FilteredColimits.colimit
 
 /-- The cocone over the proposed colimit group. -/
 @[to_additive "The cocone over the proposed colimit additive group."]
 noncomputable def colimitCocone : Cocone F where
   pt := colimit.{v, u} F
   ι := { (MonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ GroupCat MonCat.{max v u})).ι with }
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.colimit_cocone GroupCat.FilteredColimits.colimitCocone
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.colimit_cocone AddGroupCat.FilteredColimits.colimitCocone
 
-/-- The proposed colimit cocone is a colimit in `Group`. -/
+/-- The proposed colimit cocone is a colimit in `GroupCat`. -/
 @[to_additive "The proposed colimit cocone is a colimit in `AddGroup`."]
 def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
   desc t :=
@@ -172,9 +154,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
       (Types.colimitCoconeIsColimit.{v, u} (F ⋙ forget GroupCat)).uniq
       ((forget GroupCat).mapCocone t) _
         fun j => funext fun x => FunLike.congr_fun (h j) x
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.colimit_cocone_is_colimit GroupCat.FilteredColimits.colimitCoconeIsColimit
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.colimit_cocone_is_colimit AddGroupCat.FilteredColimits.colimitCoconeIsColimit
 
 @[to_additive forget₂AddMonPreservesFilteredColimits]
@@ -184,18 +164,14 @@ noncomputable instance forget₂MonPreservesFilteredColimits :
       letI : Category.{u, u} x := hx1
       ⟨fun {F} => preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
           (MonCat.FilteredColimits.colimitCoconeIsColimit.{u, u} _)⟩
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.forget₂_Mon_preserves_filtered_colimits GroupCat.FilteredColimits.forget₂MonPreservesFilteredColimits
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.forget₂_AddMon_preserves_filtered_colimits AddGroupCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits
 
 @[to_additive]
 noncomputable instance forgetPreservesFilteredColimits :
     PreservesFilteredColimits (forget GroupCat.{u}) :=
   Limits.compPreservesFilteredColimits (forget₂ GroupCat MonCat) (forget MonCat.{u})
-set_option linter.uppercaseLean3 false in
 #align Group.filtered_colimits.forget_preserves_filtered_colimits GroupCat.FilteredColimits.forgetPreservesFilteredColimits
-set_option linter.uppercaseLean3 false in
 #align AddGroup.filtered_colimits.forget_preserves_filtered_colimits AddGroupCat.FilteredColimits.forgetPreservesFilteredColimits
 
 end
@@ -210,36 +186,30 @@ section
 -- passing around `F` all the time.
 variable {J : Type v} [SmallCategory J] [IsFiltered J] (F : J ⥤ CommGroupCat.{max v u})
 
-/-- The colimit of `F ⋙ forget₂ CommGroup Group` in the category `Group`.
+/-- The colimit of `F ⋙ forget₂ CommGroupCat GroupCat` in the category `GroupCat`.
 In the following, we will show that this has the structure of a _commutative_ group.
 -/
 @[to_additive
-  "The colimit of `F ⋙ forget₂ AddCommGroup AddGroup` in the category `AddGroup`.
+  "The colimit of `F ⋙ forget₂ AddCommGroupCat AddGroupCat` in the category `AddGroupCat`.
   In the following, we will show that this has the structure of a _commutative_ additive group."]
 noncomputable abbrev G : GroupCat.{max v u} :=
   GroupCat.FilteredColimits.colimit.{v, u} (F ⋙ forget₂ CommGroupCat.{max v u} GroupCat.{max v u})
-set_option linter.uppercaseLean3 false in
 #align CommGroup.filtered_colimits.G CommGroupCat.FilteredColimits.G
-set_option linter.uppercaseLean3 false in
 #align AddCommGroup.filtered_colimits.G AddCommGroupCat.FilteredColimits.G
 
 @[to_additive]
 noncomputable instance colimitCommGroup : CommGroup.{max v u} (G.{v, u} F) :=
   { (G F).str,
     CommMonCat.FilteredColimits.colimitCommMonoid
       (F ⋙ forget₂ CommGroupCat CommMonCat.{max v u}) with }
-set_option linter.uppercaseLean3 false in
 #align CommGroup.filtered_colimits.colimit_comm_group CommGroupCat.FilteredColimits.colimitCommGroup
-set_option linter.uppercaseLean3 false in
 #align AddCommGroup.filtered_colimits.colimit_add_comm_group AddCommGroupCat.FilteredColimits.colimitAddCommGroup
 
 /-- The bundled commutative group giving the filtered colimit of a diagram. -/
 @[to_additive "The bundled additive commutative group giving the filtered colimit of a diagram."]
 noncomputable def colimit : CommGroupCat :=
   CommGroupCat.of (G.{v, u} F)
-set_option linter.uppercaseLean3 false in
 #align CommGroup.filtered_colimits.colimit CommGroupCat.FilteredColimits.colimit
-set_option linter.uppercaseLean3 false in
 #align AddCommGroup.filtered_colimits.colimit AddCommGroupCat.FilteredColimits.colimit
 
 /-- The cocone over the proposed colimit commutative group. -/
@@ -249,12 +219,10 @@ noncomputable def colimitCocone : Cocone F where
   ι :=
     { (GroupCat.FilteredColimits.colimitCocone
           (F ⋙ forget₂ CommGroupCat GroupCat.{max v u})).ι with }
-set_option linter.uppercaseLean3 false in
 #align CommGroup.filtered_colimits.colimit_cocone CommGroupCat.FilteredColimits.colimitCocone
-set_option linter.uppercaseLean3 false in
 #align AddCommGroup.filtered_colimits.colimit_cocone AddCommGroupCat.FilteredColimits.colimitCocone
 
-/-- The proposed colimit cocone is a colimit in `CommGroup`. -/
+/-- The proposed colimit cocone is a colimit in `CommGroupCat`. -/
 @[to_additive "The proposed colimit cocone is a colimit in `AddCommGroup`."]
 def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
   desc t :=
@@ -269,9 +237,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone.{v, u} F) where
     FunLike.coe_injective <|
       (Types.colimitCoconeIsColimit.{v, u} (F ⋙ forget CommGroupCat)).uniq
         ((forget CommGroupCat).mapCocone t) _ fun j => funext fun x => FunLike.congr_fun (h j) x
-set_option linter.uppercaseLean3 false in
 #align CommGroup.filtered_colimits.colimit_cocone_is_colimit CommGroupCat.FilteredColimits.colimitCoconeIsColimit
-set_option linter.uppercaseLean3 false in
 #align AddCommGroup.filtered_colimits.colimit_cocone_is_colimit AddCommGroupCat.FilteredColimits.colimitCoconeIsColimit
 
 @[to_additive]
@@ -283,18 +249,14 @@ noncomputable instance forget₂GroupPreservesFilteredColimits :
         preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit.{u, u} F)
           (GroupCat.FilteredColimits.colimitCoconeIsColimit.{u, u}
             (F ⋙ forget₂ CommGroupCat GroupCat.{u})) }
-set_option linter.uppercaseLean3 false in
 #align CommGroup.filtered_colimits.forget₂_Group_preserves_filtered_colimits CommGroupCat.FilteredColimits.forget₂GroupPreservesFilteredColimits
-set_option linter.uppercaseLean3 false in
 #align AddCommGroup.filtered_colimits.forget₂_AddGroup_preserves_filtered_colimits AddCommGroupCat.FilteredColimits.forget₂AddGroupPreservesFilteredColimits
 
 @[to_additive]
 noncomputable instance forgetPreservesFilteredColimits :
     PreservesFilteredColimits (forget CommGroupCat.{u}) :=
   Limits.compPreservesFilteredColimits (forget₂ CommGroupCat GroupCat) (forget GroupCat.{u})
-set_option linter.uppercaseLean3 false in
 #align CommGroup.filtered_colimits.forget_preserves_filtered_colimits CommGroupCat.FilteredColimits.forgetPreservesFilteredColimits
-set_option linter.uppercaseLean3 false in
 #align AddCommGroup.filtered_colimits.forget_preserves_filtered_colimits AddCommGroupCat.FilteredColimits.forgetPreservesFilteredColimits
 
 end

Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

@@ -113,7 +113,7 @@ variable [HasColimitsOfShape J TopCat.{v}]
 
 /-- Given a diagram of presheafed spaces,
 we can push all the presheaves forward to the colimit `X` of the underlying topological spaces,
-obtaining a diagram in `(presheaf C X)ᵒᵖ`.
+obtaining a diagram in `(Presheaf C X)ᵒᵖ`.
 -/
 @[simps]
 def pushforwardDiagramToColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
@@ -177,7 +177,7 @@ set_option linter.uppercaseLean3 false in
 
 variable [∀ X : TopCat.{v}, HasLimitsOfShape Jᵒᵖ (X.Presheaf C)]
 
-/-- Auxiliary definition for `PresheafedSpace.has_colimits`.
+/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.instHasColimits`.
 -/
 def colimit (F : J ⥤ PresheafedSpace.{_, _, v} C) : PresheafedSpace C where
   carrier := Limits.colimit (F ⋙ PresheafedSpace.forget C)
@@ -199,7 +199,7 @@ theorem colimit_presheaf (F : J ⥤ PresheafedSpace.{_, _, v} C) :
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.colimit_presheaf AlgebraicGeometry.PresheafedSpace.colimit_presheaf
 
-/-- Auxiliary definition for `PresheafedSpace.has_colimits`.
+/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.instHasColimits`.
 -/
 @[simps]
 def colimitCocone (F : J ⥤ PresheafedSpace.{_, _, v} C) : Cocone F where
@@ -230,7 +230,7 @@ variable [HasLimitsOfShape Jᵒᵖ C]
 
 namespace ColimitCoconeIsColimit
 
-/-- Auxiliary definition for `PresheafedSpace.colimit_cocone_is_colimit`.
+/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit`.
 -/
 def descCApp (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (U : (Opens s.pt.carrier)ᵒᵖ) :
     s.pt.presheaf.obj U ⟶
@@ -287,7 +287,7 @@ theorem desc_c_naturality (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F)
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit.desc_c_naturality AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality
 
-/-- Auxiliary definition for `PresheafedSpace.colimit_cocone_is_colimit`.
+/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit`.
 -/
 def desc (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) : colimit F ⟶ s.pt where
   base := colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).mapCocone s)
@@ -315,7 +315,7 @@ end ColimitCoconeIsColimit
 
 open ColimitCoconeIsColimit
 
-/-- Auxiliary definition for `PresheafedSpace.has_colimits`.
+/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.instHasColimits`.
 -/
 def colimitCoconeIsColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
     IsColimit (colimitCocone F) where
@@ -347,8 +347,8 @@ def colimitCoconeIsColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.colimit_cocone_is_colimit AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit
 
-instance : HasColimitsOfShape J (PresheafedSpace.{_, _, v} C)
-  where has_colimit F := ⟨colimitCocone F, colimitCoconeIsColimit F⟩
+instance : HasColimitsOfShape J (PresheafedSpace.{_, _, v} C) where
+  has_colimit F := ⟨colimitCocone F, colimitCoconeIsColimit F⟩
 
 instance : PreservesColimitsOfShape J (PresheafedSpace.forget.{u, v, v} C) :=
   ⟨fun {F} => preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit F) <| by
@@ -360,14 +360,14 @@ instance : PreservesColimitsOfShape J (PresheafedSpace.forget.{u, v, v} C) :=
 
 /-- When `C` has limits, the category of presheaved spaces with values in `C` itself has colimits.
 -/
-instance [HasLimits C] : HasColimits (PresheafedSpace.{_, _, v} C) :=
+instance instHasColimits [HasLimits C] : HasColimits (PresheafedSpace.{_, _, v} C) :=
   ⟨fun {_ _} => ⟨fun {F} => ⟨colimitCocone F, colimitCoconeIsColimit F⟩⟩⟩
 
 /-- The underlying topological space of a colimit of presheaved spaces is
 the colimit of the underlying topological spaces.
 -/
-instance forgetPreservesColimits [HasLimits C] : PreservesColimits (PresheafedSpace.forget C)
-    where preservesColimitsOfShape {J 𝒥} :=
+instance forgetPreservesColimits [HasLimits C] : PreservesColimits (PresheafedSpace.forget C) where
+  preservesColimitsOfShape {J 𝒥} :=
     { preservesColimit := fun {F} =>
         preservesColimitOfPreservesColimitCocone (colimitCoconeIsColimit F)
           (by apply IsColimit.ofIsoColimit (colimit.isColimit _)

Mathlib/Analysis/Calculus/DiffContOnCl.lean

@@ -79,9 +79,9 @@ protected theorem differentiableAt (h : DiffContOnCl 𝕜 f s) (hs : IsOpen s) (
   h.differentiableOn.differentiableAt <| hs.mem_nhds hx
 #align diff_cont_on_cl.differentiable_at DiffContOnCl.differentiableAt
 
-theorem differentiable_at' (h : DiffContOnCl 𝕜 f s) (hx : s ∈ 𝓝 x) : DifferentiableAt 𝕜 f x :=
+theorem differentiableAt' (h : DiffContOnCl 𝕜 f s) (hx : s ∈ 𝓝 x) : DifferentiableAt 𝕜 f x :=
   h.differentiableOn.differentiableAt hx
-#align diff_cont_on_cl.differentiable_at' DiffContOnCl.differentiable_at'
+#align diff_cont_on_cl.differentiable_at' DiffContOnCl.differentiableAt'
 
 protected theorem mono (h : DiffContOnCl 𝕜 f s) (ht : t ⊆ s) : DiffContOnCl 𝕜 f t :=
   ⟨h.differentiableOn.mono ht, h.continuousOn.mono (closure_mono ht)⟩