lint(algebra/*): fix some lint errors (#13058)

* add some docstrings to additive versions;
* make `with_zero.ordered_add_comm_monoid` reducible.

src/algebra/group/semiconj.lean

@@ -70,11 +70,11 @@ section mul_one_class
 variables {M : Type u} [mul_one_class M]
 
 /-- Any element semiconjugates `1` to `1`. -/
-@[simp, to_additive]
+@[simp, to_additive "Any element additively semiconjugates `0` to `0`."]
 lemma one_right (a : M) : semiconj_by a 1 1 := by rw [semiconj_by, mul_one, one_mul]
 
 /-- One semiconjugates any element to itself. -/
-@[simp, to_additive]
+@[simp, to_additive "Zero additively semiconjugates any element to itself."]
 lemma one_left (x : M) : semiconj_by 1 x x := eq.symm $ one_right x
 
 /-- The relation “there exists an element that semiconjugates `a` to `b`” on a monoid (or, more

src/algebra/hom/equiv.lean

@@ -161,8 +161,8 @@ lemma coe_to_equiv {f : M ≃* N} : ⇑(f : M ≃ N) = f := rfl
 @[simp, to_additive]
 lemma coe_to_mul_hom {f : M ≃* N} : ⇑f.to_mul_hom = f := rfl
 
-/-- A multiplicative isomorphism preserves multiplication (canonical form). -/
-@[to_additive]
+/-- A multiplicative isomorphism preserves multiplication. -/
+@[to_additive "An additive isomorphism preserves addition."]
 protected lemma map_mul (f : M ≃* N) : ∀ x y, f (x * y) = f x * f y := map_mul f
 
 /-- Makes a multiplicative isomorphism from a bijection which preserves multiplication. -/
@@ -236,15 +236,15 @@ def trans (h1 : M ≃* N) (h2 : N ≃* P) : (M ≃* P) :=
     by rw [h1.map_mul, h2.map_mul],
   ..h1.to_equiv.trans h2.to_equiv }
 
-/-- e.right_inv in canonical form -/
-@[simp, to_additive]
-lemma apply_symm_apply (e : M ≃* N) : ∀ y, e (e.symm y) = y :=
-e.to_equiv.apply_symm_apply
+/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`. -/
+@[simp, to_additive "`e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`."]
+lemma apply_symm_apply (e : M ≃* N) (y : N) : e (e.symm y) = y :=
+e.to_equiv.apply_symm_apply y
 
-/-- e.left_inv in canonical form -/
-@[simp, to_additive]
-lemma symm_apply_apply (e : M ≃* N) : ∀ x, e.symm (e x) = x :=
-e.to_equiv.symm_apply_apply
+/-- `e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`. -/
+@[simp, to_additive "`e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`."]
+lemma symm_apply_apply (e : M ≃* N) (x : M) : e.symm (e x) = x :=
+e.to_equiv.symm_apply_apply x
 
 @[simp, to_additive]
 theorem symm_comp_self (e : M ≃* N) : e.symm ∘ e = id := funext e.symm_apply_apply
@@ -323,16 +323,20 @@ def mul_equiv_of_unique_of_unique {M N}
   ..equiv_of_unique_of_unique }
 
 /-- There is a unique monoid homomorphism between two monoids with a unique element. -/
-@[to_additive] instance {M N} [unique M] [unique N] [has_mul M] [has_mul N] : unique (M ≃* N) :=
+@[to_additive
+  "There is a unique additive monoid homomorphism between two additive monoids with
+a unique element."]
+instance {M N} [unique M] [unique N] [has_mul M] [has_mul N] : unique (M ≃* N) :=
 { default := mul_equiv_of_unique_of_unique ,
   uniq := λ _, ext $ λ x, subsingleton.elim _ _}
 
 /-!
 ## Monoids
 -/
 
-/-- A multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism). -/
-@[to_additive]
+/-- A multiplicative isomorphism of monoids sends `1` to `1` (and is hence a monoid isomorphism). -/
+@[to_additive "An additive isomorphism of additive monoids sends `0` to `0`
+(and is hence an additive monoid isomorphism)."]
 protected lemma map_one {M N} [mul_one_class M] [mul_one_class N] (h : M ≃* N) : h 1 = 1 :=
 map_one h
 
@@ -451,12 +455,12 @@ def Pi_subsingleton
 -/
 
 /-- A multiplicative equivalence of groups preserves inversion. -/
-@[to_additive]
+@[to_additive "An additive equivalence of additive groups preserves negation."]
 protected lemma map_inv [group G] [group H] (h : G ≃* H) (x : G) : h x⁻¹ = (h x)⁻¹ :=
 map_inv h x
 
 /-- A multiplicative equivalence of groups preserves division. -/
-@[to_additive]
+@[to_additive "An additive equivalence of additive groups preserves subtractions."]
 protected lemma map_div [group G] [group H] (h : G ≃* H) (x y : G) : h (x / y) = h x / h y :=
 map_div h x y
 
@@ -573,8 +577,9 @@ protected def mul_left (a : G) : perm G := (to_units a).mul_left
 @[simp, to_additive]
 lemma coe_mul_left (a : G) : ⇑(equiv.mul_left a) = (*) a := rfl
 
-/-- extra simp lemma that `dsimp` can use. `simp` will never use this. -/
-@[simp, nolint simp_nf, to_additive]
+/-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
+@[simp, nolint simp_nf,
+  to_additive "Extra simp lemma that `dsimp` can use. `simp` will never use this."]
 lemma mul_left_symm_apply (a : G) : ((equiv.mul_left a).symm : G → G) = (*) a⁻¹ := rfl
 
 @[simp, to_additive]
@@ -596,8 +601,9 @@ lemma coe_mul_right (a : G) : ⇑(equiv.mul_right a) = λ x, x * a := rfl
 lemma mul_right_symm (a : G) : (equiv.mul_right a).symm = equiv.mul_right a⁻¹ :=
 ext $ λ x, rfl
 
-/-- extra simp lemma that `dsimp` can use. `simp` will never use this.  -/
-@[simp, nolint simp_nf, to_additive]
+/-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/
+@[simp, nolint simp_nf,
+  to_additive "Extra simp lemma that `dsimp` can use. `simp` will never use this."]
 lemma mul_right_symm_apply (a : G) : ((equiv.mul_right a).symm : G → G) = λ x, x * a⁻¹ := rfl
 
 @[to_additive]

src/algebra/order/monoid.lean

@@ -125,7 +125,7 @@ class linear_ordered_add_comm_monoid_with_top (α : Type*)
 (le_top : ∀ x : α, x ≤ ⊤)
 (top_add' : ∀ x : α, ⊤ + x = ⊤)
 
-@[priority 100]    -- see Note [lower instance priority]
+@[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_add_comm_monoid_with_top.to_order_top (α : Type u)
   [h : linear_ordered_add_comm_monoid_with_top α] : order_top α :=
 { ..h }
@@ -278,8 +278,9 @@ elements are ≤ 1 and then 1 is the top element.
 
 /--
 If `0` is the least element in `α`, then `with_zero α` is an `ordered_add_comm_monoid`.
+See note [reducible non-instances].
 -/
-protected def ordered_add_comm_monoid [ordered_add_comm_monoid α]
+@[reducible] protected def ordered_add_comm_monoid [ordered_add_comm_monoid α]
   (zero_le : ∀ a : α, 0 ≤ a) : ordered_add_comm_monoid (with_zero α) :=
 begin
   suffices, refine

src/topology/metric_space/emetric_space.lean

@@ -399,8 +399,8 @@ theorem subtype.edist_eq {p : α → Prop} (x y : subtype p) : edist x y = edist
 
 namespace mul_opposite
 
-/-- Pseudoemetric space instance on multiplicative opposites of pseudoemetric spaces -/
-@[to_additive]
+/-- Pseudoemetric space instance on the multiplicative opposite of a pseudoemetric space. -/
+@[to_additive "Pseudoemetric space instance on the additive opposite of a pseudoemetric space."]
 instance {α : Type*} [pseudo_emetric_space α] : pseudo_emetric_space αᵐᵒᵖ :=
 pseudo_emetric_space.induced unop ‹_›
 
@@ -925,8 +925,8 @@ def emetric_space.induced {γ β} (f : γ → β) (hf : function.injective f)
 instance {α : Type*} {p : α → Prop} [emetric_space α] : emetric_space (subtype p) :=
 emetric_space.induced coe subtype.coe_injective ‹_›
 
-/-- Emetric space instance on multiplicative opposites of emetric spaces -/
-@[to_additive]
+/-- Emetric space instance on the multiplicative opposite of an emetric space. -/
+@[to_additive "Emetric space instance on the additive opposite of an emetric space."]
 instance {α : Type*} [emetric_space α] : emetric_space αᵐᵒᵖ :=
 emetric_space.induced mul_opposite.unop mul_opposite.unop_injective ‹_›