Conjugate_of_Subgroup_is_Subgroup

import Mathlib.Analysis.Complex.Basic

theorem Conjugate_of_Subgroup_is_Subgroup {G : Type _} [Group G] (H : Subgroup G) (a : G) (h : G) (hh : h ∈ H) : a * h * a⁻¹ ∈ H.map (MulAut.conj a).toMonoidHom := by sorry