chore: tidy various files (#1145)

Mathlib/Algebra/Associated.lean

@@ -221,7 +221,7 @@ theorem of_irreducible_pow {α} [Monoid α] {x : α} {n : ℕ} (hn : n ≠ 1) :
   intro h
   obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hn
   rw [pow_succ, add_comm] at h
-  exact (or_iff_left_of_imp is_unit_pow_succ_iff.mp).mp (of_irreducible_mul h)
+  exact (or_iff_left_of_imp isUnit_pow_succ_iff.mp).mp (of_irreducible_mul h)
 #align of_irreducible_pow of_irreducible_pow
 
 theorem irreducible_or_factor {α} [Monoid α] (x : α) (h : ¬IsUnit x) :

Mathlib/Algebra/Group/Defs.lean

@@ -903,13 +903,13 @@ class SubtractionCommMonoid (G : Type u) extends SubtractionMonoid G, AddCommMon
 
 /-- Commutative `DivisionMonoid`.
 
-This is the immediate common ancestor of `comm_group` and `CommGroupWithZero`. -/
+This is the immediate common ancestor of `CommGroup` and `CommGroupWithZero`. -/
 @[to_additive SubtractionCommMonoid]
 class DivisionCommMonoid (G : Type u) extends DivisionMonoid G, CommMonoid G
 
 attribute [to_additive] DivisionCommMonoid.toCommMonoid
 
-/-- A `group` is a `monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.
+/-- A `Group` is a `Monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.
 
 There is also a division operation `/` such that `a / b = a * b⁻¹`,
 with a default so that `a / b = a * b⁻¹` holds by definition.

Mathlib/Algebra/Parity.lean

@@ -18,8 +18,8 @@ This file proves some general facts about squares, even and odd elements of semi
 In the implementation, we define `IsSquare` and we let `Even` be the notion transported by
 `to_additive`.  The definition are therefore as follows:
 ```lean
-is_square a ↔ ∃ r, a = r * r
-even a ↔ ∃ r, a = r + r
+IsSquare a ↔ ∃ r, a = r * r
+Even a ↔ ∃ r, a = r + r
 ```
 
 Odd elements are not unified with a multiplicative notion.
@@ -47,8 +47,8 @@ variable [Mul α]
 /-- An element `a` of a type `α` with multiplication satisfies `IsSquare a` if `a = r * r`,
 for some `r : α`. -/
 @[to_additive Even
-      "An element `a` of a type `α` with addition satisfies
-      `Even a` if `a = r + r`,\nfor some `r : α`."]
+      "An element `a` of a type `α` with addition satisfies `Even a` if `a = r + r`,
+      for some `r : α`."]
 def IsSquare (a : α) : Prop :=
   ∃ r, a = r * r
 #align is_square IsSquare
@@ -214,7 +214,7 @@ theorem Even.isSquare_zpow [Group α] {n : ℤ} : Even n → ∀ a : α, IsSquar
 #align even.is_square_zpow Even.isSquare_zpow
 #align even.zsmul' Even.zsmul'
 
--- `odd.tsub` requires `canonically_linear_ordered_semiring`, which we don't have
+-- `odd.tsub` requires `CanonicallyLinearOrderedSemiring`, which we don't have
 theorem Even.tsub [CanonicallyLinearOrderedAddMonoid α] [Sub α] [OrderedSub α]
     [ContravariantClass α α (· + ·) (· ≤ ·)] {m n : α} (hm : Even m) (hn : Even n) : Even (m - n) :=
   by
@@ -342,12 +342,11 @@ theorem odd_two_mul_add_one (m : α) : Odd (2 * m + 1) :=
 
 theorem Odd.map [RingHomClass F α β] (f : F) : Odd m → Odd (f m) := by
   rintro ⟨m, rfl⟩
-  exact ⟨f m, by
-        simp [two_mul]
-        rw [← Nat.cast_one, map_add, map_add, Nat.cast_one]
-        apply congrArg
-        rw [map_one]
-                ⟩
+  refine ⟨f m, ?_⟩
+  simp [two_mul]
+  rw [← Nat.cast_one, map_add, map_add, Nat.cast_one]
+  apply congrArg
+  rw [map_one]
 #align odd.map Odd.map
 
 @[simp]
@@ -390,7 +389,7 @@ section CanonicallyOrderedCommSemiring
 
 variable [CanonicallyOrderedCommSemiring α]
 
--- this holds more generally in a `canonically_ordered_add_monoid` if we refactor `odd` to use
+-- this holds more generally in a `CanonicallyOrderedAddMonoid` if we refactor `Odd` to use
 -- either `2 • t` or `t + t` instead of `2 * t`.
 theorem Odd.pos [Nontrivial α] {n : α} (hn : Odd n) : 0 < n := by
   obtain ⟨k, rfl⟩ := hn
@@ -507,8 +506,8 @@ theorem pow_bit0_abs (a : R) (p : ℕ) : |a| ^ bit0 p = a ^ bit0 p :=
   (even_bit0 _).pow_abs _
 #align pow_bit0_abs pow_bit0_abs
 
-theorem Odd.strict_mono_pow (hn : Odd n) : StrictMono fun a : R => a ^ n := by
-  cases' hn with k hk ; simpa only [hk, two_mul] using strict_mono_pow_bit1 _
-#align odd.strict_mono_pow Odd.strict_mono_pow
+theorem Odd.strictMono_pow (hn : Odd n) : StrictMono fun a : R => a ^ n := by
+  cases' hn with k hk ; simpa only [hk, two_mul] using strictMono_pow_bit1 _
+#align odd.strict_mono_pow Odd.strictMono_pow
 
 end Powers

Mathlib/CategoryTheory/Functor/FullyFaithful.lean

@@ -323,8 +323,8 @@ protected def Faithful.div (F : C ⥤ E) (G : D ⥤ E) [Faithful G] (obj : C →
       apply G.map_injective
       apply eq_of_heq
       trans F.map (𝟙 X)
-      exact h_map
-      rw [F.map_id, G.map_id, h_obj X]
+      · exact h_map
+      · rw [F.map_id, G.map_id, h_obj X]
     map_comp := by
       intros X Y Z f g
       refine G.map_injective <| eq_of_heq <| h_map.trans ?_

Mathlib/Data/Erased.lean

@@ -72,7 +72,7 @@ theorem mk_out {α} : ∀ a : Erased α, mk (out a) = a
 theorem out_inj {α} (a b : Erased α) (h : a.out = b.out) : a = b := by simpa using congr_arg mk h
 #align erased.out_inj Erased.out_inj
 
-/-- Equivalence between `erased α` and `α`. -/
+/-- Equivalence between `Erased α` and `α`. -/
 noncomputable def equiv (α) : Erased α ≃ α :=
   ⟨out, mk, mk_out, out_mk⟩
 #align erased.equiv Erased.equiv

Mathlib/Dynamics/FixedPoints/Basic.lean

@@ -160,9 +160,9 @@ theorem fixedPoints_subset_range : fixedPoints f ⊆ Set.range f := fun x hx =>
 
 /-- If `g` semiconjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
 of `fb`. -/
-theorem Semiconj.maps_to_fixedPoints {g : α → β} (h : Semiconj g fa fb) :
+theorem Semiconj.mapsTo_fixedPoints {g : α → β} (h : Semiconj g fa fb) :
     Set.MapsTo g (fixedPoints fa) (fixedPoints fb) := fun _ hx => hx.map h
-#align function.semiconj.maps_to_fixed_pts Function.Semiconj.maps_to_fixedPoints
+#align function.semiconj.maps_to_fixed_pts Function.Semiconj.mapsTo_fixedPoints
 
 /-- Any two maps `f : α → β` and `g : β → α` are inverse of each other on the sets of fixed points
 of `f ∘ g` and `g ∘ f`, respectively. -/
@@ -172,15 +172,15 @@ theorem invOn_fixedPoints_comp (f : α → β) (g : β → α) :
 #align function.inv_on_fixed_pts_comp Function.invOn_fixedPoints_comp
 
 /-- Any map `f` sends fixed points of `g ∘ f` to fixed points of `f ∘ g`. -/
-theorem maps_to_fixedPoints_comp (f : α → β) (g : β → α) :
+theorem mapsTo_fixedPoints_comp (f : α → β) (g : β → α) :
     Set.MapsTo f (fixedPoints <| g ∘ f) (fixedPoints <| f ∘ g) := fun _ hx => hx.map fun _ => rfl
-#align function.maps_to_fixed_pts_comp Function.maps_to_fixedPoints_comp
+#align function.maps_to_fixed_pts_comp Function.mapsTo_fixedPoints_comp
 
 /-- Given two maps `f : α → β` and `g : β → α`, `g` is a bijective map between the fixed points
 of `f ∘ g` and the fixed points of `g ∘ f`. The inverse map is `f`, see `invOn_fixedPoints_comp`. -/
 theorem bijOn_fixedPoints_comp (f : α → β) (g : β → α) :
     Set.BijOn g (fixedPoints <| f ∘ g) (fixedPoints <| g ∘ f) :=
-  (invOn_fixedPoints_comp f g).bijOn (maps_to_fixedPoints_comp g f) (maps_to_fixedPoints_comp f g)
+  (invOn_fixedPoints_comp f g).bijOn (mapsTo_fixedPoints_comp g f) (mapsTo_fixedPoints_comp f g)
 #align function.bij_on_fixed_pts_comp Function.bijOn_fixedPoints_comp
 
 /-- If self-maps `f` and `g` commute, then they are inverse of each other on the set of fixed points

Mathlib/GroupTheory/GroupAction/Opposite.lean

@@ -18,7 +18,7 @@ This file defines the actions on the opposite type `SMul R Mᵐᵒᵖ`, and acti
 type, `SMul Rᵐᵒᵖ M`.
 
 Note that `MulOpposite.instSMulMulOpposite` is provided in an earlier file as it is needed to
-provide the `add_monoid.nsmul` and `add_comm_group.gsmul` fields.
+provide the `AddMonoid.nsmul` and `AddCommGroup.zsmul` fields.
 -/
 
 
@@ -85,7 +85,8 @@ open MulOpposite
 /-- Like `Mul.toSMul`, but multiplies on the right.
 
 See also `Monoid.toOppositeMulAction` and `MonoidWithZero.toOppositeMulActionWithZero`. -/
-@[to_additive "Like `Add.toVAdd`, but adds on the right.\n\n
+@[to_additive "Like `Add.toVAdd`, but adds on the right.
+
   See also `AddMonoid.to_OppositeAddAction`."]
 instance Mul.toHasOppositeSmul [Mul α] : SMul αᵐᵒᵖ α :=
   ⟨fun c x => x * c.unop⟩
@@ -106,27 +107,27 @@ theorem MulOpposite.smul_eq_mul_unop [Mul α] {a : αᵐᵒᵖ} {a' : α} : a 
 
 /-- The right regular action of a group on itself is transitive. -/
 @[to_additive "The right regular action of an additive group on itself is transitive."]
-instance MulAction.OppositeRegular.is_pretransitive {G : Type _} [Group G] :
+instance MulAction.OppositeRegular.isPretransitive {G : Type _} [Group G] :
     MulAction.IsPretransitive Gᵐᵒᵖ G :=
   ⟨fun x y => ⟨op (x⁻¹ * y), mul_inv_cancel_left _ _⟩⟩
-#align mul_action.opposite_regular.is_pretransitive MulAction.OppositeRegular.is_pretransitive
-#align add_action.opposite_regular.is_pretransitive AddAction.OppositeRegular.is_pretransitive
+#align mul_action.opposite_regular.is_pretransitive MulAction.OppositeRegular.isPretransitive
+#align add_action.opposite_regular.is_pretransitive AddAction.OppositeRegular.isPretransitive
 
 @[to_additive]
-instance Semigroup.opposite_smul_comm_class [Semigroup α] :
+instance Semigroup.opposite_smulCommClass [Semigroup α] :
     SMulCommClass αᵐᵒᵖ α α where smul_comm _ _ _ := mul_assoc _ _ _
-#align semigroup.opposite_smul_comm_class Semigroup.opposite_smul_comm_class
-#align add_semigroup.opposite_vadd_comm_class AddSemigroup.opposite_vadd_comm_class
+#align semigroup.opposite_smul_comm_class Semigroup.opposite_smulCommClass
+#align add_semigroup.opposite_vadd_comm_class AddSemigroup.opposite_vaddCommClass
 
 @[to_additive]
-instance Semigroup.opposite_smul_comm_class' [Semigroup α] : SMulCommClass α αᵐᵒᵖ α :=
+instance Semigroup.opposite_smulCommClass' [Semigroup α] : SMulCommClass α αᵐᵒᵖ α :=
   SMulCommClass.symm _ _ _
-#align semigroup.opposite_smul_comm_class' Semigroup.opposite_smul_comm_class'
-#align add_semigroup.opposite_vadd_comm_class' AddSemigroup.opposite_vadd_comm_class'
+#align semigroup.opposite_smul_comm_class' Semigroup.opposite_smulCommClass'
+#align add_semigroup.opposite_vadd_comm_class' AddSemigroup.opposite_vaddCommClass'
 
-instance CommSemigroup.is_central_scalar [CommSemigroup α] : IsCentralScalar α α :=
+instance CommSemigroup.isCentralScalar [CommSemigroup α] : IsCentralScalar α α :=
   ⟨fun _ _ => mul_comm _ _⟩
-#align comm_semigroup.is_central_scalar CommSemigroup.is_central_scalar
+#align comm_semigroup.is_central_scalar CommSemigroup.isCentralScalar
 
 /-- Like `Monoid.toMulAction`, but multiplies on the right. -/
 @[to_additive "Like `AddMonoid.toAddAction`, but adds on the right."]
@@ -158,15 +159,17 @@ example [Monoid α] : Monoid.toMulAction αᵐᵒᵖ = MulOpposite.instMulAction
 
 /-- `Monoid.toOppositeMulAction` is faithful on cancellative monoids. -/
 @[to_additive "`AddMonoid.toOppositeAddAction` is faithful on cancellative monoids."]
-instance LeftCancelMonoid.to_has_faithful_opposite_scalar [LeftCancelMonoid α] :
+instance LeftCancelMonoid.toFaithfulSMul_opposite [LeftCancelMonoid α] :
     FaithfulSMul αᵐᵒᵖ α :=
   ⟨fun h => unop_injective <| mul_left_cancel (h 1)⟩
 #align left_cancel_monoid.to_has_faithful_opposite_scalar
-  LeftCancelMonoid.to_has_faithful_opposite_scalar
+  LeftCancelMonoid.toFaithfulSMul_opposite
+#align add_left_cancel_monoid.to_has_faithful_opposite_scalar
+  AddLeftCancelMonoid.toFaithfulVAdd_opposite
 
 /-- `Monoid.toOppositeMulAction` is faithful on nontrivial cancellative monoids with zero. -/
-instance CancelMonoidWithZero.to_has_faithful_opposite_scalar [CancelMonoidWithZero α]
+instance CancelMonoidWithZero.toFaithfulSMul_opposite [CancelMonoidWithZero α]
     [Nontrivial α] : FaithfulSMul αᵐᵒᵖ α :=
   ⟨fun h => unop_injective <| mul_left_cancel₀ one_ne_zero (h 1)⟩
 #align cancel_monoid_with_zero.to_has_faithful_opposite_scalar
-  CancelMonoidWithZero.to_has_faithful_opposite_scalar
+  CancelMonoidWithZero.toFaithfulSMul_opposite

Mathlib/GroupTheory/GroupAction/Pi.lean

@@ -209,9 +209,7 @@ instance mulDistribMulAction (α) {m : Monoid α} {n : ∀ i, Monoid <| f i}
 
 instance mulDistribMulAction' {g : I → Type _} {m : ∀ i, Monoid (f i)} {n : ∀ i, Monoid <| g i}
     [∀ i, MulDistribMulAction (f i) (g i)] :
-    @MulDistribMulAction (∀ i, f i) (∀ i : I, g i) (@Pi.monoid I f m)
-      (@Pi.monoid I g
-        n) where
+    @MulDistribMulAction (∀ i, f i) (∀ i : I, g i) (@Pi.monoid I f m) (@Pi.monoid I g n) where
   smul_mul := by
     intros
     ext x