Conjugate_of_Set_by_Group_Product

import Mathlib.Analysis.Complex.Basic

theorem Conjugate_of_Set_by_Group_Product {G : Type _} [Group G] (s a b : G) : b * (a * s * a⁻¹) * b⁻¹ = (b * a) * s * (b * a)⁻¹ := by sorry