Normalizer_of_Conjugate_is_Conjugate_of_Normalizer

import Mathlib.Analysis.Complex.Basic

theorem Normalizer_of_Conjugate_is_Conjugate_of_Normalizer {G : Type _} [Group G] (H : Subgroup G) (a g : G) (hg : g ∈ H.normalizer) : a * g * a⁻¹ ∈ (H.map (MulAut.conj a).toMonoidHom).normalizer := by sorry