chore(*): clean up the library using to_additive (#9790)

Since #9138 and #5487 to_additive got a lot better, so a lot of duplication in the library becomes unnecessary and makes maintenence a burden. So we remove a large number of copy-pasted declarations that can now be generated automatically.

src/algebra/big_operators/basic.lean

@@ -810,7 +810,6 @@ lemma prod_range_add_div_prod_range {α : Type*} [comm_group α] (f : ℕ → α
   (∏ k in range (n + m), f k) / (∏ k in range n, f k) = ∏ k in finset.range m, f (n + k) :=
 div_eq_of_eq_mul' (prod_range_add f n m)
 
-
 @[to_additive]
 lemma prod_range_zero (f : ℕ → β) :
   ∏ k in range 0, f k = 1 :=
@@ -939,15 +938,15 @@ begin
   rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁],
 end
 
-@[simp] lemma prod_const (b : β) : (∏ x in s, b) = b ^ s.card :=
+@[simp, to_additive] lemma prod_const (b : β) : (∏ x in s, b) = b ^ s.card :=
 by haveI := classical.dec_eq α; exact
 finset.induction_on s (by simp) (λ a s has ih,
 by rw [prod_insert has, card_insert_of_not_mem has, pow_succ, ih])
 
-lemma pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ k in range n, b
-| 0 := by simp
-| (n+1) := by simp
+@[to_additive]
+lemma pow_eq_prod_const (b : β) : ∀ n, b ^ n = ∏ k in range n, b := by simp
 
+@[to_additive sum_nsmul]
 lemma prod_pow (s : finset α) (n : ℕ) (f : α → β) :
   ∏ x in s, f x ^ n = (∏ x in s, f x) ^ n :=
 by haveI := classical.dec_eq α; exact
@@ -1086,6 +1085,7 @@ begin
   simp [this]
 end
 
+@[to_additive]
 lemma prod_update_of_mem [decidable_eq α] {s : finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) :
   (∏ x in s, function.update f i b x) = b * (∏ x in s \ (singleton i), f x) :=
 by { rw [update_eq_piecewise, prod_piecewise], simp [h] }
@@ -1170,22 +1170,6 @@ lemma prod_add_prod_eq [comm_semiring β] {s : finset α} {i : α} {f g h : α 
 by { classical, simp_rw [prod_eq_mul_prod_diff_singleton hi, ← h1, right_distrib],
      congr' 2; apply prod_congr rfl; simpa }
 
-lemma sum_update_of_mem [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α}
-  (h : i ∈ s) (f : α → β) (b : β) :
-  (∑ x in s, function.update f i b x) = b + (∑ x in s \ (singleton i), f x) :=
-by { rw [update_eq_piecewise, sum_piecewise], simp [h] }
-attribute [to_additive] prod_update_of_mem
-
-lemma sum_nsmul [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) :
-  (∑ x in s, n • (f x)) = n • ((∑ x in s, f x)) :=
-@prod_pow (multiplicative β) _ _ _ _ _
-attribute [to_additive sum_nsmul] prod_pow
-
-@[simp] lemma sum_const [add_comm_monoid β] (b : β) :
-  (∑ x in s, b) = s.card • b :=
-@prod_const (multiplicative β) _ _ _ _
-attribute [to_additive] prod_const
-
 lemma card_eq_sum_ones (s : finset α) : s.card = ∑ _ in s, 1 :=
 by simp
 

src/algebra/group/defs.lean

@@ -384,16 +384,11 @@ by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b]
 
 end monoid
 
+@[to_additive nsmul_one']
 lemma npow_one {M : Type u} [monoid M] (x : M) :
   npow 1 x = x :=
 by simp [monoid.npow_succ', monoid.npow_zero']
 
-lemma nsmul_one' {M : Type u} [add_monoid M] (x : M) :
-  nsmul 1 x = x :=
-by simp [add_monoid.nsmul_succ', add_monoid.nsmul_zero']
-
-attribute [to_additive nsmul_one'] npow_one
-
 @[to_additive nsmul_add']
 lemma npow_add {M : Type u} [monoid M] (m n : ℕ) (x : M) :
   npow (m + n) x = npow m x * npow n x :=

src/algebra/group/hom_instances.lean

@@ -24,6 +24,7 @@ universes uM uN uP uQ
 variables {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ}
 
 /-- `(M →* N)` is a `comm_monoid` if `N` is commutative. -/
+@[to_additive "`(M →+ N)` is an `add_comm_monoid` if `N` is commutative."]
 instance [mul_one_class M] [comm_monoid N] : comm_monoid (M →* N) :=
 { mul := (*),
   mul_assoc := by intros; ext; apply mul_assoc,
@@ -38,24 +39,9 @@ instance [mul_one_class M] [comm_monoid N] : comm_monoid (M →* N) :=
   npow_zero' := λ f, by { ext x, simp },
   npow_succ' := λ n f, by { ext x, simp [pow_succ] } }
 
-/-- `(M →+ N)` is an `add_comm_monoid` if `N` is commutative. -/
-instance [add_zero_class M] [add_comm_monoid N] : add_comm_monoid (M →+ N) :=
-{ add := (+),
-  add_assoc := by intros; ext; apply add_assoc,
-  zero := 0,
-  zero_add := by intros; ext; apply zero_add,
-  add_zero := by intros; ext; apply add_zero,
-  add_comm := by intros; ext; apply add_comm,
-  nsmul := λ n f,
-  { to_fun := λ x, nsmul n (f x),
-    map_zero' := by simp [nsmul_zero],
-    map_add' := λ x y, by simp [nsmul_add] },
-  nsmul_zero' := λ f, by { ext x, simp [zero_nsmul], },
-  nsmul_succ' := λ n f, by { ext x, simp [nat.succ_eq_add_one, add_comm, add_nsmul] } }
-
-attribute [to_additive] monoid_hom.comm_monoid
-
 /-- If `G` is a commutative group, then `M →* G` is a commutative group too. -/
+@[to_additive "If `G` is an additive commutative group, then `M →+ G` is an additive commutative
+group too."]
 instance {M G} [mul_one_class M] [comm_group G] : comm_group (M →* G) :=
 { inv := has_inv.inv,
   div := has_div.div,
@@ -69,22 +55,6 @@ instance {M G} [mul_one_class M] [comm_group G] : comm_group (M →* G) :=
   zpow_neg'  := λ n f, by { ext x, simp },
   ..monoid_hom.comm_monoid }
 
-/-- If `G` is an additive commutative group, then `M →+ G` is an additive commutative group too. -/
-instance {M G} [add_zero_class M] [add_comm_group G] : add_comm_group (M →+ G) :=
-{ neg := has_neg.neg,
-  sub := has_sub.sub,
-  sub_eq_add_neg := by { intros, ext, apply sub_eq_add_neg },
-  add_left_neg := by intros; ext; apply add_left_neg,
-  zsmul := λ n f, { to_fun := λ x, zsmul n (f x),
-    map_zero' := by simp,
-    map_add' := λ x y, by simp [zsmul_add] },
-  zsmul_zero' := λ f, by { ext x, simp },
-  zsmul_succ' := λ n f, by { ext x, simp [zsmul_of_nat, nat.succ_eq_add_one, add_comm, add_nsmul] },
-  zsmul_neg'  := λ n f, by { ext x, simp },
-  ..add_monoid_hom.add_comm_monoid }
-
-attribute [to_additive] monoid_hom.comm_group
-
 instance [add_comm_monoid M] : semiring (add_monoid.End M) :=
 { zero_mul := λ x, add_monoid_hom.ext $ λ i, rfl,
   mul_zero := λ x, add_monoid_hom.ext $ λ i, add_monoid_hom.map_zero _,

src/algebra/group/to_additive.lean

@@ -326,13 +326,23 @@ copied to the additive version, then `to_additive` should come last:
 @[simp, to_additive] lemma mul_one' {G : Type*} [group G] (x : G) : x * 1 = x := mul_one x
 ```
 
+The following attributes are supported and should be applied correctly by `to_additive` to
+the new additivized declaration, if they were present on the original one:
+```
+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
+```
+
 The exception to this rule is the `simps` attribute, which should come after `to_additive`:
 
 ```
 @[to_additive, simps]
 instance {M N} [has_mul M] [has_mul N] : has_mul (M × N) := ⟨λ p q, ⟨p.1 * q.1, p.2 * q.2⟩⟩
 ```
 
+Additionally the `mono` attribute is not handled by `to_additive` and should be applied afterwards
+to both the original and additivized lemma.
+
 ## Implementation notes
 
 The transport process generally works by taking all the names of
@@ -442,8 +452,10 @@ scans its type and value for names starting with `src`, and transports
 them. This includes auxiliary definitions like `src._match_1`,
 `src._proof_1`.
 
-After transporting the “main” declaration, `to_additive` transports
-its equational lemmas.
+In addition to transporting the “main” declaration, `to_additive` transports
+its equational lemmas and tags them as equational lemmas for the new declaration,
+attributes present on the original equational lemmas are also transferred first (notably
+`_refl_lemma`).
 
 ### Structure fields and constructors
 

src/algebra/group/ulift.lean

@@ -59,16 +59,11 @@ by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field
 instance mul_one_class [mul_one_class α] : mul_one_class (ulift α) :=
 by refine_struct { mul := (*), one := (1 : ulift α), .. }; tactic.pi_instance_derive_field
 
+@[to_additive]
 instance monoid [monoid α] : monoid (ulift α) :=
 by refine_struct { one := (1 : ulift α), mul := (*), npow := λ n f, ⟨npow n f.down⟩ };
 tactic.pi_instance_derive_field
 
-instance add_monoid [add_monoid α] : add_monoid (ulift α) :=
-by refine_struct { zero := (0 : ulift α), add := (+), nsmul := λ n f, ⟨nsmul n f.down⟩ };
-tactic.pi_instance_derive_field
-
-attribute [to_additive] ulift.monoid
-
 @[to_additive]
 instance comm_monoid [comm_monoid α] : comm_monoid (ulift α) :=
 by refine_struct { one := (1 : ulift α), mul := (*), npow := λ n f, ⟨npow n f.down⟩ };

src/algebra/group_power/lemmas.lean

@@ -34,7 +34,8 @@ add_monoid_hom.eq_nat_cast
   ⟨λ n, n • (1 : A), zero_nsmul _, λ _ _, add_nsmul _ _ _⟩
   (one_nsmul _)
 
-@[simp, norm_cast] lemma units.coe_pow (u : units M) (n : ℕ) : ((u ^ n : units M) : M) = u ^ n :=
+@[simp, norm_cast, to_additive]
+lemma units.coe_pow (u : units M) (n : ℕ) : ((u ^ n : units M) : M) = u ^ n :=
 (units.coe_hom M).map_pow u n
 
 instance invertible_pow (m : M) [invertible m] (n : ℕ) : invertible (m ^ n) :=
@@ -112,20 +113,20 @@ open nat
 theorem zsmul_one [has_one A] (n : ℤ) : n • (1 : A) = n :=
 by cases n; simp
 
+@[to_additive add_one_zsmul]
 lemma zpow_add_one (a : G) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
 | (of_nat n) := by simp [← int.coe_nat_succ, pow_succ']
 | -[1+0]     := by simp [int.neg_succ_of_nat_eq]
 | -[1+(n+1)] := by rw [int.neg_succ_of_nat_eq, zpow_neg, neg_add, neg_add_cancel_right, zpow_neg,
   ← int.coe_nat_succ, zpow_coe_nat, zpow_coe_nat, pow_succ _ (n + 1), mul_inv_rev,
   inv_mul_cancel_right]
 
-theorem add_one_zsmul : ∀ (a : A) (i : ℤ), (i + 1) • a = i • a + a :=
-@zpow_add_one (multiplicative A) _
-
+@[to_additive zsmul_sub_one]
 lemma zpow_sub_one (a : G) (n : ℤ) : a ^ (n - 1) = a ^ n * a⁻¹ :=
 calc a ^ (n - 1) = a ^ (n - 1) * a * a⁻¹ : (mul_inv_cancel_right _ _).symm
              ... = a^n * a⁻¹             : by rw [← zpow_add_one, sub_add_cancel]
 
+@[to_additive add_zsmul]
 lemma zpow_add (a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n :=
 begin
   induction n using int.induction_on with n ihn n ihn,
@@ -134,64 +135,50 @@ begin
   { rw [zpow_sub_one, ← mul_assoc, ← ihn, ← zpow_sub_one, add_sub_assoc] }
 end
 
+@[to_additive add_zsmul_self]
 lemma mul_self_zpow (b : G) (m : ℤ) : b*b^m = b^(m+1) :=
 by { conv_lhs {congr, rw ← zpow_one b }, rw [← zpow_add, add_comm] }
 
+@[to_additive add_self_zsmul]
 lemma mul_zpow_self (b : G) (m : ℤ) : b^m*b = b^(m+1) :=
 by { conv_lhs {congr, skip, rw ← zpow_one b }, rw [← zpow_add, add_comm] }
 
-theorem add_zsmul : ∀ (a : A) (i j : ℤ), (i + j) • a = i • a + j • a :=
-@zpow_add (multiplicative A) _
-
+@[to_additive sub_zsmul]
 lemma zpow_sub (a : G) (m n : ℤ) : a ^ (m - n) = a ^ m * (a ^ n)⁻¹ :=
 by rw [sub_eq_add_neg, zpow_add, zpow_neg]
 
-lemma sub_zsmul (m n : ℤ) (a : A) : (m - n) • a = m • a - n • a :=
-by simpa only [sub_eq_add_neg] using @zpow_sub (multiplicative A) _ _ _ _
-
+@[to_additive one_add_zsmul]
 theorem zpow_one_add (a : G) (i : ℤ) : a ^ (1 + i) = a * a ^ i :=
 by rw [zpow_add, zpow_one]
 
-theorem one_add_zsmul : ∀ (a : A) (i : ℤ), (1 + i) • a = a + i • a :=
-@zpow_one_add (multiplicative A) _
-
+@[to_additive]
 theorem zpow_mul_comm (a : G) (i j : ℤ) : a ^ i * a ^ j = a ^ j * a ^ i :=
 by rw [← zpow_add, ← zpow_add, add_comm]
 
-theorem zsmul_add_comm : ∀ (a : A) (i j : ℤ), i • a + j • a = j • a + i • a :=
-@zpow_mul_comm (multiplicative A) _
-
+-- note that `mul_zsmul` and `zpow_mul` have the primes swapped since their argument order
+-- and therefore the more "natural" choice of lemma is reversed.
+@[to_additive mul_zsmul']
 theorem zpow_mul (a : G) (m n : ℤ) : a ^ (m * n) = (a ^ m) ^ n :=
 int.induction_on n (by simp) (λ n ihn, by simp [mul_add, zpow_add, ihn])
   (λ n ihn, by simp only [mul_sub, zpow_sub, ihn, mul_one, zpow_one])
 
-theorem zsmul_mul' : ∀ (a : A) (m n : ℤ), (m * n) • a = n • (m • a) :=
-@zpow_mul (multiplicative A) _
-
+@[to_additive mul_zsmul]
 theorem zpow_mul' (a : G) (m n : ℤ) : a ^ (m * n) = (a ^ n) ^ m :=
 by rw [mul_comm, zpow_mul]
 
-theorem mul_zsmul (a : A) (m n : ℤ) : (m * n) • a = m • (n • a) :=
-by rw [mul_comm, zsmul_mul']
-
+@[to_additive bit0_zsmul]
 theorem zpow_bit0 (a : G) (n : ℤ) : a ^ bit0 n = a ^ n * a ^ n := zpow_add _ _ _
 
-theorem bit0_zsmul (a : A) (n : ℤ) : bit0 n • a = n • a + n • a :=
-@zpow_bit0 (multiplicative A) _ _ _
-
+@[to_additive bit1_zsmul]
 theorem zpow_bit1 (a : G) (n : ℤ) : a ^ bit1 n = a ^ n * a ^ n * a :=
 by rw [bit1, zpow_add, zpow_bit0, zpow_one]
 
-theorem bit1_zsmul : ∀ (a : A) (n : ℤ), bit1 n • a = n • a + n • a + a :=
-@zpow_bit1 (multiplicative A) _
-
-@[simp] theorem monoid_hom.map_zpow (f : G →* H) (a : G) (n : ℤ) : f (a ^ n) = f a ^ n :=
+@[simp, to_additive]
+theorem monoid_hom.map_zpow (f : G →* H) (a : G) (n : ℤ) : f (a ^ n) = f a ^ n :=
 by cases n; simp
 
-@[simp] theorem add_monoid_hom.map_zsmul (f : A →+ B) (a : A) (n : ℤ) : f (n • a) = n • f a :=
-f.to_multiplicative.map_zpow a n
-
-@[simp, norm_cast] lemma units.coe_zpow (u : units G) (n : ℤ) : ((u ^ n : units G) : G) = u ^ n :=
+@[simp, norm_cast, to_additive]
+lemma units.coe_zpow (u : units G) (n : ℤ) : ((u ^ n : units G) : G) = u ^ n :=
 (units.coe_hom G).map_zpow u n
 
 end group
@@ -671,6 +658,9 @@ def zmultiples_hom [add_group A] : A ≃ (ℤ →+ A) :=
   left_inv := one_zsmul,
   right_inv := λ f, add_monoid_hom.ext_int $ one_zsmul (f 1) }
 
+attribute [to_additive multiples_hom] powers_hom
+attribute [to_additive zmultiples_hom] zpowers_hom
+
 variables {M G A}
 
 @[simp] lemma powers_hom_apply [monoid M] (x : M) (n : multiplicative ℕ) :
@@ -688,15 +678,25 @@ variables {M G A}
 @[simp] lemma multiples_hom_apply [add_monoid A] (x : A) (n : ℕ) :
   multiples_hom A x n = n • x := rfl
 
+attribute [to_additive multiples_hom_apply] powers_hom_apply
+
 @[simp] lemma multiples_hom_symm_apply [add_monoid A] (f : ℕ →+ A) :
   (multiples_hom A).symm f = f 1 := rfl
 
+attribute [to_additive multiples_hom_symm_apply] powers_hom_symm_apply
+
 @[simp] lemma zmultiples_hom_apply [add_group A] (x : A) (n : ℤ) :
   zmultiples_hom A x n = n • x := rfl
 
+attribute [to_additive zmultiples_hom_apply] zpowers_hom_apply
+
 @[simp] lemma zmultiples_hom_symm_apply [add_group A] (f : ℤ →+ A) :
   (zmultiples_hom A).symm f = f 1 := rfl
 
+attribute [to_additive zmultiples_hom_symm_apply] zpowers_hom_symm_apply
+
+-- TODO use to_additive in the rest of this file
+
 lemma monoid_hom.apply_mnat [monoid M] (f : multiplicative ℕ →* M) (n : multiplicative ℕ) :
   f n = (f (multiplicative.of_add 1)) ^ n.to_add :=
 by rw [← powers_hom_symm_apply, ← powers_hom_apply, equiv.apply_symm_apply]
@@ -799,7 +799,7 @@ end
 
 variables [monoid M] [group G] [ring R]
 
-@[simp] lemma units_zpow_right {a : M} {x y : units M} (h : semiconj_by a x y) :
+@[simp, to_additive] lemma units_zpow_right {a : M} {x y : units M} (h : semiconj_by a x y) :
   ∀ m : ℤ, semiconj_by a (↑(x^m)) (↑(y^m))
 | (n : ℕ) := by simp only [zpow_coe_nat, units.coe_pow, h, pow_right]
 | -[1+n] := by simp only [zpow_neg_succ_of_nat, units.coe_pow, units_inv_right, h, pow_right]
@@ -848,11 +848,11 @@ end
 
 variables [monoid M] [group G] [ring R]
 
-@[simp] lemma units_zpow_right {a : M} {u : units M} (h : commute a u) (m : ℤ) :
+@[simp, to_additive] lemma units_zpow_right {a : M} {u : units M} (h : commute a u) (m : ℤ) :
   commute a (↑(u^m)) :=
 h.units_zpow_right m
 
-@[simp] lemma units_zpow_left {u : units M} {a : M} (h : commute ↑u a) (m : ℤ) :
+@[simp, to_additive] lemma units_zpow_left {u : units M} {a : M} (h : commute ↑u a) (m : ℤ) :
   commute (↑(u^m)) a :=
 (h.symm.units_zpow_right m).symm