English
For group G, and x,y in Conj G, x ◃ y = y ↔ y ◃ x = x; i.e., symmetry of the conjugation operation.
Русский
Для группы G и элементов x,y из Conj G, x ◃ y = y ↔ y ◃ x = x; то есть симметрия операции конъюгации.
LaTeX
$$$x \triangleleft y = y \iff y \triangleleft x = x$$$
Lean4
theorem conj_swap {G : Type*} [Group G] (x y : Conj G) : x ◃ y = y ↔ y ◃ x = x :=
by
dsimp [Conj] at *; constructor
repeat' intro h; conv_rhs => rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp