chore: tidy various files (#4423)

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -16,12 +16,12 @@ import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
 /-!
 # The category of additive commutative groups has all colimits.
 
-This file uses a "pre-automated" approach, just as for `Mon/colimits.lean`.
+This file uses a "pre-automated" approach, just as for `Mon/Colimits.lean`.
 It is a very uniform approach, that conceivably could be synthesised directly
-by a tactic that analyses the shape of `add_comm_group` and `monoid_hom`.
+by a tactic that analyses the shape of `AddCommGroup` and `MonoidHom`.
 
 TODO:
-In fact, in `AddCommGroup` there is a much nicer model of colimits as quotients
+In fact, in `AddCommGroupCat` there is a much nicer model of colimits as quotients
 of finitely supported functions, and we really should implement this as well (or instead).
 -/
 
@@ -40,7 +40,7 @@ open CategoryTheory.Limits
 namespace AddCommGroupCat.Colimits
 
 /-!
-We build the colimit of a diagram in `AddCommGroup` by constructing the
+We build the colimit of a diagram in `AddCommGroupCat` by constructing the
 free group on the disjoint union of all the abelian groups in the diagram,
 then taking the quotient by the abelian group laws within each abelian group,
 and the identifications given by the morphisms in the diagram.
@@ -105,7 +105,7 @@ def colimitSetoid : Setoid (Prequotient F) where
 
 attribute [instance] colimitSetoid
 
-/-- The underlying type of the colimit of a diagram in `AddCommGroup`.
+/-- The underlying type of the colimit of a diagram in `AddCommGroupCat`.
 -/
 def ColimitType : Type v :=
   Quotient (colimitSetoid F)
@@ -306,7 +306,7 @@ namespace AddCommGroupCat
 
 open QuotientAddGroup
 
-/-- The categorical cokernel of a morphism in `AddCommGroup`
+/-- The categorical cokernel of a morphism in `AddCommGroupCat`
 agrees with the usual group-theoretical quotient.
 -/
 noncomputable def cokernelIsoQuotient {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :

Mathlib/Algebra/Category/GroupCat/Images.lean

@@ -37,7 +37,7 @@ attribute [local ext] Subtype.ext_val
 
 section
 
--- implementation details of `has_image` for `AddCommGroupCat`; use the API, not these
+-- implementation details of `IsImage` for `AddCommGroupCat`; use the API, not these
 /-- the image of a morphism in `AddCommGroupCat` is just the bundling of `AddMonoidHom.range f` -/
 def image : AddCommGroupCat :=
   AddCommGroupCat.of (AddMonoidHom.range f)

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -16,31 +16,29 @@ import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
 import Mathlib.RingTheory.Subring.Basic
 
 /-!
-# Constructions of (co)limits in CommRing
+# Constructions of (co)limits in `CommRingCat`
 
-In this file we provide the explicit (co)cones for various (co)limits in `CommRing`, including
+In this file we provide the explicit (co)cones for various (co)limits in `CommRingCat`, including
 * tensor product is the pushout
 * `Z` is the initial object
 * `0` is the strict terminal object
 * cartesian product is the product
-* `ring_hom.eq_locus` is the equalizer
+* `RingHom.eqLocus` is the equalizer
 
 -/
 
 
 universe u u'
 
-open CategoryTheory CategoryTheory.Limits
-
-open TensorProduct
+open CategoryTheory CategoryTheory.Limits TensorProduct
 
 namespace CommRingCat
 
 section Pushout
 
 variable {R A B : CommRingCat.{u}} (f : R ⟶ A) (g : R ⟶ B)
 
-/-- The explicit cocone with tensor products as the fibered product in `CommRing`. -/
+/-- The explicit cocone with tensor products as the fibered product in `CommRingCat`. -/
 def pushoutCocone : Limits.PushoutCocone f g := by
   letI := RingHom.toAlgebra f
   letI := RingHom.toAlgebra g
@@ -148,12 +146,12 @@ end Pushout
 
 section Terminal
 
-/-- The trivial ring is the (strict) terminal object of `CommRing`. -/
+/-- The trivial ring is the (strict) terminal object of `CommRingCat`. -/
 def punitIsTerminal : IsTerminal (CommRingCat.of.{u} PUnit) := by
   refine IsTerminal.ofUnique (h := fun X => ⟨⟨⟨⟨1, rfl⟩, fun _ _ => rfl⟩, ?_, ?_⟩, ?_⟩)
-  . dsimp
-  . intros; dsimp
-  . intros f; ext; rfl
+  · dsimp
+  · intros; dsimp
+  · intros f; ext; rfl
 set_option linter.uppercaseLean3 false in
 #align CommRing.punit_is_terminal CommRingCat.punitIsTerminal
 
@@ -177,7 +175,7 @@ theorem subsingleton_of_isTerminal {X : CommRingCat} (hX : IsTerminal X) : Subsi
 set_option linter.uppercaseLean3 false in
 #align CommRing.subsingleton_of_is_terminal CommRingCat.subsingleton_of_isTerminal
 
-/-- `ℤ` is the initial object of `CommRing`. -/
+/-- `ℤ` is the initial object of `CommRingCat`. -/
 def zIsInitial : IsInitial (CommRingCat.of ℤ) :=
   IsInitial.ofUnique (h := fun R => ⟨⟨Int.castRingHom R⟩, fun a => a.ext_int _⟩)
 set_option linter.uppercaseLean3 false in
@@ -189,14 +187,14 @@ section Product
 
 variable (A B : CommRingCat.{u})
 
-/-- The product in `CommRing` is the cartesian product. This is the binary fan. -/
+/-- The product in `CommRingCat` is the cartesian product. This is the binary fan. -/
 @[simps! pt]
 def prodFan : BinaryFan A B :=
   BinaryFan.mk (CommRingCat.ofHom <| RingHom.fst A B) (CommRingCat.ofHom <| RingHom.snd A B)
 set_option linter.uppercaseLean3 false in
 #align CommRing.prod_fan CommRingCat.prodFan
 
-/-- The product in `CommRing` is the cartesian product. -/
+/-- The product in `CommRingCat` is the cartesian product. -/
 def prodFanIsLimit : IsLimit (prodFan A B) where
   lift c := RingHom.prod (c.π.app ⟨WalkingPair.left⟩) (c.π.app ⟨WalkingPair.right⟩)
   fac c j := by
@@ -223,15 +221,15 @@ section Equalizer
 
 variable {A B : CommRingCat.{u}} (f g : A ⟶ B)
 
-/-- The equalizer in `CommRing` is the equalizer as sets. This is the equalizer fork. -/
+/-- The equalizer in `CommRingCat` is the equalizer as sets. This is the equalizer fork. -/
 def equalizerFork : Fork f g :=
   Fork.ofι (CommRingCat.ofHom (RingHom.eqLocus f g).subtype) <| by
       ext ⟨x, e⟩
       simpa using e
 set_option linter.uppercaseLean3 false in
 #align CommRing.equalizer_fork CommRingCat.equalizerFork
 
-/-- The equalizer in `CommRing` is the equalizer as sets. -/
+/-- The equalizer in `CommRingCat` is the equalizer as sets. -/
 def equalizerForkIsLimit : IsLimit (equalizerFork f g) := by
   fapply Fork.IsLimit.mk'
   intro s
@@ -291,8 +289,8 @@ end Equalizer
 
 section Pullback
 
-/-- In the category of `CommRing`, the pullback of `f : A ⟶ C` and `g : B ⟶ C` is the `eq_locus` of
-the two maps `A × B ⟶ C`. This is the constructed pullback cone.
+/-- In the category of `CommRingCat`, the pullback of `f : A ⟶ C` and `g : B ⟶ C` is the `eqLocus`
+of the two maps `A × B ⟶ C`. This is the constructed pullback cone.
 -/
 def pullbackCone {A B C : CommRingCat.{u}} (f : A ⟶ C) (g : B ⟶ C) : PullbackCone f g :=
   PullbackCone.mk

Mathlib/Algebra/Module/Torsion.lean

@@ -30,9 +30,9 @@ import Mathlib.RingTheory.Finiteness
 * `Submodule.torsion R M` : the torsion submoule, containing all elements `x` of `M` such that
   `a • x = 0` for some non-zero-divisor `a` in `R`.
 * `Module.IsTorsionBy R M a` : the property that defines a `a`-torsion module. Similarly,
-  `is_torsion_by_set`, `is_torsion'` and `is_torsion`.
+  `IsTorsionBySet`, `IsTorsion'` and `IsTorsion`.
 * `Module.IsTorsionBySet.module` : Creates a `R ⧸ I`-module from a `R`-module that
-  `is_torsion_by_set R _ I`.
+  `IsTorsionBySet R _ I`.
 
 ## Main statements
 
@@ -46,15 +46,15 @@ import Mathlib.RingTheory.Finiteness
   `p i`-torsion submodules when the `p i` are pairwise coprime. A more general version with coprime
   ideals is `Submodule.torsionBySet_is_internal`.
 * `Submodule.noZeroSMulDivisors_iff_torsion_bot` : a module over a domain has
-  `no_zero_smul_divisors` (that is, there is no non-zero `a`, `x` such that `a • x = 0`)
+  `NoZeroSMulDivisors` (that is, there is no non-zero `a`, `x` such that `a • x = 0`)
   iff its torsion submodule is trivial.
 * `Submodule.QuotientTorsion.torsion_eq_bot` : quotienting by the torsion submodule makes the
   torsion submodule of the new module trivial. If `R` is a domain, we can derive an instance
   `Submodule.QuotientTorsion.noZeroSMulDivisors : NoZeroSMulDivisors R (M ⧸ torsion R M)`.
 
 ## Notation
 
-* The notions are defined for a `comm_semiring R` and a `module R M`. Some additional hypotheses on
+* The notions are defined for a `CommSemiring R` and a `Module R M`. Some additional hypotheses on
   `R` and `M` are required by some lemmas.
 * The letters `a`, `b`, ... are used for scalars (in `R`), while `x`, `y`, ... are used for vectors
   (in `M`).
@@ -851,4 +851,3 @@ theorem isTorsion_iff_isTorsion_int [AddCommGroup M] :
 #align add_monoid.is_torsion_iff_is_torsion_int AddMonoid.isTorsion_iff_isTorsion_int
 
 end AddMonoid
-

Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean

@@ -22,8 +22,6 @@ https://stacks.math.columbia.edu/tag/00FB
 
 open Ideal Polynomial PrimeSpectrum Set
 
-open Polynomial
-
 namespace AlgebraicGeometry
 
 namespace Polynomial
@@ -76,13 +74,13 @@ Stacks Project "Lemma 00FB", first part.
 
 https://stacks.math.columbia.edu/tag/00FB
 -/
-theorem isOpenMap_comap_c : IsOpenMap (PrimeSpectrum.comap (C : R →+* R[X])) := by
+theorem isOpenMap_comap_C : IsOpenMap (PrimeSpectrum.comap (C : R →+* R[X])) := by
   rintro U ⟨s, z⟩
   rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter,
     image_iUnion]
   simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]
   exact isOpen_iUnion fun f => isOpen_imageOfDf
-#align algebraic_geometry.polynomial.is_open_map_comap_C AlgebraicGeometry.Polynomial.isOpenMap_comap_c
+#align algebraic_geometry.polynomial.is_open_map_comap_C AlgebraicGeometry.Polynomial.isOpenMap_comap_C
 
 end Polynomial
 

Mathlib/AlgebraicGeometry/SheafedSpace.lean

@@ -24,17 +24,8 @@ presheaves.
 
 universe v u
 
-open CategoryTheory
-
-open TopCat
-
-open TopologicalSpace
-
-open Opposite
-
-open CategoryTheory.Limits
-
-open CategoryTheory.Category CategoryTheory.Functor
+open CategoryTheory TopCat TopologicalSpace Opposite CategoryTheory.Limits CategoryTheory.Category
+  CategoryTheory.Functor
 
 variable (C : Type u) [Category.{v} C]
 
@@ -69,7 +60,7 @@ set_option linter.uppercaseLean3 false in
 -- theorem as_coe (X : SheafedSpace.{v} C) : X.carrier = (X : TopCat.{v}) :=
 --   rfl
 -- set_option linter.uppercaseLean3 false in
--- #align algebraic_geometry.SheafedSpace.as_coe AlgebraicGeometry.SheafedSpace.as_coe
+#noalign algebraic_geometry.SheafedSpace.as_coe
 
 -- Porting note : this gives a `simpVarHead` error (`LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.`).
 -- so removed @[simp]

Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

@@ -34,9 +34,7 @@ rectangular box, additive function
 
 noncomputable section
 
-open Classical BigOperators
-
-open Function Set
+open Classical BigOperators Function Set
 
 namespace BoxIntegral
 
@@ -175,21 +173,21 @@ theorem sum_boxes_congr [Finite ι] (f : ι →ᵇᵃ[I₀] M) (hI : ↑I ≤ I
     (WithTop.coe_le_coe.2 <| π₂.le_of_mem hJ).trans hI]
 #align box_integral.box_additive_map.sum_boxes_congr BoxIntegral.BoxAdditiveMap.sum_boxes_congr
 
-section ToSmul
+section ToSMul
 
 variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E]
 
 /-- If `f` is a box-additive map, then so is the map sending `I` to the scalar multiplication
 by `f I` as a continuous linear map from `E` to itself. -/
-def toSmul (f : ι →ᵇᵃ[I₀] ℝ) : ι →ᵇᵃ[I₀] E →L[ℝ] E :=
+def toSMul (f : ι →ᵇᵃ[I₀] ℝ) : ι →ᵇᵃ[I₀] E →L[ℝ] E :=
   f.map (ContinuousLinearMap.lsmul ℝ ℝ).toLinearMap.toAddMonoidHom
-#align box_integral.box_additive_map.to_smul BoxIntegral.BoxAdditiveMap.toSmul
+#align box_integral.box_additive_map.to_smul BoxIntegral.BoxAdditiveMap.toSMul
 
 @[simp]
-theorem toSmul_apply (f : ι →ᵇᵃ[I₀] ℝ) (I : Box ι) (x : E) : f.toSmul I x = f I • x := rfl
-#align box_integral.box_additive_map.to_smul_apply BoxIntegral.BoxAdditiveMap.toSmul_apply
+theorem toSMul_apply (f : ι →ᵇᵃ[I₀] ℝ) (I : Box ι) (x : E) : f.toSMul I x = f I • x := rfl
+#align box_integral.box_additive_map.to_smul_apply BoxIntegral.BoxAdditiveMap.toSMul_apply
 
-end ToSmul
+end ToSMul
 
 /-- Given a box `I₀` in `ℝⁿ⁺¹`, `f x : Box (Fin n) → G` is a family of functions indexed by a real
 `x` and for `x ∈ [I₀.lower i, I₀.upper i]`, `f x` is box-additive on subboxes of the `i`-th face of

Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

@@ -60,9 +60,7 @@ separately.
 -/
 
 
-open NNReal ENNReal
-
-open NNReal ContinuousLinearMap MulOpposite
+open NNReal ENNReal ContinuousLinearMap MulOpposite
 
 universe u v
 
@@ -87,7 +85,9 @@ open MultiplierAlgebra
 lemma DoubleCentralizer.ext (𝕜 : Type u) (A : Type v) [NontriviallyNormedField 𝕜]
     [NonUnitalNormedRing A] [NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A]
     (a b : 𝓜(𝕜, A)) (h : a.toProd = b.toProd) : a = b := by
-  cases a; cases b; simpa using h
+  cases a
+  cases b
+  simpa using h
 
 namespace DoubleCentralizer
 
@@ -185,8 +185,8 @@ end Scalars
 instance instOne : One 𝓜(𝕜, A) :=
   ⟨⟨1, fun _x _y => rfl⟩⟩
 
-instance instMul : Mul 𝓜(𝕜, A)
-    where mul a b :=
+instance instMul : Mul 𝓜(𝕜, A) where
+  mul a b :=
     { toProd := (a.fst.comp b.fst, b.snd.comp a.snd)
       central := fun x y => show b.snd (a.snd x) * y = x * a.fst (b.fst y) by simp only [central] }
 
@@ -327,7 +327,7 @@ theorem pow_snd (n : ℕ) (a : 𝓜(𝕜, A)) : (a ^ n).snd = a.snd ^ n :=
   rfl
 #align double_centralizer.pow_snd DoubleCentralizer.pow_snd
 
-/-- The natural injection from `double_centralizer.to_prod` except the second coordinate inherits
+/-- The natural injection from `DoubleCentralizer.toProd` except the second coordinate inherits
 `MulOpposite.op`. The ring structure on `𝓜(𝕜, A)` is the pullback under this map. -/
 def toProdMulOpposite : 𝓜(𝕜, A) → (A →L[𝕜] A) × (A →L[𝕜] A)ᵐᵒᵖ := fun a =>
   (a.fst, MulOpposite.op a.snd)
@@ -376,7 +376,7 @@ def toProdMulOppositeHom : 𝓜(𝕜, A) →+* (A →L[𝕜] A) × (A →L[𝕜]
 #align double_centralizer.to_prod_mul_opposite_hom DoubleCentralizer.toProdMulOppositeHom
 
 /-- The module structure is inherited as the pullback under the additive group monomorphism
-`double_centralizer.to_prod : 𝓜(𝕜, A) →+ (A →L[𝕜] A) × (A →L[𝕜] A)` -/
+`DoubleCentralizer.toProd : 𝓜(𝕜, A) →+ (A →L[𝕜] A) × (A →L[𝕜] A)` -/
 instance instModule {S : Type _} [Semiring S] [Module S A] [SMulCommClass 𝕜 S A]
     [ContinuousConstSMul S A] [IsScalarTower S A A] [SMulCommClass S A A] : Module S 𝓜(𝕜, A) :=
   Function.Injective.module S toProdHom (ext (𝕜 := 𝕜) (A := A)) fun _x _y => rfl
@@ -424,7 +424,7 @@ section Star
 variable [StarRing 𝕜] [StarRing A] [StarModule 𝕜 A] [NormedStarGroup A]
 
 /-- The star operation on `a : 𝓜(𝕜, A)` is given by
-`(star a).to_prod = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star)`. -/
+`(star a).toProd = (star ∘ a.snd ∘ star, star ∘ a.fst ∘ star)`. -/
 instance instStar : Star 𝓜(𝕜, A) where
   star a :=
     { fst :=

Mathlib/Combinatorics/Configuration.lean

@@ -28,10 +28,10 @@ This file introduces abstract configurations of points and lines, and proves som
 * `Configuration.pointCount`: The number of lines through a given line.
 
 ## Main statements
-* `Configuration.HasLines.card_le`: `has_lines` implies `|P| ≤ |L|`.
-* `Configuration.HasPoints.card_le`: `has_points` implies `|L| ≤ |P|`.
-* `Configuration.HasLines.hasPoints`: `has_lines` and `|P| = |L|` implies `has_points`.
-* `Configuration.HasPoints.hasLines`: `has_points` and `|P| = |L|` implies `has_lines`.
+* `Configuration.HasLines.card_le`: `HasLines` implies `|P| ≤ |L|`.
+* `Configuration.HasPoints.card_le`: `HasPoints` implies `|L| ≤ |P|`.
+* `Configuration.HasLines.hasPoints`: `HasLines` and `|P| = |L|` implies `HasPoints`.
+* `Configuration.HasPoints.hasLines`: `HasPoints` and `|P| = |L|` implies `HasLines`.
 Together, these four statements say that any two of the following properties imply the third:
 (a) `HasLines`, (b) `HasPoints`, (c) `|P| = |L|`.