chore(*): Put simp attribute before to_additive (#11488)

A few lemmas were tagged in the wrong order. As tags are applied from left to right, `@[to_additive, simp]` only marks the multiplicative lemma as `simp`. The correct order is thus `@[simp, to_additive]`.

src/algebra/group/opposite.lean

@@ -140,11 +140,11 @@ semiconj_by_unop.2 h
 @[to_additive] lemma commute.unop [has_mul α] {x y : αᵐᵒᵖ} (h : commute x y) :
   commute (unop x) (unop y) := h.unop
 
-@[to_additive, simp] lemma commute_op [has_mul α] {x y : α} :
+@[simp, to_additive] lemma commute_op [has_mul α] {x y : α} :
   commute (op x) (op y) ↔ commute x y :=
 semiconj_by_op
 
-@[to_additive, simp] lemma commute_unop [has_mul α] {x y : αᵐᵒᵖ} :
+@[simp, to_additive] lemma commute_unop [has_mul α] {x y : αᵐᵒᵖ} :
   commute (unop x) (unop y) ↔ commute x y :=
 semiconj_by_unop
 

src/algebra/order/lattice_group.lean

@@ -144,10 +144,10 @@ instance has_one_lattice_has_neg_part : has_neg_part (α) := ⟨λ a, a⁻¹ ⊔
 @[to_additive neg_part_def]
 lemma m_neg_part_def (a : α) : a⁻ = a⁻¹ ⊔ 1 := rfl
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma pos_one : (1 : α)⁺ = 1 := sup_idem
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma neg_one : (1 : α)⁻ = 1 := by rw [m_neg_part_def, one_inv, sup_idem]
 
 -- a⁻ = -(a ⊓ 0)
@@ -219,7 +219,7 @@ end
 
 -- Bourbaki A.VI.12  Prop 9 a)
 -- a = a⁺ - a⁻
-@[to_additive, simp]
+@[simp, to_additive]
 lemma pos_div_neg [covariant_class α α (*) (≤)] (a : α) : a⁺ / a⁻ = a :=
 begin
   symmetry,

src/group_theory/submonoid/inverses.lean

@@ -84,11 +84,11 @@ inverse in `S`. This is an `add_monoid_hom` when `M` is commutative."]
 noncomputable
 def from_left_inv : S.left_inv → S := λ x, x.prop.some
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma mul_from_left_inv (x : S.left_inv) : (x : M) * S.from_left_inv x = 1 :=
 x.prop.some_spec
 
-@[to_additive, simp] lemma from_left_inv_one : S.from_left_inv 1 = 1 :=
+@[simp, to_additive] lemma from_left_inv_one : S.from_left_inv 1 = 1 :=
 (one_mul _).symm.trans (subtype.eq $ S.mul_from_left_inv 1)
 
 end monoid
@@ -97,7 +97,7 @@ section comm_monoid
 
 variables [comm_monoid M] (S : submonoid M)
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma from_left_inv_mul (x : S.left_inv) : (S.from_left_inv x : M) * x = 1 :=
 by rw [mul_comm, mul_from_left_inv]
 
@@ -139,10 +139,10 @@ def left_inv_equiv : S.left_inv ≃* S :=
     exact (hS x.prop).some_spec.symm },
   ..S.from_comm_left_inv }
 
-@[to_additive, simp] lemma from_left_inv_left_inv_equiv_symm (x : S) :
+@[simp, to_additive] lemma from_left_inv_left_inv_equiv_symm (x : S) :
   S.from_left_inv ((S.left_inv_equiv hS).symm x) = x := (S.left_inv_equiv hS).right_inv x
 
-@[to_additive, simp] lemma left_inv_equiv_symm_from_left_inv (x : S.left_inv) :
+@[simp, to_additive] lemma left_inv_equiv_symm_from_left_inv (x : S.left_inv) :
   (S.left_inv_equiv hS).symm (S.from_left_inv x) = x := (S.left_inv_equiv hS).left_inv x
 
 @[to_additive]
@@ -151,11 +151,11 @@ lemma left_inv_equiv_mul (x : S.left_inv) : (S.left_inv_equiv hS x : M) * x = 1
 @[to_additive]
 lemma mul_left_inv_equiv (x : S.left_inv) : (x : M) * S.left_inv_equiv hS x = 1 := by simp
 
-@[to_additive, simp] lemma left_inv_equiv_symm_mul (x : S) :
+@[simp, to_additive] lemma left_inv_equiv_symm_mul (x : S) :
   ((S.left_inv_equiv hS).symm x : M) * x = 1 :=
 by { convert S.mul_left_inv_equiv hS ((S.left_inv_equiv hS).symm x), simp }
 
-@[to_additive, simp] lemma mul_left_inv_equiv_symm (x : S) :
+@[simp, to_additive] lemma mul_left_inv_equiv_symm (x : S) :
   (x : M) * (S.left_inv_equiv hS).symm x = 1 :=
 by { convert S.left_inv_equiv_mul hS ((S.left_inv_equiv hS).symm x), simp }
 
@@ -172,7 +172,7 @@ submonoid.ext $ λ x,
   ⟨λ h, submonoid.mem_inv.mpr ((inv_eq_of_mul_eq_one h.some_spec).symm ▸ h.some.prop),
     λ h, ⟨⟨_, h⟩, mul_right_inv _⟩⟩
 
-@[to_additive, simp] lemma from_left_inv_eq_inv (x : S.left_inv) :
+@[simp, to_additive] lemma from_left_inv_eq_inv (x : S.left_inv) :
   (S.from_left_inv x : M) = x⁻¹ :=
 by rw [← mul_right_inj (x : M), mul_right_inv, mul_from_left_inv]
 
@@ -182,7 +182,7 @@ section comm_group
 
 variables [comm_group M] (S : submonoid M) (hS : S ≤ is_unit.submonoid M)
 
-@[to_additive, simp] lemma left_inv_equiv_symm_eq_inv (x : S) :
+@[simp, to_additive] lemma left_inv_equiv_symm_eq_inv (x : S) :
   ((S.left_inv_equiv hS).symm x : M) = x⁻¹ :=
 by rw [← mul_right_inj (x : M), mul_right_inv, mul_left_inv_equiv_symm]