chore(*): fix some to_additive orders (#17297)

To additive should come after simp and other attributes where possible
leanprover-community · Nov 1, 2022 · b566cd5 · b566cd5
1 parent fdc3136
commit b566cd5
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean
@@ -412,18 +412,18 @@ def hom_quotient_zpow_of_hom :
 lift _ ((mk' _).comp f) $
   λ g ⟨h, (hg : h ^ n = g)⟩, (eq_one_iff _).mpr ⟨_, by simpa only [← hg, map_zpow]⟩
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma hom_quotient_zpow_of_hom_id :
   hom_quotient_zpow_of_hom (monoid_hom.id A) n = monoid_hom.id _ :=
 monoid_hom_ext _ rfl
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma hom_quotient_zpow_of_hom_comp :
   hom_quotient_zpow_of_hom (f.comp g) n
     = (hom_quotient_zpow_of_hom f n).comp (hom_quotient_zpow_of_hom g n) :=
 monoid_hom_ext _ rfl
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma hom_quotient_zpow_of_hom_comp_of_right_inverse (i : function.right_inverse g f) :
   (hom_quotient_zpow_of_hom f n).comp (hom_quotient_zpow_of_hom g n) = monoid_hom.id _ :=
 monoid_hom_ext _ $ monoid_hom.ext $ λ x, congr_arg coe $ i x
@@ -436,18 +436,18 @@ def equiv_quotient_zpow_of_equiv :
 monoid_hom.to_mul_equiv _ _ (hom_quotient_zpow_of_hom_comp_of_right_inverse e.symm e n e.left_inv)
   (hom_quotient_zpow_of_hom_comp_of_right_inverse e e.symm n e.right_inv)
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma equiv_quotient_zpow_of_equiv_refl :
   mul_equiv.refl (A ⧸ (zpow_group_hom n : A →* A).range)
     = equiv_quotient_zpow_of_equiv (mul_equiv.refl A) n :=
 by { ext x, rw [← quotient.out_eq' x], refl }
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma equiv_quotient_zpow_of_equiv_symm :
   (equiv_quotient_zpow_of_equiv e n).symm = equiv_quotient_zpow_of_equiv e.symm n :=
 rfl
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma equiv_quotient_zpow_of_equiv_trans :
   (equiv_quotient_zpow_of_equiv e n).trans (equiv_quotient_zpow_of_equiv d n)
     = equiv_quotient_zpow_of_equiv (e.trans d) n :=

diff --git a/src/topology/continuous_function/algebra.lean b/src/topology/continuous_function/algebra.lean
@@ -467,7 +467,7 @@ instance [locally_compact_space α] [topological_space R] [has_smul R M]
   exact (continuous_fst.comp continuous_fst).smul h,
 end⟩
 
-@[simp, to_additive, norm_cast]
+@[simp, norm_cast, to_additive]
 lemma coe_smul [has_smul R M] [has_continuous_const_smul R M]
   (c : R) (f : C(α, M)) : ⇑(c • f) = c • f := rfl