Subgroup_is_Normal_Subgroup_of_Normalizer

import Mathlib.Analysis.Complex.Basic

theorem Subgroup_is_Normal_Subgroup_of_Normalizer {G : Type _} [Group G] (H : Subgroup G) (g : G) (hg : g ∈ H.normalizer) (h : G) (hh : h ∈ H) : g * h * g⁻¹ ∈ H := by sorry