chore: tidy various files (#3474)

Mathlib/CategoryTheory/Limits/Over.lean

@@ -18,22 +18,22 @@ import Mathlib.CategoryTheory.Limits.Comma
 /-!
 # Limits and colimits in the over and under categories
 
-Show that the forgetful functor `forget X : over X ⥤ C` creates colimits, and hence `over X` has
-any colimits that `C` has (as well as the dual that `forget X : under X ⟶ C` creates limits).
+Show that the forgetful functor `forget X : Over X ⥤ C` creates colimits, and hence `Over X` has
+any colimits that `C` has (as well as the dual that `forget X : Under X ⟶ C` creates limits).
 
-Note that the folder `category_theory.limits.shapes.constructions.over` further shows that
-`forget X : over X ⥤ C` creates connected limits (so `over X` has connected limits), and that
-`over X` has `J`-indexed products if `C` has `J`-indexed wide pullbacks.
+Note that the folder `CategoryTheory.Limits.Shapes.Constructions.Over` further shows that
+`forget X : Over X ⥤ C` creates connected limits (so `Over X` has connected limits), and that
+`Over X` has `J`-indexed products if `C` has `J`-indexed wide pullbacks.
 
-TODO: If `C` has binary products, then `forget X : over X ⥤ C` has a right adjoint.
+TODO: If `C` has binary products, then `forget X : Over X ⥤ C` has a right adjoint.
 -/
 
 
 noncomputable section
 
+-- morphism levels before object levels. See note [category_theory universes].
 universe v u
 
--- morphism levels before object levels. See note [category_theory universes].
 open CategoryTheory CategoryTheory.Limits
 
 variable {J : Type v} [SmallCategory J]
@@ -79,7 +79,7 @@ variable [HasPullbacks C]
 
 open Tactic
 
-/-- When `C` has pullbacks, a morphism `f : X ⟶ Y` induces a functor `over Y ⥤ over X`,
+/-- When `C` has pullbacks, a morphism `f : X ⟶ Y` induces a functor `Over Y ⥤ Over X`,
 by pulling back a morphism along `f`. -/
 @[simps]
 def pullback {X Y : C} (f : X ⟶ Y) : Over Y ⥤ Over X where
@@ -89,11 +89,10 @@ def pullback {X Y : C} (f : X ⟶ Y) : Over Y ⥤ Over X where
       (by aesop_cat)
 #align category_theory.over.pullback CategoryTheory.Over.pullback
 
-/-- `over.map f` is left adjoint to `over.pullback f`. -/
+/-- `Over.map f` is left adjoint to `Over.pullback f`. -/
 def mapPullbackAdj {A B : C} (f : A ⟶ B) : Over.map f ⊣ pullback f :=
   Adjunction.mkOfHomEquiv
-    {
-      homEquiv := fun g h =>
+    { homEquiv := fun g h =>
         { toFun := fun X =>
             Over.homMk (pullback.lift X.left g.hom (Over.w X)) (pullback.lift_snd _ _ _)
           invFun := fun Y => by
@@ -169,7 +168,7 @@ section
 
 variable [HasPushouts C]
 
-/-- When `C` has pushouts, a morphism `f : X ⟶ Y` induces a functor `under X ⥤ under Y`,
+/-- When `C` has pushouts, a morphism `f : X ⟶ Y` induces a functor `Under X ⥤ Under Y`,
 by pushing a morphism forward along `f`. -/
 @[simps]
 def pushout {X Y : C} (f : X ⟶ Y) : Under X ⥤ Under Y where

Mathlib/Data/Real/Pointwise.lean

@@ -14,7 +14,7 @@ import Mathlib.Data.Real.Basic
 /-!
 # Pointwise operations on sets of reals
 
-This file relates `Inf (a • s)`/`Sup (a • s)` with `a • Inf s`/`a • Sup s` for `s : Set ℝ`.
+This file relates `infₛ (a • s)`/`supₛ (a • s)` with `a • infₛ s`/`a • supₛ s` for `s : Set ℝ`.
 
 From these, it relates `⨅ i, a • f i` / `⨆ i, a • f i` with `a • (⨅ i, f i)` / `a • (⨆ i, f i)`,
 and provides lemmas about distributing `*` over `⨅` and `⨆`.

Mathlib/GroupTheory/FreeGroup.lean

@@ -995,14 +995,19 @@ def freeGroupUnitEquivInt : FreeGroup Unit ≃ ℤ
   invFun x := of () ^ x
   left_inv := by
     rintro ⟨L⟩
-    simp
+    simp only [quot_mk_eq_mk, map.mk, sum_mk, List.map_map]
     exact List.recOn L
      (by rfl)
      (fun ⟨⟨⟩, b⟩ tl ih => by
         cases b <;> simp [zpow_add] at ih⊢ <;> rw [ih] <;> rfl)
   right_inv x :=
-    Int.induction_on x (by simp) (fun i ih => by simp at ih; simp [zpow_add, ih]) fun i ih => by
-      simp at ih; simp [zpow_add, ih, sub_eq_add_neg]
+    Int.induction_on x (by simp)
+      (fun i ih => by
+        simp only [zpow_coe_nat, map_pow, map.of] at ih
+        simp [zpow_add, ih])
+      (fun i ih => by
+        simp only [zpow_neg, zpow_coe_nat, map_inv, map_pow, map.of, sum.map_inv, neg_inj] at ih
+        simp [zpow_add, ih, sub_eq_add_neg])
 #align free_group.free_group_unit_equiv_int FreeGroup.freeGroupUnitEquivInt
 
 section Category

Mathlib/GroupTheory/OrderOfElement.lean

@@ -36,9 +36,7 @@ order of an element
 -/
 
 
-open Function Nat
-
-open Pointwise
+open Function Nat Pointwise
 
 universe u v
 
@@ -134,8 +132,8 @@ end IsOfFinOrder
 /-- `orderOf x` is the order of the element `x`, i.e. the `n ≥ 1`, s.t. `x ^ n = 1` if it exists.
 Otherwise, i.e. if `x` is of infinite order, then `orderOf x` is `0` by convention.-/
 @[to_additive
-  "`add_order_of a` is the order of the element `a`, i.e. the `n ≥ 1`, s.t. `n • a = 0` if it
-  exists. Otherwise, i.e. if `a` is of infinite order, then `add_order_of a` is `0` by convention."]
+  "`addOrderOf a` is the order of the element `a`, i.e. the `n ≥ 1`, s.t. `n • a = 0` if it
+  exists. Otherwise, i.e. if `a` is of infinite order, then `addOrderOf a` is `0` by convention."]
 noncomputable def orderOf (x : G) : ℕ :=
   minimalPeriod (x * .) 1
 #align order_of orderOf
@@ -430,7 +428,7 @@ theorem isOfFinOrder_mul (hx : IsOfFinOrder x) (hy : IsOfFinOrder y) : IsOfFinOr
   with `y`, then `x * y` has the same order as `y`. -/
 @[to_additive addOrderOf_add_eq_right_of_forall_prime_mul_dvd
   "If each prime factor of
-  `add_order_of x` has higher multiplicity in `add_order_of y`, and `x` commutes with `y`,
+  `addOrderOf x` has higher multiplicity in `addOrderOf y`, and `x` commutes with `y`,
   then `x + y` has the same order as `y`."]
 theorem orderOf_mul_eq_right_of_forall_prime_mul_dvd (hy : IsOfFinOrder y)
     (hdvd : ∀ p : ℕ, p.Prime → p ∣ orderOf x → p * orderOf x ∣ orderOf y) :
@@ -705,7 +703,7 @@ theorem exists_pow_eq_one [Finite G] (x : G) : IsOfFinOrder x := by
 
 /-- This is the same as `orderOf_pos'` but with one fewer explicit assumption since this is
   automatic in case of a finite cancellative monoid.-/
-@[to_additive "This is the same as `add_order_of_pos' but with one fewer explicit
+@[to_additive "This is the same as `addOrderOf_pos' but with one fewer explicit
 assumption since this is automatic in case of a finite cancellative additive monoid."]
 theorem orderOf_pos [Finite G] (x : G) : 0 < orderOf x :=
   orderOf_pos' (exists_pow_eq_one x)
@@ -716,8 +714,8 @@ open Nat
 
 /-- This is the same as `orderOf_pow'` and `orderOf_pow''` but with one assumption less which is
 automatic in the case of a finite cancellative monoid.-/
-@[to_additive "This is the same as `add_order_of_nsmul'` and
-`add_order_of_nsmul` but with one assumption less which is automatic in the case of a
+@[to_additive "This is the same as `addOrderOf_nsmul'` and
+`addOrderOf_nsmul` but with one assumption less which is automatic in the case of a
 finite cancellative additive monoid."]
 theorem orderOf_pow [Finite G] (x : G) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n :=
   orderOf_pow'' _ _ (exists_pow_eq_one _)
@@ -739,8 +737,8 @@ noncomputable instance decidablePowers : DecidablePred (· ∈ Submonoid.powers
 
 /-- The equivalence between `Fin (orderOf x)` and `Submonoid.powers x`, sending `i` to `x ^ i`."-/
 @[to_additive finEquivMultiples
-  "The equivalence between `fin (add_order_of a)` and
-  `add_submonoid.multiples a`, sending `i` to `i • a`."]
+  "The equivalence between `Fin (addOrderOf a)` and
+  `AddSubmonoid.multiples a`, sending `i` to `i • a`."]
 noncomputable def finEquivPowers [Finite G] (x : G) :
     Fin (orderOf x) ≃ (Submonoid.powers x : Set G) :=
   Equiv.ofBijective (fun n => ⟨x ^ (n:ℕ), ⟨n, rfl⟩⟩)
@@ -847,8 +845,8 @@ noncomputable instance decidableZpowers : DecidablePred (· ∈ Subgroup.zpowers
 #align decidable_zmultiples decidableZmultiples
 
 /-- The equivalence between `Fin (orderOf x)` and `Subgroup.zpowers x`, sending `i` to `x ^ i`. -/
-@[to_additive finEquivZmultiples "The equivalence between `fin (add_order_of a)` and
-`subgroup.zmultiples a`, sending `i` to `i • a`."]
+@[to_additive finEquivZmultiples "The equivalence between `Fin (addOrderOf a)` and
+`Subgroup.zmultiples a`, sending `i` to `i • a`."]
 noncomputable def finEquivZpowers [Finite G] (x : G) :
     Fin (orderOf x) ≃ (Subgroup.zpowers x : Set G) :=
   (finEquivPowers x).trans (Equiv.Set.ofEq (powers_eq_zpowers x))
@@ -873,7 +871,7 @@ theorem finEquivZpowers_symm_apply [Finite G] (x : G) (n : ℕ) {hn : ∃ m : 
 /-- The equivalence between `Subgroup.zpowers` of two elements `x, y` of the same order, mapping
   `x ^ i` to `y ^ i`. -/
 @[to_additive zmultiplesEquivZmultiples
-  "The equivalence between `subgroup.zmultiples` of two elements `a, b` of the same additive order,
+  "The equivalence between `Subgroup.zmultiples` of two elements `a, b` of the same additive order,
   mapping `i • a` to `i • b`."]
 noncomputable def zpowersEquivZpowers [Finite G] (h : orderOf x = orderOf y) :
     (Subgroup.zpowers x : Set G) ≃ (Subgroup.zpowers y : Set G) :=

Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

@@ -121,7 +121,7 @@ theorem coe_mk (f : P1 → P2) (linear add) : ((mk f linear add : P1 →ᵃ[k] P
   rfl
 #align affine_map.coe_mk AffineMap.coe_mk
 
-/-- `to_fun` is the same as the result of coercing to a function. -/
+/-- `toFun` is the same as the result of coercing to a function. -/
 @[simp]
 theorem toFun_eq_coe (f : P1 →ᵃ[k] P2) : f.toFun = ⇑f :=
   rfl

Mathlib/LinearAlgebra/Matrix/DotProduct.lean

@@ -37,7 +37,7 @@ variable {R : Type v} {n : Type w}
 
 namespace Matrix
 
-section semiring
+section Semiring
 
 variable [Semiring R] [Fintype n]
 
@@ -72,9 +72,9 @@ theorem dotProduct_eq_zero_iff {v : n → R} : (∀ w, dotProduct v w = 0) ↔ v
   ⟨fun h => dotProduct_eq_zero v h, fun h w => h.symm ▸ zero_dotProduct w⟩
 #align matrix.dot_product_eq_zero_iff Matrix.dotProduct_eq_zero_iff
 
-end semiring
+end Semiring
 
-section self
+section Self
 
 variable [Fintype n]
 
@@ -100,6 +100,6 @@ theorem dotProduct_self_star_eq_zero [PartialOrder R] [NonUnitalRing R] [StarOrd
     by simp [Function.funext_iff, mul_eq_zero]
 #align matrix.dot_product_self_star_eq_zero Matrix.dotProduct_self_star_eq_zero
 
-end self
+end Self
 
 end Matrix

Mathlib/ModelTheory/LanguageMap.lean

@@ -62,7 +62,7 @@ variable {L L'}
 
 namespace LHom
 
-/-- Defines a map between languages defined with `language.mk₂`. -/
+/-- Defines a map between languages defined with `Language.mk₂`. -/
 protected def mk₂ {c f₁ f₂ : Type u} {r₁ r₂ : Type v} (φ₀ : c → L'.Constants)
     (φ₁ : f₁ → L'.Functions 1) (φ₂ : f₂ → L'.Functions 2) (φ₁' : r₁ → L'.Relations 1)
     (φ₂' : r₂ → L'.Relations 2) : Language.mk₂ c f₁ f₂ r₁ r₂ →ᴸ L' :=

Mathlib/Order/Filter/Pointwise.lean

@@ -58,9 +58,7 @@ filter multiplication, filter addition, pointwise addition, pointwise multiplica
 -/
 
 
-open Function Set
-
-open Filter Pointwise
+open Function Set Filter Pointwise
 
 variable {F α β γ δ ε : Type _}
 
@@ -151,8 +149,8 @@ theorem one_prod_one [One β] : (1 : Filter α) ×ᶠ (1 : Filter β) = 1 :=
 #align filter.one_prod_one Filter.one_prod_one
 #align filter.zero_sum_zero Filter.zero_sum_zero
 
-/-- `pure` as a `one_hom`. -/
-@[to_additive "`pure` as a `zero_hom`."]
+/-- `pure` as a `OneHom`. -/
+@[to_additive "`pure` as a `ZeroHom`."]
 def pureOneHom : OneHom α (Filter α) :=
   ⟨pure, pure_one⟩
 #align filter.pure_one_hom Filter.pureOneHom
@@ -581,8 +579,7 @@ scoped[Pointwise] attribute [instance] Filter.instNSMul Filter.instNPow
 
 /-- `Filter α` is a `Semigroup` under pointwise operations if `α` is.-/
 @[to_additive "`Filter α` is an `AddSemigroup` under pointwise operations if `α` is."]
-protected def semigroup [Semigroup α] : Semigroup (Filter α)
-    where
+protected def semigroup [Semigroup α] : Semigroup (Filter α) where
   mul := (· * ·)
   mul_assoc _ _ _ := map₂_assoc mul_assoc
 #align filter.semigroup Filter.semigroup
@@ -601,8 +598,7 @@ variable [MulOneClass α] [MulOneClass β]
 
 /-- `Filter α` is a `MulOneClass` under pointwise operations if `α` is. -/
 @[to_additive "`Filter α` is an `AddZeroClass` under pointwise operations if `α` is."]
-protected def mulOneClass : MulOneClass (Filter α)
-    where
+protected def mulOneClass : MulOneClass (Filter α) where
   one := 1
   mul := (· * ·)
   one_mul := map₂_left_identity one_mul
@@ -617,8 +613,7 @@ scoped[Pointwise] attribute [instance] Filter.semigroup Filter.addSemigroup
 `Filter α →* Filter β` induced by `map φ`. -/
 @[to_additive "If `φ : α →+ β` then `mapAddMonoidHom φ` is the monoid homomorphism
  `Filter α →+ Filter β` induced by `map φ`."]
-def mapMonoidHom [MonoidHomClass F α β] (φ : F) : Filter α →* Filter β
-    where
+def mapMonoidHom [MonoidHomClass F α β] (φ : F) : Filter α →* Filter β where
   toFun := map φ
   map_one' := Filter.map_one φ
   map_mul' _ _ := Filter.map_mul φ
@@ -716,19 +711,13 @@ theorem top_mul_top : (⊤ : Filter α) * ⊤ = ⊤ :=
 #align filter.top_mul_top Filter.top_mul_top
 #align filter.top_add_top Filter.top_add_top
 
---TODO: `to_additive` trips up on the `1 : ℕ` used in the pattern-matching.
-theorem nsmul_top {α : Type _} [AddMonoid α] : ∀ {n : ℕ}, n ≠ 0 → n • (⊤ : Filter α) = ⊤
-  | 0 => fun h => (h rfl).elim
-  | 1 => fun _ => one_nsmul _
-  | n + 2 => fun _ => by rw [succ_nsmul, nsmul_top n.succ_ne_zero, top_add_top]
-#align filter.nsmul_top Filter.nsmul_top
-
-@[to_additive existing nsmul_top]
+@[to_additive nsmul_top]
 theorem top_pow : ∀ {n : ℕ}, n ≠ 0 → (⊤ : Filter α) ^ n = ⊤
   | 0 => fun h => (h rfl).elim
   | 1 => fun _ => pow_one _
   | n + 2 => fun _ => by rw [pow_succ, top_pow n.succ_ne_zero, top_mul_top]
 #align filter.top_pow Filter.top_pow
+#align filter.nsmul_top Filter.nsmul_top
 
 @[to_additive]
 protected theorem _root_.IsUnit.filter : IsUnit a → IsUnit (pure a : Filter α) :=
@@ -771,10 +760,9 @@ protected theorem mul_eq_one_iff : f * g = 1 ↔ ∃ a b, f = pure a ∧ g = pur
  `α` is."]
 -- porting note: `to_additive` guessed `divisionAddMonoid`
 protected def divisionMonoid : DivisionMonoid (Filter α) :=
-  { Filter.monoid, Filter.instInvolutiveInv, Filter.instDiv, @Filter.instZPow α _ _ _ with
+  { Filter.monoid, Filter.instInvolutiveInv, Filter.instDiv, Filter.instZPow (α := α) with
     mul_inv_rev := fun s t => map_map₂_antidistrib mul_inv_rev
-    inv_eq_of_mul := fun s t h =>
-      by
+    inv_eq_of_mul := fun s t h => by
       obtain ⟨a, b, rfl, rfl, hab⟩ := Filter.mul_eq_one_iff.1 h
       rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
     div_eq_mul_inv := fun f g => map_map₂_distrib_right div_eq_mul_inv }
@@ -806,8 +794,7 @@ protected def divisionCommMonoid [DivisionCommMonoid α] : DivisionCommMonoid (F
 
 /-- `Filter α` has distributive negation if `α` has. -/
 protected def instDistribNeg [Mul α] [HasDistribNeg α] : HasDistribNeg (Filter α) :=
-  {
-    Filter.instInvolutiveNeg with
+  { Filter.instInvolutiveNeg with
     neg_mul := fun _ _ => map₂_map_left_comm neg_mul
     mul_neg := fun _ _ => map_map₂_right_comm mul_neg }
 #align filter.has_distrib_neg Filter.instDistribNeg
@@ -1314,8 +1301,7 @@ instance isCentralScalar [SMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α
 `Filter α` on `Filter β`. -/
 @[to_additive "An additive action of an additive monoid `α` on a type `β` gives an additive action
  of `Filter α` on `Filter β`"]
-protected def mulAction [Monoid α] [MulAction α β] : MulAction (Filter α) (Filter β)
-    where
+protected def mulAction [Monoid α] [MulAction α β] : MulAction (Filter α) (Filter β) where
   one_smul f := map₂_pure_left.trans <| by simp_rw [one_smul, map_id']
   mul_smul f g h := map₂_assoc mul_smul
 #align filter.mul_action Filter.mulAction
@@ -1325,8 +1311,7 @@ protected def mulAction [Monoid α] [MulAction α β] : MulAction (Filter α) (F
 -/
 @[to_additive "An additive action of an additive monoid on a type `β` gives an additive action on
  `Filter β`."]
-protected def mulActionFilter [Monoid α] [MulAction α β] : MulAction α (Filter β)
-    where
+protected def mulActionFilter [Monoid α] [MulAction α β] : MulAction α (Filter β) where
   mul_smul a b f := by simp only [← map_smul, map_map, Function.comp, ← mul_smul]
   one_smul f := by simp only [← map_smul, one_smul, map_id']
 #align filter.mul_action_filter Filter.mulActionFilter
@@ -1338,16 +1323,14 @@ scoped[Pointwise] attribute [instance] Filter.mulAction Filter.addAction Filter.
 /-- A distributive multiplicative action of a monoid on an additive monoid `β` gives a distributive
 multiplicative action on `Filter β`. -/
 protected def distribMulActionFilter [Monoid α] [AddMonoid β] [DistribMulAction α β] :
-    DistribMulAction α (Filter β)
-    where
+    DistribMulAction α (Filter β) where
   smul_add _ _ _ := map_map₂_distrib <| smul_add _
   smul_zero _ := (map_pure _ _).trans <| by dsimp only; rw [smul_zero, pure_zero]
 #align filter.distrib_mul_action_filter Filter.distribMulActionFilter
 
-/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `set β`. -/
+/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`. -/
 protected def mulDistribMulActionFilter [Monoid α] [Monoid β] [MulDistribMulAction α β] :
-    MulDistribMulAction α (Set β)
-    where
+    MulDistribMulAction α (Set β) where
   smul_mul _ _ _ := image_image2_distrib <| smul_mul' _
   smul_one _ := image_singleton.trans <| by rw [smul_one, singleton_one]
 #align filter.mul_distrib_mul_action_filter Filter.mulDistribMulActionFilter
@@ -1387,8 +1370,7 @@ theorem zero_smul_filter_nonpos : (0 : α) • g ≤ 0 := by
 
 theorem zero_smul_filter (hg : g.NeBot) : (0 : α) • g = 0 :=
   zero_smul_filter_nonpos.antisymm <|
-    le_map_iff.2 fun s hs =>
-      by
+    le_map_iff.2 fun s hs => by
       simp_rw [Set.image_eta, zero_smul, (hg.nonempty_of_mem hs).image_const]
       exact zero_mem_zero
 #align filter.zero_smul_filter Filter.zero_smul_filter