chore: tidy various files (#5355)

Archive/Imo/Imo1987Q1.lean

@@ -20,7 +20,7 @@ Let $p_{n, k}$ be the number of permutations of a set of cardinality `n ≥ 1` t
 elements. Prove that $∑_{k=0}^n k p_{n,k}=n!$.
 
 To prove this identity, we show that both sides are equal to the cardinality of the set
-`{(x : α, σ : perm α) | σ x = x}`, regrouping by `card (fixed_points σ)` for the left hand side and
+`{(x : α, σ : Perm α) | σ x = x}`, regrouping by `card (fixedPoints σ)` for the left hand side and
 by `x` for the right hand side.
 
 The original problem assumes `n ≥ 1`. It turns out that a version with `n * (n - 1)!` in the RHS
@@ -40,8 +40,8 @@ open Set (Iic)
 
 namespace Imo1987Q1
 
-/-- The set of pairs `(x : α, σ : perm α)` such that `σ x = x` is equivalent to the set of pairs
-`(x : α, σ : perm {x}ᶜ)`. -/
+/-- The set of pairs `(x : α, σ : Perm α)` such that `σ x = x` is equivalent to the set of pairs
+`(x : α, σ : Perm {x}ᶜ)`. -/
 def fixedPointsEquiv : { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x : α, Perm ({x}ᶜ : Set α) :=
   calc
     { σx : α × Perm α // σx.2 σx.1 = σx.1 } ≃ Σ x : α, { σ : Perm α // σ x = x } :=
@@ -57,7 +57,7 @@ theorem card_fixed_points :
     Finset.filter_eq', Finset.card_univ]
 #align imo1987_q1.card_fixed_points Imo1987Q1.card_fixed_points
 
-/-- Given `α : Type*` and `k : ℕ`, `fiber α k` is the set of permutations of `α` with exactly `k`
+/-- Given `α : Type _` and `k : ℕ`, `fiber α k` is the set of permutations of `α` with exactly `k`
 fixed points. -/
 def fiber (k : ℕ) : Set (Perm α) :=
   {σ : Perm α | card (fixedPoints σ) = k}
@@ -75,12 +75,12 @@ def p (k : ℕ) :=
   card (fiber α k)
 #align imo1987_q1.p Imo1987Q1.p
 
-/-- The set of triples `(k ≤ card α, σ ∈ fiber α k, x ∈ fixed_points σ)` is equivalent
-to the set of pairs `(x : α, σ : perm α)` such that `σ x = x`. The equivalence sends
-`(k, σ, x)` to `(x, σ)` and `(x, σ)` to `(card (fixed_points σ), σ, x)`.
+/-- The set of triples `(k ≤ card α, σ ∈ fiber α k, x ∈ fixedPoints σ)` is equivalent
+to the set of pairs `(x : α, σ : Perm α)` such that `σ x = x`. The equivalence sends
+`(k, σ, x)` to `(x, σ)` and `(x, σ)` to `(card (fixedPoints σ), σ, x)`.
 
 It is easy to see that the cardinality of the LHS is given by
-`∑ k : fin (card α + 1), k * p α k`. -/
+`∑ k : Fin (card α + 1), k * p α k`. -/
 def fixedPointsEquiv' :
     (Σ (k : Fin (card α + 1)) (σ : fiber α k), fixedPoints σ.1) ≃
       { σx : α × Perm α // σx.2 σx.1 = σx.1 } where
@@ -89,27 +89,26 @@ def fixedPointsEquiv' :
     ⟨⟨card (fixedPoints p.1.2), (card_subtype_le _).trans_lt (Nat.lt_succ_self _)⟩, ⟨p.1.2, rfl⟩,
       ⟨p.1.1, p.2⟩⟩
   left_inv := fun ⟨⟨k, hk⟩, ⟨σ, hσ⟩, ⟨x, hx⟩⟩ => by
-    simp only [mem_fiber, Fin.val_mk] at hσ 
+    simp only [mem_fiber, Fin.val_mk] at hσ
     subst k; rfl
   right_inv := fun ⟨⟨x, σ⟩, h⟩ => rfl
 #align imo1987_q1.fixed_points_equiv' Imo1987Q1.fixedPointsEquiv'
 
-/-- Main statement for any `(α : Type*) [fintype α]`. -/
+/-- Main statement for any `(α : Type _) [Fintype α]`. -/
 theorem main_fintype : ∑ k in range (card α + 1), k * p α k = card α * (card α - 1)! := by
   have A : ∀ (k) (σ : fiber α k), card (fixedPoints (↑σ : Perm α)) = k := fun k σ => σ.2
   simpa [A, ← Fin.sum_univ_eq_sum_range, -card_ofFinset, Finset.card_univ, card_fixed_points,
     mul_comm] using card_congr (fixedPointsEquiv' α)
 #align imo1987_q1.main_fintype Imo1987Q1.main_fintype
 
-/-- Main statement for permutations of `fin n`, a version that works for `n = 0`. -/
+/-- Main statement for permutations of `Fin n`, a version that works for `n = 0`. -/
 theorem main₀ (n : ℕ) : ∑ k in range (n + 1), k * p (Fin n) k = n * (n - 1)! := by
   simpa using main_fintype (Fin n)
 #align imo1987_q1.main₀ Imo1987Q1.main₀
 
-/-- Main statement for permutations of `fin n`. -/
+/-- Main statement for permutations of `Fin n`. -/
 theorem main {n : ℕ} (hn : 1 ≤ n) : ∑ k in range (n + 1), k * p (Fin n) k = n ! := by
   rw [main₀, Nat.mul_factorial_pred (zero_lt_one.trans_le hn)]
 #align imo1987_q1.main Imo1987Q1.main
 
 end Imo1987Q1
-

Mathlib/Analysis/BoxIntegral/Basic.lean

@@ -438,7 +438,7 @@ such that for every `c : ℝ≥0`, for every tagged partition `π` subordinate t
 additional distortion estimates if `BoxIntegral.IntegrationParams.bDistortion l = true`), the
 corresponding integral sum is `ε`-close to the integral.
 
-If `box.integral.integration_params.bRiemann = true`, then `r c x` does not depend on `x`. If
+If `BoxIntegral.IntegrationParams.bRiemann = true`, then `r c x` does not depend on `x`. If
 `ε ≤ 0`, then we use `r c x = 1`.  -/
 def convergenceR (h : Integrable I l f vol) (ε : ℝ) : ℝ≥0 → ℝⁿ → Ioi (0 : ℝ) :=
   if hε : 0 < ε then (hasIntegral_iff.1 h.hasIntegral ε hε).choose

Mathlib/Analysis/NormedSpace/Basic.lean

@@ -65,6 +65,7 @@ instance NormedField.toNormedSpace : NormedSpace α α where norm_smul_le a b :=
 -- shortcut instance
 instance NormedField.to_boundedSMul : BoundedSMul α α :=
   NormedSpace.boundedSMul
+#align normed_field.to_has_bounded_smul NormedField.to_boundedSMul
 
 theorem norm_zsmul (α) [NormedField α] [NormedSpace α β] (n : ℤ) (x : β) :
     ‖n • x‖ = ‖(n : α)‖ * ‖x‖ := by rw [← norm_smul, ← Int.smul_one_eq_coe, smul_assoc, one_smul]

Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

@@ -707,9 +707,9 @@ end Real
 
 section Tactics
 
--- /-!
--- ## Tactic extensions for real powers
--- -/
+/-!
+## Tactic extensions for real powers
+-/
 
 
 -- namespace NormNum

Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

@@ -14,7 +14,7 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
 # The `arctan` function.
 
 Inequalities, derivatives,
-and `real.tan` as a `local_homeomorph` between `(-(π / 2), π / 2)` and the whole line.
+and `Real.tan` as a `LocalHomeomorph` between `(-(π / 2), π / 2)` and the whole line.
 -/
 
 
@@ -214,7 +214,7 @@ theorem continuousAt_arctan {x : ℝ} : ContinuousAt arctan x :=
   continuous_arctan.continuousAt
 #align real.continuous_at_arctan Real.continuousAt_arctan
 
-/-- `real.tan` as a `local_homeomorph` between `(-(π / 2), π / 2)` and the whole line. -/
+/-- `Real.tan` as a `LocalHomeomorph` between `(-(π / 2), π / 2)` and the whole line. -/
 def tanLocalHomeomorph : LocalHomeomorph ℝ ℝ where
   toFun := tan
   invFun := arctan

Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

@@ -20,7 +20,7 @@ In this file we construct the algebraic closure of a field
 
 ## Main Definitions
 
-- `algebraic_closure k` is an algebraic closure of `k` (in the same universe).
+- `AlgebraicClosure k` is an algebraic closure of `k` (in the same universe).
   It is constructed by taking the polynomial ring generated by indeterminates `x_f`
   corresponding to monic irreducible polynomials `f` with coefficients in `k`, and quotienting
   out by a maximal ideal containing every `f(x_f)`, and then repeating this step countably
@@ -98,7 +98,7 @@ theorem spanEval_ne_top : spanEval k ≠ ⊤ := by
     MulZeroClass.mul_zero]
 #align algebraic_closure.span_eval_ne_top AlgebraicClosure.spanEval_ne_top
 
-/-- A random maximal ideal that contains `span_eval k` -/
+/-- A random maximal ideal that contains `spanEval k` -/
 def maxIdeal : Ideal (MvPolynomial (MonicIrreducible k) k) :=
   Classical.choose <| Ideal.exists_le_maximal _ <| spanEval_ne_top k
 #align algebraic_closure.max_ideal AlgebraicClosure.maxIdeal
@@ -111,7 +111,7 @@ theorem le_maxIdeal : spanEval k ≤ maxIdeal k :=
   (Classical.choose_spec <| Ideal.exists_le_maximal _ <| spanEval_ne_top k).2
 #align algebraic_closure.le_max_ideal AlgebraicClosure.le_maxIdeal
 
-/-- The first step of constructing `algebraic_closure`: adjoin a root of all monic polynomials -/
+/-- The first step of constructing `AlgebraicClosure`: adjoin a root of all monic polynomials -/
 def AdjoinMonic : Type u :=
   MvPolynomial (MonicIrreducible k) k ⧸ maxIdeal k
 #align algebraic_closure.adjoin_monic AlgebraicClosure.AdjoinMonic
@@ -124,7 +124,7 @@ instance AdjoinMonic.inhabited : Inhabited (AdjoinMonic k) :=
   ⟨37⟩
 #align algebraic_closure.adjoin_monic.inhabited AlgebraicClosure.AdjoinMonic.inhabited
 
-/-- The canonical ring homomorphism to `adjoin_monic k`. -/
+/-- The canonical ring homomorphism to `AdjoinMonic k`. -/
 def toAdjoinMonic : k →+* AdjoinMonic k :=
   (Ideal.Quotient.mk _).comp C
 #align algebraic_closure.to_adjoin_monic AlgebraicClosure.toAdjoinMonic
@@ -158,12 +158,12 @@ theorem AdjoinMonic.exists_root {f : k[X]} (hfm : f.Monic) (hfi : Irreducible f)
     exact le_maxIdeal k (Ideal.subset_span <| ⟨_, rfl⟩)⟩
 #align algebraic_closure.adjoin_monic.exists_root AlgebraicClosure.AdjoinMonic.exists_root
 
-/-- The `n`th step of constructing `algebraic_closure`, together with its `field` instance. -/
+/-- The `n`th step of constructing `AlgebraicClosure`, together with its `Field` instance. -/
 def stepAux (n : ℕ) : Σ α : Type u, Field α :=
   Nat.recOn n ⟨k, inferInstance⟩ fun _ ih => ⟨@AdjoinMonic ih.1 ih.2, @AdjoinMonic.field ih.1 ih.2⟩
 #align algebraic_closure.step_aux AlgebraicClosure.stepAux
 
-/-- The `n`th step of constructing `algebraic_closure`. -/
+/-- The `n`th step of constructing `AlgebraicClosure`. -/
 def Step (n : ℕ) : Type u :=
   (stepAux k n).1
 #align algebraic_closure.step AlgebraicClosure.Step
@@ -385,16 +385,15 @@ instance {R S : Type _} [CommSemiring R] [CommSemiring S] [Algebra R S] [Algebra
 
 /-- Canonical algebra embedding from the `n`th step to the algebraic closure. -/
 def ofStepHom (n) : Step k n →ₐ[k] AlgebraicClosure k :=
-  { ofStep k n with commutes' := by {
-  --Porting Note: Originally `(fun x => Ring.DirectLimit.of_f n.zero_le x)`
-  -- I think one problem was in recognizing that we want `toStepOfLE` in `of_f`
+  { ofStep k n with
+    commutes' := by
+    --Porting Note: Originally `(fun x => Ring.DirectLimit.of_f n.zero_le x)`
+    -- I think one problem was in recognizing that we want `toStepOfLE` in `of_f`
       intro x
       simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
           MonoidHom.coe_coe]
       convert @Ring.DirectLimit.of_f ℕ _ (Step k) _ (fun m n h => (toStepOfLE k m n h : _ → _))
-          0 n n.zero_le x
-    }
-  }
+          0 n n.zero_le x }
 #align algebraic_closure.of_step_hom AlgebraicClosure.ofStepHom
 
 theorem isAlgebraic : Algebra.IsAlgebraic k (AlgebraicClosure k) := fun z =>

Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

@@ -19,15 +19,15 @@ This file specializes the theory of minpoly to the case of an algebra over a GCD
 
 ## Main results
 
- * `is_integrally_closed_eq_field_fractions`: For integrally closed domains, the minimal polynomial
-    over the ring is the same as the minimal polynomial over the fraction field.
+ * `minpoly.isIntegrallyClosed_eq_field_fractions`: For integrally closed domains, the minimal
+    polynomial over the ring is the same as the minimal polynomial over the fraction field.
 
- * `is_integrally_closed_dvd` : For integrally closed domains, the minimal polynomial divides any
-    primitive polynomial that has the integral element as root.
+ * `minpoly.isIntegrallyClosed_dvd` : For integrally closed domains, the minimal polynomial divides
+    any primitive polynomial that has the integral element as root.
 
- * `is_integrally_closed_unique` : The minimal polynomial of an element `x` is uniquely
-    characterized by its defining property: if there is another monic polynomial of minimal degree
-    that has `x` as a root, then this polynomial is equal to the minimal polynomial of `x`.
+ * `minpoly.IsIntegrallyClosed.Minpoly.unique` : The minimal polynomial of an element `x` is
+    uniquely characterized by its defining property: if there is another monic polynomial of minimal
+    degree that has `x` as a root, then this polynomial is equal to the minimal polynomial of `x`.
 
 -/
 
@@ -48,7 +48,7 @@ variable (K L : Type _) [Field K] [Algebra R K] [IsFractionRing R K] [Field L] [
 variable [IsIntegrallyClosed R]
 
 /-- For integrally closed domains, the minimal polynomial over the ring is the same as the minimal
-polynomial over the fraction field. See `minpoly.is_integrally_closed_eq_field_fractions'` if
+polynomial over the fraction field. See `minpoly.isIntegrallyClosed_eq_field_fractions'` if
 `S` is already a `K`-algebra. -/
 theorem isIntegrallyClosed_eq_field_fractions [IsDomain S] {s : S} (hs : IsIntegral R s) :
     minpoly K (algebraMap S L s) = (minpoly R s).map (algebraMap R K) := by
@@ -60,7 +60,7 @@ theorem isIntegrallyClosed_eq_field_fractions [IsDomain S] {s : S} (hs : IsInteg
 #align minpoly.is_integrally_closed_eq_field_fractions minpoly.isIntegrallyClosed_eq_field_fractions
 
 /-- For integrally closed domains, the minimal polynomial over the ring is the same as the minimal
-polynomial over the fraction field. Compared to `minpoly.is_integrally_closed_eq_field_fractions`,
+polynomial over the fraction field. Compared to `minpoly.isIntegrallyClosed_eq_field_fractions`,
 this version is useful if the element is in a ring that is already a `K`-algebra. -/
 theorem isIntegrallyClosed_eq_field_fractions' [IsDomain S] [Algebra K S] [IsScalarTower R K S]
     {s : S} (hs : IsIntegral R s) : minpoly K s = (minpoly R s).map (algebraMap R K) := by
@@ -157,8 +157,6 @@ noncomputable section AdjoinRoot
 
 open Algebra Polynomial AdjoinRoot
 
--- porting note: commented out because of redundant binder annotation update
---variable {R}
 variable {x : S}
 
 theorem ToAdjoin.injective (hx : IsIntegral R x) : Function.Injective (Minpoly.toAdjoin R x) := by
@@ -172,14 +170,14 @@ theorem ToAdjoin.injective (hx : IsIntegral R x) : Function.Injective (Minpoly.t
   rw [← hP, hQ, RingHom.map_mul, mk_self, MulZeroClass.zero_mul]
 #align minpoly.to_adjoin.injective minpoly.ToAdjoin.injective
 
-/-- The algebra isomorphism `adjoin_root (minpoly R x) ≃ₐ[R] adjoin R x` -/
+/-- The algebra isomorphism `AdjoinRoot (minpoly R x) ≃ₐ[R] adjoin R x` -/
 @[simps!]
 def equivAdjoin (hx : IsIntegral R x) : AdjoinRoot (minpoly R x) ≃ₐ[R] adjoin R ({x} : Set S) :=
   AlgEquiv.ofBijective (Minpoly.toAdjoin R x)
     ⟨minpoly.ToAdjoin.injective hx, Minpoly.toAdjoin.surjective R x⟩
 #align minpoly.equiv_adjoin minpoly.equivAdjoin
 
-/-- The `power_basis` of `adjoin R {x}` given by `x`. See `algebra.adjoin.power_basis` for a version
+/-- The `PowerBasis` of `adjoin R {x}` given by `x`. See `Algebra.adjoin.powerBasis` for a version
 over a field. -/
 @[simps!]
 def Algebra.adjoin.powerBasis' (hx : IsIntegral R x) :

Mathlib/FieldTheory/RatFunc.lean

@@ -76,11 +76,11 @@ We define the degree of a rational function, with values in `ℤ`:
 To provide good API encapsulation and speed up unification problems,
 `RatFunc` is defined as a structure, and all operations are `@[irreducible] def`s
 
-We need a couple of maps to set up the `field` and `IsFractionRing` structure,
-namely `RatFunc.of_fraction_ring`, `RatFunc.to_fraction_ring`, `RatFunc.mk` and
-`RatFunc.to_fraction_ring_ring_equiv`.
-All these maps get `simp`ed to bundled morphisms like `algebra_map K[X] (RatFunc K)`
-and `is_localization.alg_equiv`.
+We need a couple of maps to set up the `Field` and `IsFractionRing` structure,
+namely `RatFunc.ofFractionRing`, `RatFunc.toFractionRing`, `RatFunc.mk` and
+`RatFunc.toFractionRingRingEquiv`.
+All these maps get `simp`ed to bundled morphisms like `algebraMap K[X] (RatFunc K)`
+and `IsLocalization.algEquiv`.
 
 There are separate lifts and maps of homomorphisms, to provide routes of lifting even when
 the codomain is not a field or even an integral domain.

Mathlib/GroupTheory/Schreier.lean

@@ -22,7 +22,7 @@ In this file we prove Schreier's lemma.
 - `closure_mul_image_eq` : **Schreier's Lemma**: If `R : Set G` is a right_transversal
   of `H : Subgroup G` with `1 ∈ R`, and if `G` is generated by `S : Set G`,
   then `H` is generated by the `Set` `(R * S).image (fun g ↦ g * (toFun hR g)⁻¹)`.
-- `fG_of_index_ne_zero` : **Schreier's Lemma**: A finite index subgroup of a finitely generated
+- `fg_of_index_ne_zero` : **Schreier's Lemma**: A finite index subgroup of a finitely generated
   group is finitely generated.
 - `card_commutator_le_of_finite_commutatorSet`: A theorem of Schur: The size of the commutator
   subgroup is bounded in terms of the number of commutators.
@@ -129,15 +129,15 @@ theorem exists_finset_card_le_mul [FiniteIndex H] {S : Finset G} (hS : closure (
 
 /-- **Schreier's Lemma**: A finite index subgroup of a finitely generated
   group is finitely generated. -/
-instance fG_of_index_ne_zero [hG : Group.FG G] [FiniteIndex H] : Group.FG H := by
+instance fg_of_index_ne_zero [hG : Group.FG G] [FiniteIndex H] : Group.FG H := by
   obtain ⟨S, hS⟩ := hG.1
   obtain ⟨T, -, hT⟩ := exists_finset_card_le_mul H hS
   exact ⟨⟨T, hT⟩⟩
-#align subgroup.fg_of_index_ne_zero Subgroup.fG_of_index_ne_zero
+#align subgroup.fg_of_index_ne_zero Subgroup.fg_of_index_ne_zero
 
 theorem rank_le_index_mul_rank [hG : Group.FG G] [FiniteIndex H] :
     Group.rank H ≤ H.index * Group.rank G := by
-  haveI := H.fG_of_index_ne_zero
+  haveI := H.fg_of_index_ne_zero
   obtain ⟨S, hS₀, hS⟩ := Group.rank_spec G
   obtain ⟨T, hT₀, hT⟩ := exists_finset_card_le_mul H hS
   calc

Mathlib/GroupTheory/Subsemigroup/Operations.lean

@@ -788,7 +788,7 @@ theorem srange_top_iff_surjective {N} [Mul N] {f : M →ₙ* N} :
 
 /-- The range of a surjective semigroup hom is the whole of the codomain. -/
 @[to_additive (attr := simp)
-  "The range of a surjective `add_semigroup` hom is the whole of the codomain."]
+  "The range of a surjective `AddSemigroup` hom is the whole of the codomain."]
 theorem srange_top_of_surjective {N} [Mul N] (f : M →ₙ* N) (hf : Function.Surjective f) :
     f.srange = (⊤ : Subsemigroup N) :=
   srange_top_iff_surjective.2 hf