fix(group_theory/*, algebra/group): [to_additive, simp] doesn't work (#…

…5468)

As explained in `algebra/group/to_additive`, `@[to_additive, simp]` doesn't work (it doesn't attach a `simp` attribute to the additive lemma), but conversely `@[simps, to_additive]` is also wrong.

Along the way I also noticed that some `right_inv` (as in an inverse function) lemmas were being changed to `right_neg` by to_additive :D

src/algebra/category/Group/basic.lean

@@ -60,10 +60,11 @@ instance one.unique : unique (1 : Group) :=
 @[simp, to_additive]
 lemma one_apply (G H : Group) (g : G) : (1 : G ⟶ H) g = 1 := rfl
 
-@[to_additive, ext]
+@[ext, to_additive]
 lemma ext (G H : Group) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
 by { ext1, apply w }
 
+-- should to_additive do this automatically?
 attribute [ext] AddGroup.ext
 
 @[to_additive has_forget_to_AddMon]

src/algebra/group/hom.lean

@@ -668,8 +668,8 @@ def eval [monoid M] [comm_monoid N] : M →* (M →* N) →* N := (monoid_hom.id
 lemma eval_apply [monoid M] [comm_monoid N] (x : M) (f : M →* N) : eval x f = f x := rfl
 
 /-- Composition of monoid morphisms (`monoid_hom.comp`) as a monoid morphism. -/
-@[simps, to_additive "Composition of additive monoid morphisms
-(`add_monoid_hom.comp`) as an additive monoid morphism."]
+@[to_additive "Composition of additive monoid morphisms
+(`add_monoid_hom.comp`) as an additive monoid morphism.", simps]
 def comp_hom [monoid M] [comm_monoid N] [comm_monoid P] :
   (N →* P) →* (M →* N) →* (M →* P) :=
 { to_fun := λ g, { to_fun := g.comp, map_one' := comp_one g, map_mul' := comp_mul g },

src/algebra/group/semiconj.lean

@@ -45,7 +45,7 @@ variables {S : Type u} [semigroup S] {a b x y z x' y' : S}
 
 /-- If `a` semiconjugates `x` to `y` and `x'` to `y'`,
 then it semiconjugates `x * x'` to `y * y'`. -/
-@[to_additive, simp] lemma mul_right (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
+@[simp, to_additive] lemma mul_right (h : semiconj_by a x y) (h' : semiconj_by a x' y') :
   semiconj_by a (x * x') (y * y') :=
 by unfold semiconj_by; assoc_rw [h.eq, h'.eq]
 

src/algebra/ordered_monoid.lean

@@ -208,14 +208,19 @@ namespace units
 instance [monoid α] [preorder α] : preorder (units α) :=
 preorder.lift (coe : units α → α)
 
-@[simp, to_additive, norm_cast]
+@[simp, norm_cast, to_additive]
 theorem coe_le_coe [monoid α] [preorder α] {a b : units α} :
   (a : α) ≤ b ↔ a ≤ b := iff.rfl
 
-@[simp, to_additive, norm_cast]
+-- should `to_additive` do this?
+attribute [norm_cast] add_units.coe_le_coe
+
+@[simp, norm_cast, to_additive]
 theorem coe_lt_coe [monoid α] [preorder α] {a b : units α} :
   (a : α) < b ↔ a < b := iff.rfl
 
+attribute [norm_cast] add_units.coe_lt_coe
+
 @[to_additive]
 instance [monoid α] [partial_order α] : partial_order (units α) :=
 partial_order.lift coe units.ext
@@ -224,16 +229,20 @@ partial_order.lift coe units.ext
 instance [monoid α] [linear_order α] : linear_order (units α) :=
 linear_order.lift coe units.ext
 
-@[simp, to_additive, norm_cast]
+@[simp, norm_cast, to_additive]
 theorem max_coe [monoid α] [linear_order α] {a b : units α} :
   (↑(max a b) : α) = max a b :=
 by by_cases b ≤ a; simp [max, h]
 
-@[simp, to_additive, norm_cast]
+attribute [norm_cast] add_units.max_coe
+
+@[simp, norm_cast, to_additive]
 theorem min_coe [monoid α] [linear_order α] {a b : units α} :
   (↑(min a b) : α) = min a b :=
 by by_cases a ≤ b; simp [min, h]
 
+attribute [norm_cast] add_units.min_coe
+
 end units
 
 namespace with_zero

src/group_theory/monoid_localization.lean

@@ -850,11 +850,11 @@ noncomputable def mul_equiv_of_localizations
 ⟨f.lift k.map_units, k.lift f.map_units, f.lift_left_inverse,
   k.lift_left_inverse, monoid_hom.map_mul _⟩
 
-@[to_additive, simp] lemma mul_equiv_of_localizations_apply
+@[simp, to_additive] lemma mul_equiv_of_localizations_apply
   {k : localization_map S P} {x} :
   f.mul_equiv_of_localizations k x = f.lift k.map_units x := rfl
 
-@[to_additive, simp] lemma mul_equiv_of_localizations_symm_apply
+@[simp, to_additive] lemma mul_equiv_of_localizations_symm_apply
   {k : localization_map S P} {x} :
   (f.mul_equiv_of_localizations k).symm x = k.lift f.map_units x := rfl
 
@@ -872,7 +872,7 @@ def of_mul_equiv_of_localizations (k : N ≃* P) : localization_map S P :=
   let ⟨x, hx⟩ := f.surj z in ⟨x, show v * k _ = k _, by rw [←hx, k.map_mul, ←hz]; refl⟩)
 (λ x y, k.apply_eq_iff_eq.trans f.eq_iff_exists)
 
-@[to_additive, simp] lemma of_mul_equiv_of_localizations_apply {k : N ≃* P} (x) :
+@[simp, to_additive] lemma of_mul_equiv_of_localizations_apply {k : N ≃* P} (x) :
   (f.of_mul_equiv_of_localizations k).to_map x = k (f.to_map x) := rfl
 
 @[to_additive] lemma of_mul_equiv_of_localizations_eq {k : N ≃* P} :
@@ -890,11 +890,13 @@ k.apply_symm_apply (f.to_map x)
   (f.of_mul_equiv_of_localizations k).to_map x = y ↔ f.to_map x = k.symm y :=
 k.to_equiv.eq_symm_apply.symm
 
-@[to_additive] lemma mul_equiv_of_localizations_right_inv (k : localization_map S P) :
+@[to_additive add_equiv_of_localizations_right_inv]
+lemma mul_equiv_of_localizations_right_inv (k : localization_map S P) :
   f.of_mul_equiv_of_localizations (f.mul_equiv_of_localizations k) = k :=
 to_map_injective $ f.lift_comp k.map_units
 
-@[to_additive, simp] lemma mul_equiv_of_localizations_right_inv_apply
+@[to_additive add_equiv_of_localizations_right_inv_apply, simp]
+lemma mul_equiv_of_localizations_right_inv_apply
   {k : localization_map S P} {x} :
   (f.of_mul_equiv_of_localizations (f.mul_equiv_of_localizations k)).to_map x = k.to_map x :=
 ext_iff.1 (f.mul_equiv_of_localizations_right_inv k) x
@@ -903,7 +905,7 @@ ext_iff.1 (f.mul_equiv_of_localizations_right_inv k) x
   f.mul_equiv_of_localizations (f.of_mul_equiv_of_localizations k) = k :=
 mul_equiv.ext $ monoid_hom.ext_iff.1 $ f.lift_of_comp k.to_monoid_hom
 
-@[to_additive, simp] lemma mul_equiv_of_localizations_left_inv_apply {k : N ≃* P} (x) :
+@[simp, to_additive] lemma mul_equiv_of_localizations_left_inv_apply {k : N ≃* P} (x) :
   f.mul_equiv_of_localizations (f.of_mul_equiv_of_localizations k) x = k x :=
 by rw mul_equiv_of_localizations_left_inv
 
@@ -937,7 +939,7 @@ let H' : S.comap k.to_monoid_hom = T :=
       exact k.to_equiv.injective hc⟩, λ ⟨c, hc⟩, ⟨⟨k c, H ▸ set.mem_image_of_mem k c.2⟩,
     by erw ←k.map_mul; rw [hc, k.map_mul]; refl⟩⟩)
 
-@[to_additive, simp] lemma of_mul_equiv_of_dom_apply
+@[simp, to_additive] lemma of_mul_equiv_of_dom_apply
   {k : P ≃* M} (H : T.map k.to_monoid_hom = S) (x) :
   (f.of_mul_equiv_of_dom H).to_map x = f.to_map (k x) := rfl
 
@@ -993,7 +995,7 @@ f.map_eq (λ y : S, H ▸ set.mem_image_of_mem j y.2) _
   f.mul_equiv_of_mul_equiv k H (f.mk' x y) = k.mk' (j x) ⟨j y, H ▸ set.mem_image_of_mem j y.2⟩ :=
 f.map_mk' (λ y : S, H ▸ set.mem_image_of_mem j y.2) _ _
 
-@[to_additive, simp] lemma of_mul_equiv_of_mul_equiv_apply
+@[simp, to_additive] lemma of_mul_equiv_of_mul_equiv_apply
   {k : localization_map T Q} {j : M ≃* P} (H : S.map j.to_monoid_hom = T) (x) :
   (f.of_mul_equiv_of_localizations (f.mul_equiv_of_mul_equiv k H)).to_map x = k.to_map (j x) :=
 ext_iff.1 (f.mul_equiv_of_localizations_right_inv (k.of_mul_equiv_of_dom H)) x

src/group_theory/submonoid/operations.lean

@@ -129,7 +129,7 @@ lemma comap_comap (S : submonoid P) (g : N →* P) (f : M →* N) :
   (S.comap g).comap f = S.comap (g.comp f) :=
 rfl
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma comap_id (S : submonoid P) : S.comap (monoid_hom.id _) = S :=
 ext (by simp)
 

src/topology/algebra/monoid.lean

@@ -42,12 +42,13 @@ variables [topological_space M] [has_mul M] [has_continuous_mul M]
 lemma continuous_mul : continuous (λp:M×M, p.1 * p.2) :=
 has_continuous_mul.continuous_mul
 
-@[to_additive, continuity]
+@[continuity, to_additive]
 lemma continuous.mul [topological_space α] {f : α → M} {g : α → M}
   (hf : continuous f) (hg : continuous g) :
   continuous (λx, f x * g x) :=
 continuous_mul.comp (hf.prod_mk hg : _)
 
+-- should `to_additive` be doing this?
 attribute [continuity] continuous.add
 
 @[to_additive]
@@ -101,7 +102,7 @@ instance [topological_space N] [has_mul N] [has_continuous_mul N] : has_continuo
 ⟨((continuous_fst.comp continuous_fst).mul (continuous_fst.comp continuous_snd)).prod_mk
  ((continuous_snd.comp continuous_fst).mul (continuous_snd.comp continuous_snd))⟩
 
-@[to_additive, priority 100]
+@[priority 100, to_additive]
 instance has_continuous_mul_of_discrete_topology [topological_space N]
   [has_mul N] [discrete_topology N] : has_continuous_mul N :=
 ⟨continuous_of_discrete_topology⟩
@@ -247,11 +248,12 @@ by { rcases s with ⟨l⟩, simp, exact continuous_list_prod l }
 
 attribute [continuity] continuous_multiset_sum
 
-@[to_additive, continuity]
+@[continuity, to_additive]
 lemma continuous_finset_prod [topological_space α] {f : β → α → M} (s : finset β) :
   (∀c∈s, continuous (f c)) → continuous (λa, ∏ c in s, f c a) :=
 continuous_multiset_prod _
 
+-- should `to_additive` be doing this?
 attribute [continuity] continuous_finset_sum
 
 end