feat(tactic/to_additive): Improvements to to_additive (#5487)

Change a couple of things in to_additive:
- First add a `tactic.copy_attribute'` intended for user attributes with parameters very similar to `tactic.copy_attribute` that just copies the parameter over when setting the attribute. This allows to_additive after many other attributes to transfer those attributes properly (e.g. norm_cast)
- Have to additive register generated equation lemmas as such, this necessitates a bit of restructuring, first all declarations must be generated (including equational lemmas), then the equational lemmas need their attributes, then they are registered as equation lemmas, finally the attributes are added to the main declaration.
- I also fixup the library in many places to account for these changes simplifying the source files, only one new lemma was added, in src/analysis/normed/group/quotient.lean `quotient_norm_mk_le'` to replace the unprimed version in the proof of `norm_normed_mk_le` as simp got better thanks to the new simp lemmas introduced by this PR. Probably many more handwritten additive versions can now be deleted in a future PR, especially defs and instances.
- All other library changes are just simplifications by using to additive for some hand generated declarations, and many more attributes on the generated lemmas.
- The attribute mono is trickier as it contains for its parameter not actual exprs containing names but exprs making names from strings, so I don't see how to handle it right now. We now warn the user about this, and fix the library in a couple of places.

Author: alexjbest

src/algebra/big_operators/order.lean

@@ -443,10 +443,12 @@ namespace fintype
 
 variables [fintype ι]
 
-@[mono, to_additive sum_mono]
+@[to_additive sum_mono, mono]
 lemma prod_mono' [ordered_comm_monoid M] : monotone (λ f : ι → M, ∏ i, f i) :=
 λ f g hfg, finset.prod_le_prod'' $ λ x _, hfg x
 
+attribute [mono] sum_mono
+
 @[to_additive sum_strict_mono]
 lemma prod_strict_mono' [ordered_cancel_comm_monoid M] : strict_mono (λ f : ι → M, ∏ x, f x) :=
 λ f g hfg, let ⟨hle, i, hlt⟩ := pi.lt_def.mp hfg in

src/algebra/category/Group/basic.lean

@@ -71,9 +71,6 @@ lemma one_apply (G H : Group) (g : G) : (1 : G ⟶ H) g = 1 := rfl
 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]
 instance has_forget_to_Mon : has_forget₂ Group Mon := bundled_hom.forget₂ _ _
 
@@ -128,12 +125,10 @@ instance one.unique : unique (1 : CommGroup) :=
 @[simp, to_additive]
 lemma one_apply (G H : CommGroup) (g : G) : (1 : G ⟶ H) g = 1 := rfl
 
-@[to_additive,ext]
+@[ext, to_additive]
 lemma ext (G H : CommGroup) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
 by { ext1, apply w }
 
-attribute [ext] AddCommGroup.ext
-
 @[to_additive has_forget_to_AddGroup]
 instance has_forget_to_Group : has_forget₂ CommGroup Group := bundled_hom.forget₂ _ _
 

src/algebra/category/Mon/filtered_colimits.lean

@@ -199,7 +199,7 @@ def cocone_morphism (j : J) : F.obj j ⟶ colimit :=
     rw [F.map_id, id_apply, id_apply], refl,
   end }
 
-@[to_additive, simp]
+@[simp, to_additive]
 lemma cocone_naturality {j j' : J} (f : j ⟶ j') :
   F.map f ≫ (cocone_morphism j') = cocone_morphism j :=
 monoid_hom.coe_inj ((types.colimit_cocone (F ⋙ forget Mon)).ι.naturality f)

src/algebra/free.lean

@@ -55,12 +55,12 @@ attribute [pattern] has_mul.mul
 theorem mul_eq (x y : free_magma α) : mul x y = x * y := rfl
 
 /-- Recursor for `free_magma` using `x * y` instead of `free_magma.mul x y`. -/
-@[to_additive "Recursor for `free_add_magma` using `x + y` instead of `free_add_magma.add x y`."]
+@[elab_as_eliminator, to_additive
+  "Recursor for `free_add_magma` using `x + y` instead of `free_add_magma.add x y`."]
 def rec_on' {C : free_magma α → Sort l} (x)
   (ih1 : ∀ x, C (of x)) (ih2 : ∀ x y, C x → C y → C (x * y)) :
   C x :=
 free_magma.rec_on x ih1 ih2
-attribute [elab_as_eliminator] rec_on' free_add_magma.rec_on'
 
 end free_magma
 

src/algebra/free_monoid.lean

@@ -57,21 +57,17 @@ lemma of_injective : function.injective (@of α) :=
 λ a b, list.head_eq_of_cons_eq
 
 /-- Recursor for `free_monoid` using `1` and `of x * xs` instead of `[]` and `x :: xs`. -/
-@[to_additive
+@[elab_as_eliminator, to_additive
   "Recursor for `free_add_monoid` using `0` and `of x + xs` instead of `[]` and `x :: xs`."]
 def rec_on {C : free_monoid α → Sort*} (xs : free_monoid α) (h0 : C 1)
   (ih : Π x xs, C xs → C (of x * xs)) : C xs := list.rec_on xs h0 ih
 
-attribute [elab_as_eliminator] rec_on free_add_monoid.rec_on
-
-@[to_additive]
+@[ext, to_additive]
 lemma hom_eq ⦃f g : free_monoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) :
   f = g :=
 monoid_hom.ext $ λ l, rec_on l (f.map_one.trans g.map_one.symm) $
   λ x xs hxs, by simp only [h, hxs, monoid_hom.map_mul]
 
-attribute [ext] hom_eq free_add_monoid.hom_eq
-
 /-- Equivalence between maps `α → M` and monoid homomorphisms `free_monoid α →* M`. -/
 @[to_additive "Equivalence between maps `α → A` and additive monoid homomorphisms
 `free_add_monoid α →+ A`."]

src/algebra/group/basic.lean

@@ -94,7 +94,6 @@ variables {G : Type u} [comm_semigroup G]
 @[no_rsimp, to_additive]
 lemma mul_left_comm : ∀ a b c : G, a * (b * c) = b * (a * c) :=
 left_comm has_mul.mul mul_comm mul_assoc
-attribute [no_rsimp] add_left_comm
 
 @[to_additive]
 lemma mul_right_comm : ∀ a b c : G, a * b * c = a * c * b :=

src/algebra/group/defs.lean

@@ -76,8 +76,6 @@ variables {G : Type u} [semigroup G]
 lemma mul_assoc : ∀ a b c : G, a * b * c = a * (b * c) :=
 semigroup.mul_assoc
 
-attribute [no_rsimp] add_assoc -- TODO(Mario): find out why this isn't copying
-
 @[to_additive]
 instance semigroup.to_is_associative : is_associative G (*) :=
 ⟨mul_assoc⟩
@@ -101,7 +99,6 @@ variables {G : Type u} [comm_semigroup G]
 @[no_rsimp, to_additive]
 lemma mul_comm : ∀ a b : G, a * b = b * a :=
 comm_semigroup.mul_comm
-attribute [no_rsimp] add_comm
 
 @[to_additive]
 instance comm_semigroup.to_is_commutative : is_commutative G (*) :=
@@ -206,8 +203,6 @@ begin
   exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂),
 end
 
-attribute [ext] add_zero_class.ext
-
 section mul_one_class
 variables {M : Type u} [mul_one_class M]
 
@@ -219,8 +214,6 @@ mul_one_class.one_mul
 lemma mul_one : ∀ a : M, a * 1 = a :=
 mul_one_class.mul_one
 
-attribute [ematch] add_zero zero_add -- TODO(Mario): Make to_additive transfer this
-
 @[to_additive]
 instance mul_one_class.to_is_left_id : is_left_id M (*) 1 :=
 ⟨ mul_one_class.one_mul ⟩
@@ -382,8 +375,6 @@ begin
   subst h_npow,
 end
 
-attribute [ext] add_monoid.ext
-
 section monoid
 variables {M : Type u} [monoid M]
 
@@ -432,8 +423,6 @@ end
 lemma comm_monoid.ext {M : Type*} ⦃m₁ m₂ : comm_monoid M⦄ (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
 comm_monoid.to_monoid_injective $ monoid.ext h_mul
 
-attribute [ext] add_comm_monoid.ext
-
 section left_cancel_monoid
 
 /-- An additive monoid in which addition is left-cancellative.
@@ -459,8 +448,6 @@ lemma left_cancel_monoid.ext {M : Type*} ⦃m₁ m₂ : left_cancel_monoid M⦄
   (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
 left_cancel_monoid.to_monoid_injective $ monoid.ext h_mul
 
-attribute [ext] add_left_cancel_monoid.ext
-
 end left_cancel_monoid
 
 section right_cancel_monoid
@@ -488,8 +475,6 @@ lemma right_cancel_monoid.ext {M : Type*} ⦃m₁ m₂ : right_cancel_monoid M
   (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
 right_cancel_monoid.to_monoid_injective $ monoid.ext h_mul
 
-attribute [ext] add_right_cancel_monoid.ext
-
 end right_cancel_monoid
 
 section cancel_monoid
@@ -518,8 +503,6 @@ lemma cancel_monoid.ext {M : Type*} ⦃m₁ m₂ : cancel_monoid M⦄
   (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
 cancel_monoid.to_left_cancel_monoid_injective $ left_cancel_monoid.ext h_mul
 
-attribute [ext] add_cancel_monoid.ext
-
 /-- Commutative version of add_cancel_monoid. -/
 @[protect_proj, ancestor add_left_cancel_monoid add_comm_monoid]
 class add_cancel_comm_monoid (M : Type u) extends add_left_cancel_monoid M, add_comm_monoid M
@@ -541,8 +524,6 @@ lemma cancel_comm_monoid.ext {M : Type*} ⦃m₁ m₂ : cancel_comm_monoid M⦄
   (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
 cancel_comm_monoid.to_comm_monoid_injective $ comm_monoid.ext h_mul
 
-attribute [ext] add_cancel_comm_monoid.ext
-
 @[priority 100, to_additive] -- see Note [lower instance priority]
 instance cancel_comm_monoid.to_cancel_monoid (M : Type u) [cancel_comm_monoid M] :
   cancel_monoid M :=
@@ -676,8 +657,6 @@ begin
   subst h_gpow,
 end
 
-attribute [ext] sub_neg_monoid.ext
-
 @[to_additive]
 lemma div_eq_mul_inv {G : Type u} [div_inv_monoid G] :
   ∀ a b : G, a / b = a * b⁻¹ :=
@@ -794,8 +773,6 @@ begin
   exact h_inv
 end
 
-attribute [ext] add_group.ext
-
 /-- A commutative group is a group with commutative `(*)`. -/
 @[protect_proj, ancestor group comm_monoid]
 class comm_group (G : Type u) extends group G, comm_monoid G
@@ -821,8 +798,6 @@ lemma comm_group.ext {G : Type*} ⦃g₁ g₂ : comm_group G⦄
   (h_mul : g₁.mul = g₂.mul) : g₁ = g₂ :=
 comm_group.to_group_injective $ group.ext h_mul
 
-attribute [ext] add_comm_group.ext
-
 section comm_group
 
 variables {G : Type u} [comm_group G]

src/algebra/group/hom.lean

@@ -269,8 +269,6 @@ lemma monoid_with_zero_hom.ext [mul_zero_one_class M] [mul_zero_one_class N]
   ⦃f g : monoid_with_zero_hom M N⦄ (h : ∀ x, f x = g x) : f = g :=
 monoid_with_zero_hom.coe_inj (funext h)
 
-attribute [ext] zero_hom.ext add_hom.ext add_monoid_hom.ext
-
 @[to_additive]
 lemma one_hom.ext_iff [has_one M] [has_one N] {f g : one_hom M N} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ h x, h ▸ rfl, λ h, one_hom.ext h⟩

src/algebra/group/to_additive.lean

@@ -509,10 +509,14 @@ protected meta def attr : user_attribute unit value_type :=
     then proceed_fields env src tgt prio
     else do
       transform_decl_with_prefix_dict dict val.replace_all val.trace relevant ignore reorder src tgt
-        [`reducible, `_refl_lemma, `simp, `instance, `refl, `symm, `trans, `elab_as_eliminator,
-         `no_rsimp, `measurability],
+        [`reducible, `_refl_lemma, `simp, `norm_cast, `instance, `refl, `symm, `trans,
+          `elab_as_eliminator, `no_rsimp, `continuity, `ext, `ematch, `measurability, `alias,
+          `_ext_core, `_ext_lemma_core, `nolint],
       mwhen (has_attribute' `simps src)
         (trace "Apply the simps attribute after the to_additive attribute"),
+      mwhen (has_attribute' `mono src)
+        (trace $ "to_additive does not work with mono, apply the mono attribute to both" ++
+          "versions after"),
       match val.doc with
       | some doc := add_doc_string tgt doc
       | none := skip

src/algebra/group/units.lean

@@ -106,10 +106,8 @@ ext hv
 
 variables (a b : units α) {c : units α}
 @[simp, norm_cast, to_additive] lemma coe_mul : (↑(a * b) : α) = a * b := rfl
-attribute [norm_cast] add_units.coe_add
 
 @[simp, norm_cast, to_additive] lemma coe_one : ((1 : units α) : α) = 1 := rfl
-attribute [norm_cast] add_units.coe_zero
 
 @[simp, norm_cast, to_additive] lemma coe_eq_one {a : units α} : (a : α) = 1 ↔ a = 1 :=
 by rw [←units.coe_one, eq_iff]