G : Type u_1
inst✝ : Group G
a✝ x✝ y a x : G
⊢ a * x = a * x * a⁻¹ * a
G : Type u_1
inst✝ : Group G
a✝ x✝ y a x : G
⊢ SemiconjBy a x (a * x * a⁻¹)
unfold SemiconjBy
no goals
G : Type u_1
inst✝ : Group G
a✝ x✝ y a x : G
⊢ a * x = a * x * a⁻¹ * a
rw [mul_assoc, inv_mul_self, mul_one]