[Merged by Bors] - fix(Tactic/ToAdditive): handle AddCommute and AddSemiconjBy correctly

Mathlib/Algebra/Group/Commute/Defs.lean

@@ -30,7 +30,7 @@ Most of the proofs come from the properties of `SemiconjBy`.
 variable {G : Type*}
 
 /-- Two elements commute if `a * b = b * a`. -/
-@[to_additive AddCommute "Two elements additively commute if `a + b = b + a`"]
+@[to_additive "Two elements additively commute if `a + b = b + a`"]
 def Commute {S : Type*} [Mul S] (a b : S) : Prop :=
   SemiconjBy a b b
 #align commute Commute
@@ -67,7 +67,7 @@ protected theorem symm {a b : S} (h : Commute a b) : Commute b a :=
 protected theorem semiconjBy {a b : S} (h : Commute a b) : SemiconjBy a b b :=
   h
 #align commute.semiconj_by Commute.semiconjBy
-#align add_commute.semiconj_by AddCommute.semiconjBy
+#align add_commute.semiconj_by AddCommute.addSemiconjBy
 
 @[to_additive]
 protected theorem symm_iff {a b : S} : Commute a b ↔ Commute b a :=

Mathlib/Algebra/Group/Opposite.lean

@@ -220,16 +220,16 @@ theorem op_div [DivInvMonoid α] (x y : α) : op (x / y) = (op y)⁻¹ * op x :=
 theorem semiconjBy_op [Mul α] {a x y : α} : SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y :=
   by simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]
 #align mul_opposite.semiconj_by_op MulOpposite.semiconjBy_op
-#align add_opposite.semiconj_by_op AddOpposite.semiconjBy_op
+#align add_opposite.semiconj_by_op AddOpposite.addSemiconjBy_op
 
 @[to_additive (attr := simp, nolint simpComm)]
 theorem semiconjBy_unop [Mul α] {a x y : αᵐᵒᵖ} :
     SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y := by
   conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]
 #align mul_opposite.semiconj_by_unop MulOpposite.semiconjBy_unop
-#align add_opposite.semiconj_by_unop AddOpposite.semiconjBy_unop
+#align add_opposite.semiconj_by_unop AddOpposite.addSemiconjBy_unop
 
-attribute [nolint simpComm] AddOpposite.semiconjBy_unop
+attribute [nolint simpComm] AddOpposite.addSemiconjBy_unop
 
 @[to_additive]
 theorem _root_.SemiconjBy.op [Mul α] {a x y : α} (h : SemiconjBy a x y) :
@@ -252,24 +252,25 @@ theorem _root_.Commute.op [Mul α] {x y : α} (h : Commute x y) : Commute (op x)
 #align add_commute.op AddCommute.op
 
 @[to_additive]
-theorem Commute.unop [Mul α] {x y : αᵐᵒᵖ} (h : Commute x y) : Commute (unop x) (unop y) :=
+nonrec theorem _root_.Commute.unop [Mul α] {x y : αᵐᵒᵖ} (h : Commute x y) :
+    Commute (unop x) (unop y) :=
   h.unop
-#align mul_opposite.commute.unop MulOpposite.Commute.unop
-#align add_opposite.commute.unop AddOpposite.Commute.unop
+#align mul_opposite.commute.unop Commute.unop
+#align add_opposite.commute.unop AddCommute.unop
 
 @[to_additive (attr := simp)]
 theorem commute_op [Mul α] {x y : α} : Commute (op x) (op y) ↔ Commute x y :=
   semiconjBy_op
 #align mul_opposite.commute_op MulOpposite.commute_op
-#align add_opposite.commute_op AddOpposite.commute_op
+#align add_opposite.commute_op AddOpposite.addCommute_op
 
 @[to_additive (attr := simp, nolint simpComm)]
 theorem commute_unop [Mul α] {x y : αᵐᵒᵖ} : Commute (unop x) (unop y) ↔ Commute x y :=
   semiconjBy_unop
 #align mul_opposite.commute_unop MulOpposite.commute_unop
-#align add_opposite.commute_unop AddOpposite.commute_unop
+#align add_opposite.commute_unop AddOpposite.addCommute_unop
 
-attribute [nolint simpComm] AddOpposite.commute_unop
+attribute [nolint simpComm] AddOpposite.addCommute_unop
 
 /-- The function `MulOpposite.op` is an additive equivalence. -/
 @[simps! (config := { fullyApplied := false, simpRhs := true }) apply symm_apply]

Mathlib/Algebra/Group/Pi.lean

@@ -563,7 +563,7 @@ theorem Pi.mulSingle_commute [∀ i, MulOneClass <| f i] :
     simp [hij]
   simp [h1, h2]
 #align pi.mul_single_commute Pi.mulSingle_commute
-#align pi.single_commute Pi.single_commute
+#align pi.single_commute Pi.single_addCommute
 
 /-- The injection into a pi group with the same values commutes. -/
 @[to_additive "The injection into an additive pi group with the same values commutes."]
@@ -573,7 +573,7 @@ theorem Pi.mulSingle_apply_commute [∀ i, MulOneClass <| f i] (x : ∀ i, f i)
   · rfl
   · exact Pi.mulSingle_commute hij _ _
 #align pi.mul_single_apply_commute Pi.mulSingle_apply_commute
-#align pi.single_apply_commute Pi.single_apply_commute
+#align pi.single_apply_commute Pi.single_apply_addCommute
 
 @[to_additive]
 theorem Pi.update_eq_div_mul_mulSingle [∀ i, Group <| f i] (g : ∀ i : I, f i) (x : f i) :

Mathlib/Algebra/Group/Semiconj/Defs.lean

@@ -32,7 +32,7 @@ operations (`pow_right`, field inverse etc) are in the files that define corresp
 variable {S M G : Type*}
 
 /-- `x` is semiconjugate to `y` by `a`, if `a * x = y * a`. -/
-@[to_additive AddSemiconjBy "`x` is additive semiconjugate to `y` by `a` if `a + x = y + a`"]
+@[to_additive "`x` is additive semiconjugate to `y` by `a` if `a + x = y + a`"]
 def SemiconjBy [Mul M] (a x y : M) : Prop :=
   a * x = y * a
 #align semiconj_by SemiconjBy
@@ -143,7 +143,7 @@ end Group
 
 end SemiconjBy
 
-@[to_additive (attr := simp) addSemiconjBy_iff_eq]
+@[to_additive (attr := simp)]
 theorem semiconjBy_iff_eq [CancelCommMonoid M] {a x y : M} : SemiconjBy a x y ↔ x = y :=
   ⟨fun h => mul_left_cancel (h.trans (mul_comm _ _)), fun h => by rw [h, SemiconjBy, mul_comm]⟩
 #align semiconj_by_iff_eq semiconjBy_iff_eq

Mathlib/Algebra/Group/Semiconj/Units.lean

@@ -123,7 +123,7 @@ end Group
 end SemiconjBy
 
 /-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/
-@[to_additive AddUnits.mk_addSemiconjBy "`a` semiconjugates `x` to `a + x + -a`."]
+@[to_additive "`a` semiconjugates `x` to `a + x + -a`."]
 theorem Units.mk_semiconjBy [Monoid M] (u : Mˣ) (x : M) : SemiconjBy (↑u) x (u * x * ↑u⁻¹) := by
   unfold SemiconjBy; rw [Units.inv_mul_cancel_right]
 #align units.mk_semiconj_by Units.mk_semiconjBy

Mathlib/Data/Finset/NoncommProd.lean

@@ -217,7 +217,7 @@ theorem noncommProd_eq_prod {α : Type*} [CommMonoid α] (s : Multiset α) :
 #align multiset.noncomm_prod_eq_prod Multiset.noncommProd_eq_prod
 #align multiset.noncomm_sum_eq_sum Multiset.noncommSum_eq_sum
 
-@[to_additive noncommSum_addCommute]
+@[to_additive]
 theorem noncommProd_commute (s : Multiset α) (comm) (y : α) (h : ∀ x ∈ s, Commute y x) :
     Commute y (s.noncommProd comm) := by
   induction s using Quotient.inductionOn
@@ -366,7 +366,7 @@ theorem noncommProd_eq_pow_card (s : Finset α) (f : α → β) (comm) (m : β)
 #align finset.noncomm_prod_eq_pow_card Finset.noncommProd_eq_pow_card
 #align finset.noncomm_sum_eq_card_nsmul Finset.noncommSum_eq_card_nsmul
 
-@[to_additive noncommSum_addCommute]
+@[to_additive]
 theorem noncommProd_commute (s : Finset α) (f : α → β) (comm) (y : β)
     (h : ∀ x ∈ s, Commute y (f x)) : Commute y (s.noncommProd f comm) := by
   apply Multiset.noncommProd_commute

Mathlib/GroupTheory/NoncommPiCoprod.lean

@@ -294,7 +294,7 @@ theorem commute_subtype_of_commute (i j : ι) (hne : i ≠ j) :
   rintro ⟨x, hx⟩ ⟨y, hy⟩
   exact hcomm i j hne x y hx hy
 #align subgroup.commute_subtype_of_commute Subgroup.commute_subtype_of_commute
-#align add_subgroup.commute_subtype_of_commute AddSubgroup.commute_subtype_of_commute
+#align add_subgroup.commute_subtype_of_commute AddSubgroup.addCommute_subtype_of_addCommute
 
 /-- The canonical homomorphism from a family of subgroups where elements from different subgroups
 commute -/

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -3717,7 +3717,7 @@ theorem commute_of_normal_of_disjoint (H₁ H₂ : Subgroup G) (hH₁ : H₁.Nor
     apply H₂.mul_mem _ (H₂.inv_mem hy)
     apply hH₂.conj_mem _ hy
 #align subgroup.commute_of_normal_of_disjoint Subgroup.commute_of_normal_of_disjoint
-#align add_subgroup.commute_of_normal_of_disjoint AddSubgroup.commute_of_normal_of_disjoint
+#align add_subgroup.commute_of_normal_of_disjoint AddSubgroup.addCommute_of_normal_of_disjoint
 
 end SubgroupNormal
 

Mathlib/Tactic/ToAdditive.lean

@@ -734,6 +734,8 @@ def nameDict : String → List String
   | "units"       => ["add", "Units"]
   | "cyclic"      => ["add", "Cyclic"]
   | "rootable"    => ["divisible"]
+  | "commute"     => ["add", "Commute"]
+  | "semiconj"    => ["add", "Semiconj"]
   | x             => [x]
 
 /--
@@ -808,6 +810,10 @@ def fixAbbreviation : List String → List String
   | "Is"::"Of"::"Fin"::"Order"::s     => "IsOfFinAddOrder" :: fixAbbreviation s
   | "is" :: "Central" :: "Scalar" :: s  => "isCentralVAdd" :: fixAbbreviation s
   | "Is" :: "Central" :: "Scalar" :: s  => "IsCentralVAdd" :: fixAbbreviation s
+  | "function" :: "_" :: "add" :: "Semiconj" :: s
+                                      => "function" :: "_" :: "semiconj" :: fixAbbreviation s
+  | "function" :: "_" :: "add" :: "Commute" :: s
+                                      => "function" :: "_" :: "commute" :: fixAbbreviation s
   | x :: s                            => x :: fixAbbreviation s
   | []                                => []