theorem NormalSubgroups.normal_iff_leftCoset_eq_rightCoset {G : Type u_1} [Group G] (H : Subgroup G) : H.Normal ↔ ∀ (g : G), g • ↑H = MulOpposite.op g • ↑H

theorem NormalSubgroups.normal_iff_conj_image_eq {G : Type u_1} [Group G] (H : Subgroup G) : H.Normal ↔ ∀ (g : G), ⇑(MulAut.conj g) '' ↑H = ↑H

theorem NormalSubgroups.normal_iff_conj_mem {G : Type u_1} [Group G] (H : Subgroup G) : H.Normal ↔ ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H

theorem NormalSubgroups.normal_tfae {G : Type u_1} [Group G] (H : Subgroup G) : [H.Normal, ∀ (g : G), g • ↑H = MulOpposite.op g • ↑H, ∀ (g : G), ⇑(MulAut.conj g) '' ↑H = ↑H, ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H].TFAE