style: fix more doc-strings with indentation by an odd number of spaces (#24907)

Continuation of #24893.

Author: grunweg

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -385,7 +385,7 @@ variable (M : Type v) [AddCommMonoid M] [Module R M]
 -- local notation "S'" => (restrictScalars f).obj ⟨S⟩
 
 /-- Given an `R`-module M, consider Hom(S, M) -- the `R`-linear maps between S (as an `R`-module by
- means of restriction of scalars) and M. `S` acts on Hom(S, M) by `s • g = x ↦ g (x • s)`
+means of restriction of scalars) and M. `S` acts on Hom(S, M) by `s • g = x ↦ g (x • s)`
 -/
 instance hasSMul : SMul S <| (restrictScalars f).obj (of _ S) →ₗ[R] M where
   smul s g :=

Mathlib/Algebra/Group/Subgroup/Finite.lean

@@ -50,7 +50,7 @@ protected theorem list_prod_mem {l : List G} : (∀ x ∈ l, x ∈ K) → l.prod
 
 /-- Product of a multiset of elements in a subgroup of a `CommGroup` is in the subgroup. -/
 @[to_additive "Sum of a multiset of elements in an `AddSubgroup` of an `AddCommGroup` is in
- the `AddSubgroup`."]
+the `AddSubgroup`."]
 protected theorem multiset_prod_mem {G} [CommGroup G] (K : Subgroup G) (g : Multiset G) :
     (∀ a ∈ g, a ∈ K) → g.prod ∈ K :=
   multiset_prod_mem g
@@ -63,7 +63,7 @@ theorem multiset_noncommProd_mem (K : Subgroup G) (g : Multiset G) (comm) :
 /-- Product of elements of a subgroup of a `CommGroup` indexed by a `Finset` is in the
     subgroup. -/
 @[to_additive "Sum of elements in an `AddSubgroup` of an `AddCommGroup` indexed by a `Finset`
- is in the `AddSubgroup`."]
+is in the `AddSubgroup`."]
 protected theorem prod_mem {G : Type*} [CommGroup G] (K : Subgroup G) {ι : Type*} {t : Finset ι}
     {f : ι → G} (h : ∀ c ∈ t, f c ∈ K) : (∏ c ∈ t, f c) ∈ K :=
   prod_mem h
@@ -213,7 +213,7 @@ theorem pi_mem_of_mulSingle_mem [Finite η] [DecidableEq η] {H : Subgroup (∀
 
 /-- For finite index types, the `Subgroup.pi` is generated by the embeddings of the groups. -/
 @[to_additive "For finite index types, the `Subgroup.pi` is generated by the embeddings of the
- additive groups."]
+additive groups."]
 theorem pi_le_iff [DecidableEq η] [Finite η] {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
     pi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.mulSingle f i) (H i) ≤ J := by
   constructor
@@ -263,7 +263,7 @@ instance decidableMemRange (f : G →* N) [Fintype G] [DecidableEq N] : Decidabl
 Note: this instance can form a diamond with `Subtype.fintype` in the
 presence of `Fintype N`. -/
 @[to_additive "The range of a finite additive monoid under an additive monoid homomorphism is
- finite.
+finite.
 
 Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the presence
 of `Fintype N`."]
@@ -278,7 +278,7 @@ presence of `Fintype N`. -/
 @[to_additive "The range of a finite additive group under an additive group homomorphism is finite.
 
 Note: this instance can form a diamond with `Subtype.fintype` or `Subgroup.fintype` in the
- presence of `Fintype N`."]
+presence of `Fintype N`."]
 instance fintypeRange [Fintype G] [DecidableEq N] (f : G →* N) : Fintype (range f) :=
   Set.fintypeRange f
 

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -154,8 +154,8 @@ lemma IsRightCancelMulZero.to_isCancelMulZero [IsRightCancelMulZero M₀] :
 end CommSemigroup
 
 /-- A type `M` is a `CancelCommMonoidWithZero` if it is a commutative monoid with zero element,
- `0` is left and right absorbing,
-  and left/right multiplication by a non-zero element is injective. -/
+`0` is left and right absorbing,
+and left/right multiplication by a non-zero element is injective. -/
 class CancelCommMonoidWithZero (M₀ : Type*) extends CommMonoidWithZero M₀, IsLeftCancelMulZero M₀
 
 -- See note [lower cancel priority]

Mathlib/Algebra/GroupWithZero/Divisibility.lean

@@ -27,7 +27,7 @@ theorem eq_zero_of_zero_dvd (h : 0 ∣ a) : a = 0 :=
   Dvd.elim h fun c H' => H'.trans (zero_mul c)
 
 /-- Given an element `a` of a commutative semigroup with zero, there exists another element whose
-    product with zero equals `a` iff `a` equals zero. -/
+product with zero equals `a` iff `a` equals zero. -/
 @[simp]
 theorem zero_dvd_iff : 0 ∣ a ↔ a = 0 :=
   ⟨eq_zero_of_zero_dvd, fun h => by
@@ -41,13 +41,13 @@ theorem dvd_zero (a : α) : a ∣ 0 :=
 end SemigroupWithZero
 
 /-- Given two elements `b`, `c` of a `CancelMonoidWithZero` and a nonzero element `a`,
- `a*b` divides `a*c` iff `b` divides `c`. -/
+`a*b` divides `a*c` iff `b` divides `c`. -/
 theorem mul_dvd_mul_iff_left [CancelMonoidWithZero α] {a b c : α} (ha : a ≠ 0) :
     a * b ∣ a * c ↔ b ∣ c :=
   exists_congr fun d => by rw [mul_assoc, mul_right_inj' ha]
 
 /-- Given two elements `a`, `b` of a commutative `CancelMonoidWithZero` and a nonzero
-  element `c`, `a*c` divides `b*c` iff `a` divides `b`. -/
+element `c`, `a*c` divides `b*c` iff `a` divides `b`. -/
 theorem mul_dvd_mul_iff_right [CancelCommMonoidWithZero α] {a b c : α} (hc : c ≠ 0) :
     a * c ∣ b * c ↔ a ∣ b :=
   exists_congr fun d => by rw [mul_right_comm, mul_left_inj' hc]

Mathlib/Algebra/Module/LinearMap/End.lean

@@ -346,7 +346,7 @@ variable (S)
 
 /-- Applying a linear map at `v : M`, seen as `S`-linear map from `M →ₗ[R] M₂` to `M₂`.
 
- See `LinearMap.applyₗ` for a version where `S = R`. -/
+See `LinearMap.applyₗ` for a version where `S = R`. -/
 @[simps]
 def applyₗ' : M →+ (M →ₗ[R] M₂) →ₗ[S] M₂ where
   toFun v :=

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

@@ -39,7 +39,7 @@ The actual assumptions on `R` are weaker.
   `NoZeroDivisors R[A]`.
 
 TODO: move the rest of the docs to UniqueProds?
- `NoZeroDivisors.of_left_ordered` shows that if `R` is a semiring with no non-zero
+* `NoZeroDivisors.of_left_ordered` shows that if `R` is a semiring with no non-zero
   zero-divisors, `A` is a linearly ordered, add right cancel semigroup with strictly monotone
   left addition, then `R[A]` has no non-zero zero-divisors.
 * `NoZeroDivisors.of_right_ordered` shows that if `R` is a semiring with no non-zero

Mathlib/Algebra/MvPolynomial/Rename.lean

@@ -120,7 +120,7 @@ theorem rename_leftInverse {f : σ → τ} {g : τ → σ} (hf : Function.LeftIn
 
 theorem rename_rightInverse {f : σ → τ} {g : τ → σ} (hf : Function.RightInverse f g) :
     Function.RightInverse (rename f : MvPolynomial σ R → MvPolynomial τ R) (rename g) :=
- rename_leftInverse hf
+  rename_leftInverse hf
 
 theorem rename_surjective (f : σ → τ) (hf : Function.Surjective f) :
     Function.Surjective (rename f : MvPolynomial σ R → MvPolynomial τ R) :=

Mathlib/Algebra/Squarefree/Basic.lean

@@ -15,13 +15,13 @@ except the squares of units.
 Results about squarefree natural numbers are proved in `Data.Nat.Squarefree`.
 
 ## Main Definitions
- - `Squarefree r` indicates that `r` is only divisible by `x * x` if `x` is a unit.
+- `Squarefree r` indicates that `r` is only divisible by `x * x` if `x` is a unit.
 
 ## Main Results
- - `multiplicity.squarefree_iff_emultiplicity_le_one`: `x` is `Squarefree` iff for every `y`, either
+- `multiplicity.squarefree_iff_emultiplicity_le_one`: `x` is `Squarefree` iff for every `y`, either
   `emultiplicity y x ≤ 1` or `IsUnit y`.
- - `UniqueFactorizationMonoid.squarefree_iff_nodup_factors`: A nonzero element `x` of a unique
- factorization monoid is squarefree iff `factors x` has no duplicate factors.
+- `UniqueFactorizationMonoid.squarefree_iff_nodup_factors`: A nonzero element `x` of a unique
+  factorization monoid is squarefree iff `factors x` has no duplicate factors.
 
 ## Tags
 squarefree, multiplicity

Mathlib/Algebra/Star/Basic.lean

@@ -316,8 +316,8 @@ def starRingEnd : R →+* R := @starRingAut R _ _
 scoped[ComplexConjugate] notation "conj" => starRingEnd _
 
 /-- This is not a simp lemma, since we usually want simp to keep `starRingEnd` bundled.
- For example, for complex conjugation, we don't want simp to turn `conj x`
- into the bare function `star x` automatically since most lemmas are about `conj x`. -/
+For example, for complex conjugation, we don't want simp to turn `conj x`
+into the bare function `star x` automatically since most lemmas are about `conj x`. -/
 theorem starRingEnd_apply (x : R) : starRingEnd R x = star x := rfl
 
 /- Porting note (https://github.com/leanprover-community/mathlib4/issues/11119): removed `simp` attribute due to report by linter:

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -88,7 +88,7 @@ abbrev fV (i j : 𝒰.J) : v 𝒰 f g i j ⟶ pullback (𝒰.map i ≫ f) g :=
   pullback.fst _ _
 
 /-- The map `((Xᵢ ×[Z] Y) ×[X] Xⱼ) ×[Xᵢ ×[Z] Y] ((Xᵢ ×[Z] Y) ×[X] Xₖ)` ⟶
- `((Xⱼ ×[Z] Y) ×[X] Xₖ) ×[Xⱼ ×[Z] Y] ((Xⱼ ×[Z] Y) ×[X] Xᵢ)` needed for gluing -/
+`((Xⱼ ×[Z] Y) ×[X] Xₖ) ×[Xⱼ ×[Z] Y] ((Xⱼ ×[Z] Y) ×[X] Xᵢ)` needed for gluing -/
 def t' (i j k : 𝒰.J) :
     pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ pullback (fV 𝒰 f g j k) (fV 𝒰 f g j i) := by
   refine (pullbackRightPullbackFstIso ..).hom ≫ ?_