feat(Algebra/Group): Add commute_iff_eq and a few lemmas on conjugati…

…on (#9870)

This introduces some helpful, small lemmas around conjugation in groups, as well as `commute_iff_eq`,
which removes the need to use `show` or `unfold` to get an expression of the form `a * b = b * a` to prove.

Mathlib/Algebra/Group/Basic.lean

@@ -781,6 +781,10 @@ theorem inv_mul_eq_one : a⁻¹ * b = 1 ↔ a = b := by rw [mul_eq_one_iff_eq_in
 #align inv_mul_eq_one inv_mul_eq_one
 #align neg_add_eq_zero neg_add_eq_zero
 
+@[to_additive (attr := simp)]
+theorem conj_eq_one_iff : a * b * a⁻¹ = 1 ↔ b = 1 := by
+  rw [mul_inv_eq_one, mul_right_eq_self]
+
 @[to_additive]
 theorem div_left_injective : Function.Injective fun a ↦ a / b := by
   -- FIXME this could be by `simpa`, but it fails. This is probably a bug in `simpa`.

Mathlib/Algebra/Group/Commute/Basic.lean

@@ -91,5 +91,13 @@ lemma inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by
 #align commute.inv_mul_cancel_assoc Commute.inv_mul_cancel_assoc
 #align add_commute.neg_add_cancel_assoc AddCommute.neg_add_cancel_assoc
 
+@[to_additive (attr := simp)]
+protected theorem conj_iff (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹) ↔ Commute a b :=
+  SemiconjBy.conj_iff
+
+@[to_additive]
+protected theorem conj (comm : Commute a b) (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹) :=
+  (Commute.conj_iff h).mpr comm
+
 end Group
 end Commute

Mathlib/Algebra/Group/Commute/Defs.lean

@@ -38,6 +38,12 @@ def Commute {S : Type*} [Mul S] (a b : S) : Prop :=
 #align commute Commute
 #align add_commute AddCommute
 
+/--
+Two elements `a` and `b` commute if `a * b = b * a`.
+-/
+@[to_additive]
+theorem commute_iff_eq {S : Type*} [Mul S] (a b : S) : Commute a b ↔ a * b = b * a := Iff.rfl
+
 namespace Commute
 
 section Mul

Mathlib/Algebra/Group/Semiconj/Defs.lean

@@ -140,6 +140,14 @@ theorem conj_mk (a x : G) : SemiconjBy a x (a * x * a⁻¹) := by
 #align semiconj_by.conj_mk SemiconjBy.conj_mk
 #align add_semiconj_by.conj_mk AddSemiconjBy.conj_mk
 
+@[to_additive (attr := simp)]
+theorem conj_iff {a x y b : G} :
+    SemiconjBy (b * a * b⁻¹) (b * x * b⁻¹) (b * y * b⁻¹) ↔ SemiconjBy a x y := by
+  unfold SemiconjBy
+  simp only [← mul_assoc, inv_mul_cancel_right]
+  repeat rw [mul_assoc]
+  rw [mul_left_cancel_iff, ← mul_assoc, ← mul_assoc, mul_right_cancel_iff]
+
 end Group
 
 end SemiconjBy