diff --git a/Mathlib.lean b/Mathlib.lean
index 8f9f578b01b59..b3fc5c09d5010 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -289,6 +289,7 @@ import Mathlib.Algebra.Group.Semiconj.Defs
 import Mathlib.Algebra.Group.Semiconj.Units
 import Mathlib.Algebra.Group.Subgroup.Actions
 import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Group.Subgroup.Finite
 import Mathlib.Algebra.Group.Subgroup.MulOpposite
 import Mathlib.Algebra.Group.Subgroup.Order
diff --git a/Mathlib/Algebra/GradedMonoid.lean b/Mathlib/Algebra/GradedMonoid.lean
index 5f4ad73f043d1..12fa6e2789b3c 100644
--- a/Mathlib/Algebra/GradedMonoid.lean
+++ b/Mathlib/Algebra/GradedMonoid.lean
@@ -4,11 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Algebra.BigOperators.Group.List
-import Mathlib.Algebra.Group.InjSurj
+import Mathlib.Algebra.Group.Action.End
+import Mathlib.Algebra.Group.Submonoid.Defs
 import Mathlib.Data.List.FinRange
-import Mathlib.Algebra.Group.Action.Defs
 import Mathlib.Data.SetLike.Basic
-import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Data.Sigma.Basic
 import Lean.Elab.Tactic
 
diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean
index ca7a9f590871e..4896096b2e55e 100644
--- a/Mathlib/Algebra/Group/Subgroup/Basic.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean
@@ -5,17 +5,14 @@ Authors: Kexing Ying
 -/
 import Mathlib.Algebra.Group.Conj
 import Mathlib.Algebra.Group.Pi.Lemmas
-import Mathlib.Algebra.Group.Subsemigroup.Operations
 import Mathlib.Algebra.Group.Submonoid.Operations
+import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Data.Set.Image
 import Mathlib.Tactic.ApplyFun
 
 /-!
 # Subgroups
 
-This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled
-form (unbundled subgroups are in `Deprecated/Subgroups.lean`).
-
 We prove subgroups of a group form a complete lattice, and results about images and preimages of
 subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.
 
@@ -43,10 +40,6 @@ Notation used here:
 
 Definitions in the file:
 
-* `Subgroup G` : the type of subgroups of a group `G`
-
-* `AddSubgroup A` : the type of subgroups of an additive group `A`
-
 * `CompleteLattice (Subgroup G)` : the subgroups of `G` form a complete lattice
 
 * `Subgroup.closure k` : the minimal subgroup that includes the set `k`
@@ -93,302 +86,16 @@ variable {A : Type*} [AddGroup A]
 
 section SubgroupClass
 
-/-- `InvMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under inverses. -/
-class InvMemClass (S : Type*) (G : outParam Type*) [Inv G] [SetLike S G] : Prop where
-  /-- `s` is closed under inverses -/
-  inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s
-
-export InvMemClass (inv_mem)
-
-/-- `NegMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under negation. -/
-class NegMemClass (S : Type*) (G : outParam Type*) [Neg G] [SetLike S G] : Prop where
-  /-- `s` is closed under negation -/
-  neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s
-
-export NegMemClass (neg_mem)
-
-/-- `SubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`. -/
-class SubgroupClass (S : Type*) (G : outParam Type*) [DivInvMonoid G] [SetLike S G]
-    extends SubmonoidClass S G, InvMemClass S G : Prop
-
-/-- `AddSubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are
-additive subgroups of `G`. -/
-class AddSubgroupClass (S : Type*) (G : outParam Type*) [SubNegMonoid G] [SetLike S G]
-    extends AddSubmonoidClass S G, NegMemClass S G : Prop
-
-attribute [to_additive] InvMemClass SubgroupClass
-
-attribute [aesop safe apply (rule_sets := [SetLike])] inv_mem neg_mem
-
-@[to_additive (attr := simp)]
-theorem inv_mem_iff {S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G] {H : S}
-    {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
-  ⟨fun h => inv_inv x ▸ inv_mem h, inv_mem⟩
-
 variable {M S : Type*} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {H K : S}
 
-/-- A subgroup is closed under division. -/
-@[to_additive (attr := aesop safe apply (rule_sets := [SetLike]))
-  "An additive subgroup is closed under subtraction."]
-theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H := by
-  rw [div_eq_mul_inv]; exact mul_mem hx (inv_mem hy)
-
-@[to_additive (attr := aesop safe apply (rule_sets := [SetLike]))]
-theorem zpow_mem {x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
-  | (n : ℕ) => by
-    rw [zpow_natCast]
-    exact pow_mem hx n
-  | -[n+1] => by
-    rw [zpow_negSucc]
-    exact inv_mem (pow_mem hx n.succ)
-
 variable [SetLike S G] [SubgroupClass S G]
 
 @[to_additive]
 theorem div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
   inv_div b a ▸ inv_mem_iff
 
-@[to_additive /-(attr := simp)-/] -- Porting note: `simp` cannot simplify LHS
-theorem exists_inv_mem_iff_exists_mem {P : G → Prop} :
-    (∃ x : G, x ∈ H ∧ P x⁻¹) ↔ ∃ x ∈ H, P x := by
-  constructor <;>
-    · rintro ⟨x, x_in, hx⟩
-      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩
-
-@[to_additive]
-theorem mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
-  ⟨fun hba => by simpa using mul_mem hba (inv_mem h), fun hb => mul_mem hb h⟩
-
-@[to_additive]
-theorem mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
-  ⟨fun hab => by simpa using mul_mem (inv_mem h) hab, mul_mem h⟩
-
-namespace InvMemClass
-
-/-- A subgroup of a group inherits an inverse. -/
-@[to_additive "An additive subgroup of an `AddGroup` inherits an inverse."]
-instance inv {G : Type u_1} {S : Type u_2} [Inv G] [SetLike S G]
-  [InvMemClass S G] {H : S} : Inv H :=
-  ⟨fun a => ⟨a⁻¹, inv_mem a.2⟩⟩
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_inv (x : H) : (x⁻¹).1 = x.1⁻¹ :=
-  rfl
-
-end InvMemClass
-
-namespace SubgroupClass
-
-@[to_additive (attr := deprecated (since := "2024-01-15"))] alias coe_inv := InvMemClass.coe_inv
-
--- Here we assume H, K, and L are subgroups, but in fact any one of them
--- could be allowed to be a subsemigroup.
--- Counterexample where K and L are submonoids: H = ℤ, K = ℕ, L = -ℕ
--- Counterexample where H and K are submonoids: H = {n | n = 0 ∨ 3 ≤ n}, K = 3ℕ + 4ℕ, L = 5ℤ
-@[to_additive]
-theorem subset_union {H K L : S} : (H : Set G) ⊆ K ∪ L ↔ H ≤ K ∨ H ≤ L := by
-  refine ⟨fun h ↦ ?_, fun h x xH ↦ h.imp (· xH) (· xH)⟩
-  rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
-  exact fun ⟨x, xH, xK⟩ y yH ↦ (h <| mul_mem xH yH).elim
-    ((h yH).resolve_left fun yK ↦ xK <| (mul_mem_cancel_right yK).mp ·)
-    (mul_mem_cancel_left <| (h xH).resolve_left xK).mp
-
-/-- A subgroup of a group inherits a division -/
-@[to_additive "An additive subgroup of an `AddGroup` inherits a subtraction."]
-instance div {G : Type u_1} {S : Type u_2} [DivInvMonoid G] [SetLike S G]
-  [SubgroupClass S G] {H : S} : Div H :=
-  ⟨fun a b => ⟨a / b, div_mem a.2 b.2⟩⟩
-
-/-- An additive subgroup of an `AddGroup` inherits an integer scaling. -/
-instance _root_.AddSubgroupClass.zsmul {M S} [SubNegMonoid M] [SetLike S M]
-    [AddSubgroupClass S M] {H : S} : SMul ℤ H :=
-  ⟨fun n a => ⟨n • a.1, zsmul_mem a.2 n⟩⟩
-
-/-- A subgroup of a group inherits an integer power. -/
-@[to_additive existing]
-instance zpow {M S} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow H ℤ :=
-  ⟨fun a n => ⟨a.1 ^ n, zpow_mem a.2 n⟩⟩
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_div (x y : H) : (x / y).1 = x.1 / y.1 :=
-  rfl
-
-variable (H)
-
--- Prefer subclasses of `Group` over subclasses of `SubgroupClass`.
-/-- A subgroup of a group inherits a group structure. -/
-@[to_additive "An additive subgroup of an `AddGroup` inherits an `AddGroup` structure."]
-instance (priority := 75) toGroup : Group H :=
-  Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
-
--- Prefer subclasses of `CommGroup` over subclasses of `SubgroupClass`.
-/-- A subgroup of a `CommGroup` is a `CommGroup`. -/
-@[to_additive "An additive subgroup of an `AddCommGroup` is an `AddCommGroup`."]
-instance (priority := 75) toCommGroup {G : Type*} [CommGroup G] [SetLike S G] [SubgroupClass S G] :
-    CommGroup H :=
-  Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
-
-/-- The natural group hom from a subgroup of group `G` to `G`. -/
-@[to_additive (attr := coe)
-  "The natural group hom from an additive subgroup of `AddGroup` `G` to `G`."]
-protected def subtype : H →* G where
-  toFun := ((↑) : H → G); map_one' := rfl; map_mul' := fun _ _ => rfl
-
-@[to_additive (attr := simp)]
-theorem coeSubtype : (SubgroupClass.subtype H : H → G) = ((↑) : H → G) := by
-  rfl
-
-variable {H}
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n :=
-  rfl
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n :=
-  rfl
-
-/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
-@[to_additive "The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`."]
-def inclusion {H K : S} (h : H ≤ K) : H →* K :=
-  MonoidHom.mk' (fun x => ⟨x, h x.prop⟩) fun _ _=> rfl
-
-@[to_additive (attr := simp)]
-theorem inclusion_self (x : H) : inclusion le_rfl x = x := by
-  cases x
-  rfl
-
-@[to_additive (attr := simp)]
-theorem inclusion_mk {h : H ≤ K} (x : G) (hx : x ∈ H) : inclusion h ⟨x, hx⟩ = ⟨x, h hx⟩ :=
-  rfl
-
-@[to_additive]
-theorem inclusion_right (h : H ≤ K) (x : K) (hx : (x : G) ∈ H) : inclusion h ⟨x, hx⟩ = x := by
-  cases x
-  rfl
-
-@[simp]
-theorem inclusion_inclusion {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : H) :
-    inclusion hKL (inclusion hHK x) = inclusion (hHK.trans hKL) x := by
-  cases x
-  rfl
-
-@[to_additive (attr := simp)]
-theorem coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
-  cases a
-  simp only [inclusion, MonoidHom.mk'_apply]
-
-@[to_additive (attr := simp)]
-theorem subtype_comp_inclusion {H K : S} (hH : H ≤ K) :
-    (SubgroupClass.subtype K).comp (inclusion hH) = SubgroupClass.subtype H := by
-  ext
-  simp only [MonoidHom.comp_apply, coeSubtype, coe_inclusion]
-
-end SubgroupClass
-
 end SubgroupClass
 
-/-- A subgroup of a group `G` is a subset containing 1, closed under multiplication
-and closed under multiplicative inverse. -/
-structure Subgroup (G : Type*) [Group G] extends Submonoid G where
-  /-- `G` is closed under inverses -/
-  inv_mem' {x} : x ∈ carrier → x⁻¹ ∈ carrier
-
-/-- An additive subgroup of an additive group `G` is a subset containing 0, closed
-under addition and additive inverse. -/
-structure AddSubgroup (G : Type*) [AddGroup G] extends AddSubmonoid G where
-  /-- `G` is closed under negation -/
-  neg_mem' {x} : x ∈ carrier → -x ∈ carrier
-
-attribute [to_additive] Subgroup
-
--- Porting note: Removed, translation already exists
--- attribute [to_additive AddSubgroup.toAddSubmonoid] Subgroup.toSubmonoid
-
-/-- Reinterpret a `Subgroup` as a `Submonoid`. -/
-add_decl_doc Subgroup.toSubmonoid
-
-/-- Reinterpret an `AddSubgroup` as an `AddSubmonoid`. -/
-add_decl_doc AddSubgroup.toAddSubmonoid
-
-namespace Subgroup
-
-@[to_additive]
-instance : SetLike (Subgroup G) G where
-  coe s := s.carrier
-  coe_injective' p q h := by
-    obtain ⟨⟨⟨hp,_⟩,_⟩,_⟩ := p
-    obtain ⟨⟨⟨hq,_⟩,_⟩,_⟩ := q
-    congr
-
--- Porting note: Below can probably be written more uniformly
-@[to_additive]
-instance : SubgroupClass (Subgroup G) G where
-  inv_mem := Subgroup.inv_mem' _
-  one_mem _ := (Subgroup.toSubmonoid _).one_mem'
-  mul_mem := (Subgroup.toSubmonoid _).mul_mem'
-
-@[to_additive (attr := simp, nolint simpNF)] -- Porting note (#10675): dsimp can not prove this
-theorem mem_carrier {s : Subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s :=
-  Iff.rfl
-
-@[to_additive (attr := simp)]
-theorem mem_mk {s : Set G} {x : G} (h_one) (h_mul) (h_inv) :
-    x ∈ mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ↔ x ∈ s :=
-  Iff.rfl
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_set_mk {s : Set G} (h_one) (h_mul) (h_inv) :
-    (mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv : Set G) = s :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk_le_mk {s t : Set G} (h_one) (h_mul) (h_inv) (h_one') (h_mul') (h_inv') :
-    mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ≤ mk ⟨⟨t, h_one'⟩, h_mul'⟩ h_inv' ↔ s ⊆ t :=
-  Iff.rfl
-
-initialize_simps_projections Subgroup (carrier → coe)
-initialize_simps_projections AddSubgroup (carrier → coe)
-
-@[to_additive (attr := simp)]
-theorem coe_toSubmonoid (K : Subgroup G) : (K.toSubmonoid : Set G) = K :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mem_toSubmonoid (K : Subgroup G) (x : G) : x ∈ K.toSubmonoid ↔ x ∈ K :=
-  Iff.rfl
-
-@[to_additive]
-theorem toSubmonoid_injective : Function.Injective (toSubmonoid : Subgroup G → Submonoid G) :=
-  -- fun p q h => SetLike.ext'_iff.2 (show _ from SetLike.ext'_iff.1 h)
-  fun p q h => by
-    have := SetLike.ext'_iff.1 h
-    rw [coe_toSubmonoid, coe_toSubmonoid] at this
-    exact SetLike.ext'_iff.2 this
-
-@[to_additive (attr := simp)]
-theorem toSubmonoid_eq {p q : Subgroup G} : p.toSubmonoid = q.toSubmonoid ↔ p = q :=
-  toSubmonoid_injective.eq_iff
-
-@[to_additive (attr := mono)]
-theorem toSubmonoid_strictMono : StrictMono (toSubmonoid : Subgroup G → Submonoid G) := fun _ _ =>
-  id
-
-@[to_additive (attr := mono)]
-theorem toSubmonoid_mono : Monotone (toSubmonoid : Subgroup G → Submonoid G) :=
-  toSubmonoid_strictMono.monotone
-
-@[to_additive (attr := simp)]
-theorem toSubmonoid_le {p q : Subgroup G} : p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q :=
-  Iff.rfl
-
-@[to_additive (attr := simp)]
-lemma coe_nonempty (s : Subgroup G) : (s : Set G).Nonempty := ⟨1, one_mem _⟩
-
-end Subgroup
-
 /-!
 ### Conversion to/from `Additive`/`Multiplicative`
 -/
@@ -430,211 +137,10 @@ namespace Subgroup
 
 variable (H K : Subgroup G)
 
-/-- Copy of a subgroup with a new `carrier` equal to the old one. Useful to fix definitional
-equalities. -/
-@[to_additive
-      "Copy of an additive subgroup with a new `carrier` equal to the old one.
-      Useful to fix definitional equalities"]
-protected def copy (K : Subgroup G) (s : Set G) (hs : s = K) : Subgroup G where
-  carrier := s
-  one_mem' := hs.symm ▸ K.one_mem'
-  mul_mem' := hs.symm ▸ K.mul_mem'
-  inv_mem' hx := by simpa [hs] using hx -- Porting note: `▸` didn't work here
-
-@[to_additive (attr := simp)]
-theorem coe_copy (K : Subgroup G) (s : Set G) (hs : s = ↑K) : (K.copy s hs : Set G) = s :=
-  rfl
-
-@[to_additive]
-theorem copy_eq (K : Subgroup G) (s : Set G) (hs : s = ↑K) : K.copy s hs = K :=
-  SetLike.coe_injective hs
-
-/-- Two subgroups are equal if they have the same elements. -/
-@[to_additive (attr := ext) "Two `AddSubgroup`s are equal if they have the same elements."]
-theorem ext {H K : Subgroup G} (h : ∀ x, x ∈ H ↔ x ∈ K) : H = K :=
-  SetLike.ext h
-
-/-- A subgroup contains the group's 1. -/
-@[to_additive "An `AddSubgroup` contains the group's 0."]
-protected theorem one_mem : (1 : G) ∈ H :=
-  one_mem _
-
-/-- A subgroup is closed under multiplication. -/
-@[to_additive "An `AddSubgroup` is closed under addition."]
-protected theorem mul_mem {x y : G} : x ∈ H → y ∈ H → x * y ∈ H :=
-  mul_mem
-
-/-- A subgroup is closed under inverse. -/
-@[to_additive "An `AddSubgroup` is closed under inverse."]
-protected theorem inv_mem {x : G} : x ∈ H → x⁻¹ ∈ H :=
-  inv_mem
-
-/-- A subgroup is closed under division. -/
-@[to_additive "An `AddSubgroup` is closed under subtraction."]
-protected theorem div_mem {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H :=
-  div_mem hx hy
-
-@[to_additive]
-protected theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
-  inv_mem_iff
-
 @[to_additive]
 protected theorem div_mem_comm_iff {a b : G} : a / b ∈ H ↔ b / a ∈ H :=
   div_mem_comm_iff
 
-@[to_additive]
-protected theorem exists_inv_mem_iff_exists_mem (K : Subgroup G) {P : G → Prop} :
-    (∃ x : G, x ∈ K ∧ P x⁻¹) ↔ ∃ x ∈ K, P x :=
-  exists_inv_mem_iff_exists_mem
-
-@[to_additive]
-protected theorem mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
-  mul_mem_cancel_right h
-
-@[to_additive]
-protected theorem mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
-  mul_mem_cancel_left h
-
-@[to_additive]
-protected theorem pow_mem {x : G} (hx : x ∈ K) : ∀ n : ℕ, x ^ n ∈ K :=
-  pow_mem hx
-
-@[to_additive]
-protected theorem zpow_mem {x : G} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K :=
-  zpow_mem hx
-
-/-- Construct a subgroup from a nonempty set that is closed under division. -/
-@[to_additive "Construct a subgroup from a nonempty set that is closed under subtraction"]
-def ofDiv (s : Set G) (hsn : s.Nonempty) (hs : ∀ᵉ (x ∈ s) (y ∈ s), x * y⁻¹ ∈ s) :
-    Subgroup G :=
-  have one_mem : (1 : G) ∈ s := by
-    let ⟨x, hx⟩ := hsn
-    simpa using hs x hx x hx
-  have inv_mem : ∀ x, x ∈ s → x⁻¹ ∈ s := fun x hx => by simpa using hs 1 one_mem x hx
-  { carrier := s
-    one_mem' := one_mem
-    inv_mem' := inv_mem _
-    mul_mem' := fun hx hy => by simpa using hs _ hx _ (inv_mem _ hy) }
-
-/-- A subgroup of a group inherits a multiplication. -/
-@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an addition."]
-instance mul : Mul H :=
-  H.toSubmonoid.mul
-
-/-- A subgroup of a group inherits a 1. -/
-@[to_additive "An `AddSubgroup` of an `AddGroup` inherits a zero."]
-instance one : One H :=
-  H.toSubmonoid.one
-
-/-- A subgroup of a group inherits an inverse. -/
-@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an inverse."]
-instance inv : Inv H :=
-  ⟨fun a => ⟨a⁻¹, H.inv_mem a.2⟩⟩
-
-/-- A subgroup of a group inherits a division -/
-@[to_additive "An `AddSubgroup` of an `AddGroup` inherits a subtraction."]
-instance div : Div H :=
-  ⟨fun a b => ⟨a / b, H.div_mem a.2 b.2⟩⟩
-
-/-- An `AddSubgroup` of an `AddGroup` inherits a natural scaling. -/
-instance _root_.AddSubgroup.nsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℕ H :=
-  ⟨fun n a => ⟨n • a, H.nsmul_mem a.2 n⟩⟩
-
-/-- A subgroup of a group inherits a natural power -/
-@[to_additive existing]
-protected instance npow : Pow H ℕ :=
-  ⟨fun a n => ⟨a ^ n, H.pow_mem a.2 n⟩⟩
-
-/-- An `AddSubgroup` of an `AddGroup` inherits an integer scaling. -/
-instance _root_.AddSubgroup.zsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℤ H :=
-  ⟨fun n a => ⟨n • a, H.zsmul_mem a.2 n⟩⟩
-
-/-- A subgroup of a group inherits an integer power -/
-@[to_additive existing]
-instance zpow : Pow H ℤ :=
-  ⟨fun a n => ⟨a ^ n, H.zpow_mem a.2 n⟩⟩
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_mul (x y : H) : (↑(x * y) : G) = ↑x * ↑y :=
-  rfl
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_one : ((1 : H) : G) = 1 :=
-  rfl
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_inv (x : H) : ↑(x⁻¹ : H) = (x⁻¹ : G) :=
-  rfl
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_div (x y : H) : (↑(x / y) : G) = ↑x / ↑y :=
-  rfl
-
--- Porting note: removed simp, theorem has variable as head symbol
-@[to_additive (attr := norm_cast)]
-theorem coe_mk (x : G) (hx : x ∈ H) : ((⟨x, hx⟩ : H) : G) = x :=
-  rfl
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n :=
-  rfl
-
-@[to_additive (attr := norm_cast)] -- Porting note (#10685): dsimp can prove this
-theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk_eq_one {g : G} {h} : (⟨g, h⟩ : H) = 1 ↔ g = 1 := Submonoid.mk_eq_one ..
-
-/-- A subgroup of a group inherits a group structure. -/
-@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an `AddGroup` structure."]
-instance toGroup {G : Type*} [Group G] (H : Subgroup G) : Group H :=
-  Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
-
-/-- A subgroup of a `CommGroup` is a `CommGroup`. -/
-@[to_additive "An `AddSubgroup` of an `AddCommGroup` is an `AddCommGroup`."]
-instance toCommGroup {G : Type*} [CommGroup G] (H : Subgroup G) : CommGroup H :=
-  Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
-    (fun _ _ => rfl) fun _ _ => rfl
-
-/-- The natural group hom from a subgroup of group `G` to `G`. -/
-@[to_additive "The natural group hom from an `AddSubgroup` of `AddGroup` `G` to `G`."]
-protected def subtype : H →* G where
-  toFun := ((↑) : H → G); map_one' := rfl; map_mul' _ _ := rfl
-
-@[to_additive (attr := simp)]
-theorem coeSubtype : ⇑ H.subtype = ((↑) : H → G) :=
-  rfl
-
-@[to_additive]
-theorem subtype_injective : Function.Injective (Subgroup.subtype H) :=
-  Subtype.coe_injective
-
-/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
-@[to_additive "The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`."]
-def inclusion {H K : Subgroup G} (h : H ≤ K) : H →* K :=
-  MonoidHom.mk' (fun x => ⟨x, h x.2⟩) fun _ _ => rfl
-
-@[to_additive (attr := simp)]
-theorem coe_inclusion {H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
-  cases a
-  simp only [inclusion, coe_mk, MonoidHom.mk'_apply]
-
-@[to_additive]
-theorem inclusion_injective {H K : Subgroup G} (h : H ≤ K) : Function.Injective <| inclusion h :=
-  Set.inclusion_injective h
-
-@[to_additive (attr := simp)]
-lemma inclusion_inj {H K : Subgroup G} (h : H ≤ K) {x y : H} :
-    inclusion h x = inclusion h y ↔ x = y :=
-  (inclusion_injective h).eq_iff
-
-@[to_additive (attr := simp)]
-theorem subtype_comp_inclusion {H K : Subgroup G} (hH : H ≤ K) :
-    K.subtype.comp (inclusion hH) = H.subtype :=
-  rfl
-
 /-- The subgroup `G` of the group `G`. -/
 @[to_additive "The `AddSubgroup G` of the `AddGroup G`."]
 instance : Top (Subgroup G) :=
@@ -1507,57 +1013,12 @@ theorem pi_eq_bot_iff (H : ∀ i, Subgroup (f i)) : pi Set.univ H = ⊥ ↔ ∀
 
 end Pi
 
-/-- A subgroup is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` -/
-structure Normal : Prop where
-  /-- `N` is closed under conjugation -/
-  conj_mem : ∀ n, n ∈ H → ∀ g : G, g * n * g⁻¹ ∈ H
-
-attribute [class] Normal
-
 end Subgroup
 
-namespace AddSubgroup
-
-/-- An AddSubgroup is normal if whenever `n ∈ H`, then `g + n - g ∈ H` for every `g : G` -/
-structure Normal (H : AddSubgroup A) : Prop where
-  /-- `N` is closed under additive conjugation -/
-  conj_mem : ∀ n, n ∈ H → ∀ g : A, g + n + -g ∈ H
-
-attribute [to_additive] Subgroup.Normal
-
-attribute [class] Normal
-
-end AddSubgroup
-
 namespace Subgroup
 
 variable {H K : Subgroup G}
 
-@[to_additive]
-instance (priority := 100) normal_of_comm {G : Type*} [CommGroup G] (H : Subgroup G) : H.Normal :=
-  ⟨by simp [mul_comm, mul_left_comm]⟩
-
-namespace Normal
-
-@[to_additive]
-theorem conj_mem' (nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) :
-    g⁻¹ * n * g ∈ H := by
-  convert nH.conj_mem n hn g⁻¹
-  rw [inv_inv]
-
-@[to_additive]
-theorem mem_comm (nH : H.Normal) {a b : G} (h : a * b ∈ H) : b * a ∈ H := by
-  have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹
-  -- Porting note: Previous code was:
-  -- simpa
-  simp_all only [inv_mul_cancel_left, inv_inv]
-
-@[to_additive]
-theorem mem_comm_iff (nH : H.Normal) {a b : G} : a * b ∈ H ↔ b * a ∈ H :=
-  ⟨nH.mem_comm, nH.mem_comm⟩
-
-end Normal
-
 variable (H)
 
 /-- A subgroup is characteristic if it is fixed by all automorphisms.
@@ -1640,53 +1101,8 @@ variable (H)
 
 section Normalizer
 
-/-- The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal. -/
-@[to_additive "The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal."]
-def normalizer : Subgroup G where
-  carrier := { g : G | ∀ n, n ∈ H ↔ g * n * g⁻¹ ∈ H }
-  one_mem' := by simp
-  mul_mem' {a b} (ha : ∀ n, n ∈ H ↔ a * n * a⁻¹ ∈ H) (hb : ∀ n, n ∈ H ↔ b * n * b⁻¹ ∈ H) n := by
-    rw [hb, ha]
-    simp only [mul_assoc, mul_inv_rev]
-  inv_mem' {a} (ha : ∀ n, n ∈ H ↔ a * n * a⁻¹ ∈ H) n := by
-    rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
-    simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]
-
--- variant for sets.
--- TODO should this replace `normalizer`?
-/-- The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy `g*S*g⁻¹=S` -/
-@[to_additive
-      "The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy
-      `g+S-g=S`."]
-def setNormalizer (S : Set G) : Subgroup G where
-  carrier := { g : G | ∀ n, n ∈ S ↔ g * n * g⁻¹ ∈ S }
-  one_mem' := by simp
-  mul_mem' {a b} (ha : ∀ n, n ∈ S ↔ a * n * a⁻¹ ∈ S) (hb : ∀ n, n ∈ S ↔ b * n * b⁻¹ ∈ S) n := by
-    rw [hb, ha]
-    simp only [mul_assoc, mul_inv_rev]
-  inv_mem' {a} (ha : ∀ n, n ∈ S ↔ a * n * a⁻¹ ∈ S) n := by
-    rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
-    simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]
-
 variable {H}
 
-@[to_additive]
-theorem mem_normalizer_iff {g : G} : g ∈ H.normalizer ↔ ∀ h, h ∈ H ↔ g * h * g⁻¹ ∈ H :=
-  Iff.rfl
-
-@[to_additive]
-theorem mem_normalizer_iff'' {g : G} : g ∈ H.normalizer ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H := by
-  rw [← inv_mem_iff (x := g), mem_normalizer_iff, inv_inv]
-
-@[to_additive]
-theorem mem_normalizer_iff' {g : G} : g ∈ H.normalizer ↔ ∀ n, n * g ∈ H ↔ g * n ∈ H :=
-  ⟨fun h n => by rw [h, mul_assoc, mul_inv_cancel_right], fun h n => by
-    rw [mul_assoc, ← h, inv_mul_cancel_right]⟩
-
-@[to_additive]
-theorem le_normalizer : H ≤ normalizer H := fun x xH n => by
-  rw [H.mul_mem_cancel_right (H.inv_mem xH), H.mul_mem_cancel_left xH]
-
 @[to_additive]
 instance (priority := 100) normal_in_normalizer : (H.subgroupOf H.normalizer).Normal :=
   ⟨fun x xH g => by simpa only [mem_subgroupOf] using (g.2 x.1).1 xH⟩
@@ -1748,32 +1164,6 @@ variable (H)
 
 end Normalizer
 
-/-- Commutativity of a subgroup -/
-structure IsCommutative : Prop where
-  /-- `*` is commutative on `H` -/
-  is_comm : Std.Commutative (α := H) (· * ·)
-
-attribute [class] IsCommutative
-
-/-- Commutativity of an additive subgroup -/
-structure _root_.AddSubgroup.IsCommutative (H : AddSubgroup A) : Prop where
-  /-- `+` is commutative on `H` -/
-  is_comm : Std.Commutative (α := H) (· + ·)
-
-attribute [to_additive] Subgroup.IsCommutative
-
-attribute [class] AddSubgroup.IsCommutative
-
-/-- A commutative subgroup is commutative. -/
-@[to_additive "A commutative subgroup is commutative."]
-instance IsCommutative.commGroup [h : H.IsCommutative] : CommGroup H :=
-  { H.toGroup with mul_comm := h.is_comm.comm }
-
-/-- A subgroup of a commutative group is commutative. -/
-@[to_additive "A subgroup of a commutative group is commutative."]
-instance commGroup_isCommutative {G : Type*} [CommGroup G] (H : Subgroup G) : H.IsCommutative :=
-  ⟨CommMagma.to_isCommutative⟩
-
 @[to_additive]
 instance map_isCommutative (f : G →* G') [H.IsCommutative] : (H.map f).IsCommutative :=
   ⟨⟨by
@@ -1795,11 +1185,6 @@ theorem comap_injective_isCommutative {f : G' →* G} (hf : Injective f) [H.IsCo
 instance subgroupOf_isCommutative [H.IsCommutative] : (H.subgroupOf K).IsCommutative :=
   H.comap_injective_isCommutative Subtype.coe_injective
 
-@[to_additive]
-lemma mul_comm_of_mem_isCommutative [H.IsCommutative] {a b : G} (ha : a ∈ H) (hb : b ∈ H) :
-    a * b = b * a := by
-  simpa only [MulMemClass.mk_mul_mk, Subtype.mk.injEq] using mul_comm (⟨a, ha⟩ : H) (⟨b, hb⟩ : H)
-
 end Subgroup
 
 namespace MulEquiv
@@ -2944,4 +2329,4 @@ def noncenter (G : Type*) [Monoid G] : Set (ConjClasses G) :=
 
 end ConjClasses
 
-set_option linter.style.longFile 3000
+set_option linter.style.longFile 2500
diff --git a/Mathlib/Algebra/Group/Subgroup/Defs.lean b/Mathlib/Algebra/Group/Subgroup/Defs.lean
new file mode 100644
index 0000000000000..2bbdaa180486f
--- /dev/null
+++ b/Mathlib/Algebra/Group/Subgroup/Defs.lean
@@ -0,0 +1,704 @@
+/-
+Copyright (c) 2020 Kexing Ying. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kexing Ying
+-/
+import Mathlib.Algebra.Group.Submonoid.Defs
+import Mathlib.Tactic.Common
+
+/-!
+# Subgroups
+
+This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled
+form (unbundled subgroups are in `Deprecated/Subgroups.lean`).
+
+Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
+
+## Main definitions
+
+Notation used here:
+
+- `G N` are `Group`s
+
+- `A` is an `AddGroup`
+
+- `H K` are `Subgroup`s of `G` or `AddSubgroup`s of `A`
+
+- `x` is an element of type `G` or type `A`
+
+- `f g : N →* G` are group homomorphisms
+
+- `s k` are sets of elements of type `G`
+
+Definitions in the file:
+
+* `Subgroup G` : the type of subgroups of a group `G`
+
+* `AddSubgroup A` : the type of subgroups of an additive group `A`
+
+* `Subgroup.subtype` : the natural group homomorphism from a subgroup of group `G` to `G`
+
+## Implementation notes
+
+Subgroup inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as
+membership of a subgroup's underlying set.
+
+## Tags
+subgroup, subgroups
+-/
+
+assert_not_exists OrderedAddCommMonoid
+assert_not_exists Multiset
+assert_not_exists Ring
+
+open Function
+open scoped Int
+
+variable {G G' G'' : Type*} [Group G] [Group G'] [Group G'']
+variable {A : Type*} [AddGroup A]
+
+section SubgroupClass
+
+/-- `InvMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under inverses. -/
+class InvMemClass (S : Type*) (G : outParam Type*) [Inv G] [SetLike S G] : Prop where
+  /-- `s` is closed under inverses -/
+  inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s
+
+export InvMemClass (inv_mem)
+
+/-- `NegMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under negation. -/
+class NegMemClass (S : Type*) (G : outParam Type*) [Neg G] [SetLike S G] : Prop where
+  /-- `s` is closed under negation -/
+  neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s
+
+export NegMemClass (neg_mem)
+
+/-- `SubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`. -/
+class SubgroupClass (S : Type*) (G : outParam Type*) [DivInvMonoid G] [SetLike S G]
+    extends SubmonoidClass S G, InvMemClass S G : Prop
+
+/-- `AddSubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are
+additive subgroups of `G`. -/
+class AddSubgroupClass (S : Type*) (G : outParam Type*) [SubNegMonoid G] [SetLike S G]
+    extends AddSubmonoidClass S G, NegMemClass S G : Prop
+
+attribute [to_additive] InvMemClass SubgroupClass
+
+attribute [aesop safe apply (rule_sets := [SetLike])] inv_mem neg_mem
+
+@[to_additive (attr := simp)]
+theorem inv_mem_iff {S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G] {H : S}
+    {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
+  ⟨fun h => inv_inv x ▸ inv_mem h, inv_mem⟩
+
+variable {M S : Type*} [DivInvMonoid M] [SetLike S M] [hSM : SubgroupClass S M] {H K : S}
+
+/-- A subgroup is closed under division. -/
+@[to_additive (attr := aesop safe apply (rule_sets := [SetLike]))
+  "An additive subgroup is closed under subtraction."]
+theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H := by
+  rw [div_eq_mul_inv]; exact mul_mem hx (inv_mem hy)
+
+@[to_additive (attr := aesop safe apply (rule_sets := [SetLike]))]
+theorem zpow_mem {x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
+  | (n : ℕ) => by
+    rw [zpow_natCast]
+    exact pow_mem hx n
+  | -[n+1] => by
+    rw [zpow_negSucc]
+    exact inv_mem (pow_mem hx n.succ)
+
+variable [SetLike S G] [SubgroupClass S G]
+
+@[to_additive /-(attr := simp)-/] -- Porting note: `simp` cannot simplify LHS
+theorem exists_inv_mem_iff_exists_mem {P : G → Prop} :
+    (∃ x : G, x ∈ H ∧ P x⁻¹) ↔ ∃ x ∈ H, P x := by
+  constructor <;>
+    · rintro ⟨x, x_in, hx⟩
+      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩
+
+@[to_additive]
+theorem mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
+  ⟨fun hba => by simpa using mul_mem hba (inv_mem h), fun hb => mul_mem hb h⟩
+
+@[to_additive]
+theorem mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
+  ⟨fun hab => by simpa using mul_mem (inv_mem h) hab, mul_mem h⟩
+
+namespace InvMemClass
+
+/-- A subgroup of a group inherits an inverse. -/
+@[to_additive "An additive subgroup of an `AddGroup` inherits an inverse."]
+instance inv {G : Type u_1} {S : Type u_2} [Inv G] [SetLike S G]
+  [InvMemClass S G] {H : S} : Inv H :=
+  ⟨fun a => ⟨a⁻¹, inv_mem a.2⟩⟩
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_inv (x : H) : (x⁻¹).1 = x.1⁻¹ :=
+  rfl
+
+end InvMemClass
+
+namespace SubgroupClass
+
+@[to_additive (attr := deprecated (since := "2024-01-15"))] alias coe_inv := InvMemClass.coe_inv
+
+-- Here we assume H, K, and L are subgroups, but in fact any one of them
+-- could be allowed to be a subsemigroup.
+-- Counterexample where K and L are submonoids: H = ℤ, K = ℕ, L = -ℕ
+-- Counterexample where H and K are submonoids: H = {n | n = 0 ∨ 3 ≤ n}, K = 3ℕ + 4ℕ, L = 5ℤ
+@[to_additive]
+theorem subset_union {H K L : S} : (H : Set G) ⊆ K ∪ L ↔ H ≤ K ∨ H ≤ L := by
+  refine ⟨fun h ↦ ?_, fun h x xH ↦ h.imp (· xH) (· xH)⟩
+  rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
+  exact fun ⟨x, xH, xK⟩ y yH ↦ (h <| mul_mem xH yH).elim
+    ((h yH).resolve_left fun yK ↦ xK <| (mul_mem_cancel_right yK).mp ·)
+    (mul_mem_cancel_left <| (h xH).resolve_left xK).mp
+
+/-- A subgroup of a group inherits a division -/
+@[to_additive "An additive subgroup of an `AddGroup` inherits a subtraction."]
+instance div {G : Type u_1} {S : Type u_2} [DivInvMonoid G] [SetLike S G]
+  [SubgroupClass S G] {H : S} : Div H :=
+  ⟨fun a b => ⟨a / b, div_mem a.2 b.2⟩⟩
+
+/-- An additive subgroup of an `AddGroup` inherits an integer scaling. -/
+instance _root_.AddSubgroupClass.zsmul {M S} [SubNegMonoid M] [SetLike S M]
+    [AddSubgroupClass S M] {H : S} : SMul ℤ H :=
+  ⟨fun n a => ⟨n • a.1, zsmul_mem a.2 n⟩⟩
+
+/-- A subgroup of a group inherits an integer power. -/
+@[to_additive existing]
+instance zpow {M S} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow H ℤ :=
+  ⟨fun a n => ⟨a.1 ^ n, zpow_mem a.2 n⟩⟩
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_div (x y : H) : (x / y).1 = x.1 / y.1 :=
+  rfl
+
+variable (H)
+
+-- Prefer subclasses of `Group` over subclasses of `SubgroupClass`.
+/-- A subgroup of a group inherits a group structure. -/
+@[to_additive "An additive subgroup of an `AddGroup` inherits an `AddGroup` structure."]
+instance (priority := 75) toGroup : Group H :=
+  Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
+    (fun _ _ => rfl) fun _ _ => rfl
+
+-- Prefer subclasses of `CommGroup` over subclasses of `SubgroupClass`.
+/-- A subgroup of a `CommGroup` is a `CommGroup`. -/
+@[to_additive "An additive subgroup of an `AddCommGroup` is an `AddCommGroup`."]
+instance (priority := 75) toCommGroup {G : Type*} [CommGroup G] [SetLike S G] [SubgroupClass S G] :
+    CommGroup H :=
+  Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
+    (fun _ _ => rfl) fun _ _ => rfl
+
+/-- The natural group hom from a subgroup of group `G` to `G`. -/
+@[to_additive (attr := coe)
+  "The natural group hom from an additive subgroup of `AddGroup` `G` to `G`."]
+protected def subtype : H →* G where
+  toFun := ((↑) : H → G); map_one' := rfl; map_mul' := fun _ _ => rfl
+
+@[to_additive (attr := simp)]
+theorem coeSubtype : (SubgroupClass.subtype H : H → G) = ((↑) : H → G) := by
+  rfl
+
+variable {H}
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n :=
+  rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n :=
+  rfl
+
+/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
+@[to_additive "The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`."]
+def inclusion {H K : S} (h : H ≤ K) : H →* K :=
+  MonoidHom.mk' (fun x => ⟨x, h x.prop⟩) fun _ _=> rfl
+
+@[to_additive (attr := simp)]
+theorem inclusion_self (x : H) : inclusion le_rfl x = x := by
+  cases x
+  rfl
+
+@[to_additive (attr := simp)]
+theorem inclusion_mk {h : H ≤ K} (x : G) (hx : x ∈ H) : inclusion h ⟨x, hx⟩ = ⟨x, h hx⟩ :=
+  rfl
+
+@[to_additive]
+theorem inclusion_right (h : H ≤ K) (x : K) (hx : (x : G) ∈ H) : inclusion h ⟨x, hx⟩ = x := by
+  cases x
+  rfl
+
+@[simp]
+theorem inclusion_inclusion {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : H) :
+    inclusion hKL (inclusion hHK x) = inclusion (hHK.trans hKL) x := by
+  cases x
+  rfl
+
+@[to_additive (attr := simp)]
+theorem coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
+  cases a
+  simp only [inclusion, MonoidHom.mk'_apply]
+
+@[to_additive (attr := simp)]
+theorem subtype_comp_inclusion {H K : S} (hH : H ≤ K) :
+    (SubgroupClass.subtype K).comp (inclusion hH) = SubgroupClass.subtype H := by
+  ext
+  simp only [MonoidHom.comp_apply, coeSubtype, coe_inclusion]
+
+end SubgroupClass
+
+end SubgroupClass
+
+/-- A subgroup of a group `G` is a subset containing 1, closed under multiplication
+and closed under multiplicative inverse. -/
+structure Subgroup (G : Type*) [Group G] extends Submonoid G where
+  /-- `G` is closed under inverses -/
+  inv_mem' {x} : x ∈ carrier → x⁻¹ ∈ carrier
+
+/-- An additive subgroup of an additive group `G` is a subset containing 0, closed
+under addition and additive inverse. -/
+structure AddSubgroup (G : Type*) [AddGroup G] extends AddSubmonoid G where
+  /-- `G` is closed under negation -/
+  neg_mem' {x} : x ∈ carrier → -x ∈ carrier
+
+attribute [to_additive] Subgroup
+
+-- Porting note: Removed, translation already exists
+-- attribute [to_additive AddSubgroup.toAddSubmonoid] Subgroup.toSubmonoid
+
+/-- Reinterpret a `Subgroup` as a `Submonoid`. -/
+add_decl_doc Subgroup.toSubmonoid
+
+/-- Reinterpret an `AddSubgroup` as an `AddSubmonoid`. -/
+add_decl_doc AddSubgroup.toAddSubmonoid
+
+namespace Subgroup
+
+@[to_additive]
+instance : SetLike (Subgroup G) G where
+  coe s := s.carrier
+  coe_injective' p q h := by
+    obtain ⟨⟨⟨hp,_⟩,_⟩,_⟩ := p
+    obtain ⟨⟨⟨hq,_⟩,_⟩,_⟩ := q
+    congr
+
+-- Porting note: Below can probably be written more uniformly
+@[to_additive]
+instance : SubgroupClass (Subgroup G) G where
+  inv_mem := Subgroup.inv_mem' _
+  one_mem _ := (Subgroup.toSubmonoid _).one_mem'
+  mul_mem := (Subgroup.toSubmonoid _).mul_mem'
+
+@[to_additive (attr := simp, nolint simpNF)] -- Porting note (#10675): dsimp can not prove this
+theorem mem_carrier {s : Subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s :=
+  Iff.rfl
+
+@[to_additive (attr := simp)]
+theorem mem_mk {s : Set G} {x : G} (h_one) (h_mul) (h_inv) :
+    x ∈ mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ↔ x ∈ s :=
+  Iff.rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_set_mk {s : Set G} (h_one) (h_mul) (h_inv) :
+    (mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv : Set G) = s :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk_le_mk {s t : Set G} (h_one) (h_mul) (h_inv) (h_one') (h_mul') (h_inv') :
+    mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ≤ mk ⟨⟨t, h_one'⟩, h_mul'⟩ h_inv' ↔ s ⊆ t :=
+  Iff.rfl
+
+initialize_simps_projections Subgroup (carrier → coe)
+initialize_simps_projections AddSubgroup (carrier → coe)
+
+@[to_additive (attr := simp)]
+theorem coe_toSubmonoid (K : Subgroup G) : (K.toSubmonoid : Set G) = K :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mem_toSubmonoid (K : Subgroup G) (x : G) : x ∈ K.toSubmonoid ↔ x ∈ K :=
+  Iff.rfl
+
+@[to_additive]
+theorem toSubmonoid_injective : Function.Injective (toSubmonoid : Subgroup G → Submonoid G) :=
+  -- fun p q h => SetLike.ext'_iff.2 (show _ from SetLike.ext'_iff.1 h)
+  fun p q h => by
+    have := SetLike.ext'_iff.1 h
+    rw [coe_toSubmonoid, coe_toSubmonoid] at this
+    exact SetLike.ext'_iff.2 this
+
+@[to_additive (attr := simp)]
+theorem toSubmonoid_eq {p q : Subgroup G} : p.toSubmonoid = q.toSubmonoid ↔ p = q :=
+  toSubmonoid_injective.eq_iff
+
+@[to_additive (attr := mono)]
+theorem toSubmonoid_strictMono : StrictMono (toSubmonoid : Subgroup G → Submonoid G) := fun _ _ =>
+  id
+
+@[to_additive (attr := mono)]
+theorem toSubmonoid_mono : Monotone (toSubmonoid : Subgroup G → Submonoid G) :=
+  toSubmonoid_strictMono.monotone
+
+@[to_additive (attr := simp)]
+theorem toSubmonoid_le {p q : Subgroup G} : p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q :=
+  Iff.rfl
+
+@[to_additive (attr := simp)]
+lemma coe_nonempty (s : Subgroup G) : (s : Set G).Nonempty := ⟨1, one_mem _⟩
+
+end Subgroup
+
+namespace Subgroup
+
+variable (H K : Subgroup G)
+
+/-- Copy of a subgroup with a new `carrier` equal to the old one. Useful to fix definitional
+equalities. -/
+@[to_additive
+      "Copy of an additive subgroup with a new `carrier` equal to the old one.
+      Useful to fix definitional equalities"]
+protected def copy (K : Subgroup G) (s : Set G) (hs : s = K) : Subgroup G where
+  carrier := s
+  one_mem' := hs.symm ▸ K.one_mem'
+  mul_mem' := hs.symm ▸ K.mul_mem'
+  inv_mem' hx := by simpa [hs] using hx -- Porting note: `▸` didn't work here
+
+@[to_additive (attr := simp)]
+theorem coe_copy (K : Subgroup G) (s : Set G) (hs : s = ↑K) : (K.copy s hs : Set G) = s :=
+  rfl
+
+@[to_additive]
+theorem copy_eq (K : Subgroup G) (s : Set G) (hs : s = ↑K) : K.copy s hs = K :=
+  SetLike.coe_injective hs
+
+/-- Two subgroups are equal if they have the same elements. -/
+@[to_additive (attr := ext) "Two `AddSubgroup`s are equal if they have the same elements."]
+theorem ext {H K : Subgroup G} (h : ∀ x, x ∈ H ↔ x ∈ K) : H = K :=
+  SetLike.ext h
+
+/-- A subgroup contains the group's 1. -/
+@[to_additive "An `AddSubgroup` contains the group's 0."]
+protected theorem one_mem : (1 : G) ∈ H :=
+  one_mem _
+
+/-- A subgroup is closed under multiplication. -/
+@[to_additive "An `AddSubgroup` is closed under addition."]
+protected theorem mul_mem {x y : G} : x ∈ H → y ∈ H → x * y ∈ H :=
+  mul_mem
+
+/-- A subgroup is closed under inverse. -/
+@[to_additive "An `AddSubgroup` is closed under inverse."]
+protected theorem inv_mem {x : G} : x ∈ H → x⁻¹ ∈ H :=
+  inv_mem
+
+/-- A subgroup is closed under division. -/
+@[to_additive "An `AddSubgroup` is closed under subtraction."]
+protected theorem div_mem {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H :=
+  div_mem hx hy
+
+@[to_additive]
+protected theorem inv_mem_iff {x : G} : x⁻¹ ∈ H ↔ x ∈ H :=
+  inv_mem_iff
+
+@[to_additive]
+protected theorem exists_inv_mem_iff_exists_mem (K : Subgroup G) {P : G → Prop} :
+    (∃ x : G, x ∈ K ∧ P x⁻¹) ↔ ∃ x ∈ K, P x :=
+  exists_inv_mem_iff_exists_mem
+
+@[to_additive]
+protected theorem mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H :=
+  mul_mem_cancel_right h
+
+@[to_additive]
+protected theorem mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H :=
+  mul_mem_cancel_left h
+
+@[to_additive]
+protected theorem pow_mem {x : G} (hx : x ∈ K) : ∀ n : ℕ, x ^ n ∈ K :=
+  pow_mem hx
+
+@[to_additive]
+protected theorem zpow_mem {x : G} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K :=
+  zpow_mem hx
+
+/-- Construct a subgroup from a nonempty set that is closed under division. -/
+@[to_additive "Construct a subgroup from a nonempty set that is closed under subtraction"]
+def ofDiv (s : Set G) (hsn : s.Nonempty) (hs : ∀ᵉ (x ∈ s) (y ∈ s), x * y⁻¹ ∈ s) :
+    Subgroup G :=
+  have one_mem : (1 : G) ∈ s := by
+    let ⟨x, hx⟩ := hsn
+    simpa using hs x hx x hx
+  have inv_mem : ∀ x, x ∈ s → x⁻¹ ∈ s := fun x hx => by simpa using hs 1 one_mem x hx
+  { carrier := s
+    one_mem' := one_mem
+    inv_mem' := inv_mem _
+    mul_mem' := fun hx hy => by simpa using hs _ hx _ (inv_mem _ hy) }
+
+/-- A subgroup of a group inherits a multiplication. -/
+@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an addition."]
+instance mul : Mul H :=
+  H.toSubmonoid.mul
+
+/-- A subgroup of a group inherits a 1. -/
+@[to_additive "An `AddSubgroup` of an `AddGroup` inherits a zero."]
+instance one : One H :=
+  H.toSubmonoid.one
+
+/-- A subgroup of a group inherits an inverse. -/
+@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an inverse."]
+instance inv : Inv H :=
+  ⟨fun a => ⟨a⁻¹, H.inv_mem a.2⟩⟩
+
+/-- A subgroup of a group inherits a division -/
+@[to_additive "An `AddSubgroup` of an `AddGroup` inherits a subtraction."]
+instance div : Div H :=
+  ⟨fun a b => ⟨a / b, H.div_mem a.2 b.2⟩⟩
+
+/-- An `AddSubgroup` of an `AddGroup` inherits a natural scaling. -/
+instance _root_.AddSubgroup.nsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℕ H :=
+  ⟨fun n a => ⟨n • a, H.nsmul_mem a.2 n⟩⟩
+
+/-- A subgroup of a group inherits a natural power -/
+@[to_additive existing]
+protected instance npow : Pow H ℕ :=
+  ⟨fun a n => ⟨a ^ n, H.pow_mem a.2 n⟩⟩
+
+/-- An `AddSubgroup` of an `AddGroup` inherits an integer scaling. -/
+instance _root_.AddSubgroup.zsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℤ H :=
+  ⟨fun n a => ⟨n • a, H.zsmul_mem a.2 n⟩⟩
+
+/-- A subgroup of a group inherits an integer power -/
+@[to_additive existing]
+instance zpow : Pow H ℤ :=
+  ⟨fun a n => ⟨a ^ n, H.zpow_mem a.2 n⟩⟩
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_mul (x y : H) : (↑(x * y) : G) = ↑x * ↑y :=
+  rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_one : ((1 : H) : G) = 1 :=
+  rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_inv (x : H) : ↑(x⁻¹ : H) = (x⁻¹ : G) :=
+  rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_div (x y : H) : (↑(x / y) : G) = ↑x / ↑y :=
+  rfl
+
+-- Porting note: removed simp, theorem has variable as head symbol
+@[to_additive (attr := norm_cast)]
+theorem coe_mk (x : G) (hx : x ∈ H) : ((⟨x, hx⟩ : H) : G) = x :=
+  rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n :=
+  rfl
+
+@[to_additive (attr := norm_cast)] -- Porting note (#10685): dsimp can prove this
+theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk_eq_one {g : G} {h} : (⟨g, h⟩ : H) = 1 ↔ g = 1 := Submonoid.mk_eq_one ..
+
+/-- A subgroup of a group inherits a group structure. -/
+@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an `AddGroup` structure."]
+instance toGroup {G : Type*} [Group G] (H : Subgroup G) : Group H :=
+  Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
+    (fun _ _ => rfl) fun _ _ => rfl
+
+/-- A subgroup of a `CommGroup` is a `CommGroup`. -/
+@[to_additive "An `AddSubgroup` of an `AddCommGroup` is an `AddCommGroup`."]
+instance toCommGroup {G : Type*} [CommGroup G] (H : Subgroup G) : CommGroup H :=
+  Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
+    (fun _ _ => rfl) fun _ _ => rfl
+
+/-- The natural group hom from a subgroup of group `G` to `G`. -/
+@[to_additive "The natural group hom from an `AddSubgroup` of `AddGroup` `G` to `G`."]
+protected def subtype : H →* G where
+  toFun := ((↑) : H → G); map_one' := rfl; map_mul' _ _ := rfl
+
+@[to_additive (attr := simp)]
+theorem coeSubtype : ⇑ H.subtype = ((↑) : H → G) :=
+  rfl
+
+@[to_additive]
+theorem subtype_injective : Function.Injective (Subgroup.subtype H) :=
+  Subtype.coe_injective
+
+/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
+@[to_additive "The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`."]
+def inclusion {H K : Subgroup G} (h : H ≤ K) : H →* K :=
+  MonoidHom.mk' (fun x => ⟨x, h x.2⟩) fun _ _ => rfl
+
+@[to_additive (attr := simp)]
+theorem coe_inclusion {H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
+  cases a
+  simp only [inclusion, coe_mk, MonoidHom.mk'_apply]
+
+@[to_additive]
+theorem inclusion_injective {H K : Subgroup G} (h : H ≤ K) : Function.Injective <| inclusion h :=
+  Set.inclusion_injective h
+
+@[to_additive (attr := simp)]
+lemma inclusion_inj {H K : Subgroup G} (h : H ≤ K) {x y : H} :
+    inclusion h x = inclusion h y ↔ x = y :=
+  (inclusion_injective h).eq_iff
+
+@[to_additive (attr := simp)]
+theorem subtype_comp_inclusion {H K : Subgroup G} (hH : H ≤ K) :
+    K.subtype.comp (inclusion hH) = H.subtype :=
+  rfl
+
+variable {k : Set G}
+
+open Set
+
+variable {N : Type*} [Group N] {P : Type*} [Group P]
+
+/-- A subgroup is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` -/
+structure Normal : Prop where
+  /-- `N` is closed under conjugation -/
+  conj_mem : ∀ n, n ∈ H → ∀ g : G, g * n * g⁻¹ ∈ H
+
+attribute [class] Normal
+
+end Subgroup
+
+namespace AddSubgroup
+
+/-- An AddSubgroup is normal if whenever `n ∈ H`, then `g + n - g ∈ H` for every `g : G` -/
+structure Normal (H : AddSubgroup A) : Prop where
+  /-- `N` is closed under additive conjugation -/
+  conj_mem : ∀ n, n ∈ H → ∀ g : A, g + n + -g ∈ H
+
+attribute [to_additive] Subgroup.Normal
+
+attribute [class] Normal
+
+end AddSubgroup
+
+namespace Subgroup
+
+variable {H K : Subgroup G}
+
+@[to_additive]
+instance (priority := 100) normal_of_comm {G : Type*} [CommGroup G] (H : Subgroup G) : H.Normal :=
+  ⟨by simp [mul_comm, mul_left_comm]⟩
+
+namespace Normal
+
+@[to_additive]
+theorem conj_mem' (nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) :
+    g⁻¹ * n * g ∈ H := by
+  convert nH.conj_mem n hn g⁻¹
+  rw [inv_inv]
+
+@[to_additive]
+theorem mem_comm (nH : H.Normal) {a b : G} (h : a * b ∈ H) : b * a ∈ H := by
+  have : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ H := nH.conj_mem (a * b) h a⁻¹
+  -- Porting note: Previous code was:
+  -- simpa
+  simp_all only [inv_mul_cancel_left, inv_inv]
+
+@[to_additive]
+theorem mem_comm_iff (nH : H.Normal) {a b : G} : a * b ∈ H ↔ b * a ∈ H :=
+  ⟨nH.mem_comm, nH.mem_comm⟩
+
+end Normal
+
+end Subgroup
+
+namespace Subgroup
+
+variable (H : Subgroup G) {K : Subgroup G}
+
+section Normalizer
+
+/-- The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal. -/
+@[to_additive "The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal."]
+def normalizer : Subgroup G where
+  carrier := { g : G | ∀ n, n ∈ H ↔ g * n * g⁻¹ ∈ H }
+  one_mem' := by simp
+  mul_mem' {a b} (ha : ∀ n, n ∈ H ↔ a * n * a⁻¹ ∈ H) (hb : ∀ n, n ∈ H ↔ b * n * b⁻¹ ∈ H) n := by
+    rw [hb, ha]
+    simp only [mul_assoc, mul_inv_rev]
+  inv_mem' {a} (ha : ∀ n, n ∈ H ↔ a * n * a⁻¹ ∈ H) n := by
+    rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
+    simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]
+
+-- variant for sets.
+-- TODO should this replace `normalizer`?
+/-- The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy `g*S*g⁻¹=S` -/
+@[to_additive
+      "The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy
+      `g+S-g=S`."]
+def setNormalizer (S : Set G) : Subgroup G where
+  carrier := { g : G | ∀ n, n ∈ S ↔ g * n * g⁻¹ ∈ S }
+  one_mem' := by simp
+  mul_mem' {a b} (ha : ∀ n, n ∈ S ↔ a * n * a⁻¹ ∈ S) (hb : ∀ n, n ∈ S ↔ b * n * b⁻¹ ∈ S) n := by
+    rw [hb, ha]
+    simp only [mul_assoc, mul_inv_rev]
+  inv_mem' {a} (ha : ∀ n, n ∈ S ↔ a * n * a⁻¹ ∈ S) n := by
+    rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
+    simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]
+
+variable {H}
+
+@[to_additive]
+theorem mem_normalizer_iff {g : G} : g ∈ H.normalizer ↔ ∀ h, h ∈ H ↔ g * h * g⁻¹ ∈ H :=
+  Iff.rfl
+
+@[to_additive]
+theorem mem_normalizer_iff'' {g : G} : g ∈ H.normalizer ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H := by
+  rw [← inv_mem_iff (x := g), mem_normalizer_iff, inv_inv]
+
+@[to_additive]
+theorem mem_normalizer_iff' {g : G} : g ∈ H.normalizer ↔ ∀ n, n * g ∈ H ↔ g * n ∈ H :=
+  ⟨fun h n => by rw [h, mul_assoc, mul_inv_cancel_right], fun h n => by
+    rw [mul_assoc, ← h, inv_mul_cancel_right]⟩
+
+@[to_additive]
+theorem le_normalizer : H ≤ normalizer H := fun x xH n => by
+  rw [H.mul_mem_cancel_right (H.inv_mem xH), H.mul_mem_cancel_left xH]
+
+end Normalizer
+
+/-- Commutativity of a subgroup -/
+structure IsCommutative : Prop where
+  /-- `*` is commutative on `H` -/
+  is_comm : Std.Commutative (α := H) (· * ·)
+
+attribute [class] IsCommutative
+
+/-- Commutativity of an additive subgroup -/
+structure _root_.AddSubgroup.IsCommutative (H : AddSubgroup A) : Prop where
+  /-- `+` is commutative on `H` -/
+  is_comm : Std.Commutative (α := H) (· + ·)
+
+attribute [to_additive] Subgroup.IsCommutative
+
+attribute [class] AddSubgroup.IsCommutative
+
+/-- A commutative subgroup is commutative. -/
+@[to_additive "A commutative subgroup is commutative."]
+instance IsCommutative.commGroup [h : H.IsCommutative] : CommGroup H :=
+  { H.toGroup with mul_comm := h.is_comm.comm }
+
+/-- A subgroup of a commutative group is commutative. -/
+@[to_additive "A subgroup of a commutative group is commutative."]
+instance commGroup_isCommutative {G : Type*} [CommGroup G] (H : Subgroup G) : H.IsCommutative :=
+  ⟨CommMagma.to_isCommutative⟩
+
+@[to_additive]
+lemma mul_comm_of_mem_isCommutative [H.IsCommutative] {a b : G} (ha : a ∈ H) (hb : b ∈ H) :
+    a * b = b * a := by
+  simpa only [MulMemClass.mk_mul_mk, Subtype.mk.injEq] using mul_comm (⟨a, ha⟩ : H) (⟨b, hb⟩ : H)
+
+end Subgroup
diff --git a/Mathlib/Algebra/Group/Subgroup/Order.lean b/Mathlib/Algebra/Group/Subgroup/Order.lean
index 7e9cd2eefee49..6229466df62b8 100644
--- a/Mathlib/Algebra/Group/Subgroup/Order.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Order.lean
@@ -5,6 +5,7 @@ Authors: Damiano Testa, Ruben Van de Velde
 -/
 import Mathlib.Order.Atoms
 import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subsemigroup.Operations
 import Mathlib.Algebra.Order.Group.InjSurj
 import Mathlib.Algebra.Order.Group.Unbundled.Abs
 
diff --git a/Mathlib/Algebra/Group/Submonoid/Defs.lean b/Mathlib/Algebra/Group/Submonoid/Defs.lean
index d1a62b639d86a..3bb3c3e2e3ea9 100644
--- a/Mathlib/Algebra/Group/Submonoid/Defs.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Defs.lean
@@ -295,3 +295,158 @@ theorem eq_of_eqOn_topM {f g : M →* N} (h : Set.EqOn f g (⊤ : Submonoid M))
 end MonoidHom
 
 end NonAssoc
+
+namespace OneMemClass
+
+variable {A M₁ : Type*} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A)
+
+/-- A submonoid of a monoid inherits a 1. -/
+@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits a zero."]
+instance one : One S' :=
+  ⟨⟨1, OneMemClass.one_mem S'⟩⟩
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_one : ((1 : S') : M₁) = 1 :=
+  rfl
+
+variable {S'}
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_eq_one {x : S'} : (↑x : M₁) = 1 ↔ x = 1 :=
+  (Subtype.ext_iff.symm : (x : M₁) = (1 : S') ↔ x = 1)
+
+variable (S')
+
+@[to_additive]
+theorem one_def : (1 : S') = ⟨1, OneMemClass.one_mem S'⟩ :=
+  rfl
+
+end OneMemClass
+
+variable {A : Type*} [MulOneClass M] [SetLike A M] [hA : SubmonoidClass A M] (S' : A)
+
+/-- An `AddSubmonoid` of an `AddMonoid` inherits a scalar multiplication. -/
+instance AddSubmonoidClass.nSMul {M} [AddMonoid M] {A : Type*} [SetLike A M]
+    [AddSubmonoidClass A M] (S : A) : SMul ℕ S :=
+  ⟨fun n a => ⟨n • a.1, nsmul_mem a.2 n⟩⟩
+
+namespace SubmonoidClass
+
+/-- A submonoid of a monoid inherits a power operator. -/
+instance nPow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow S ℕ :=
+  ⟨fun a n => ⟨a.1 ^ n, pow_mem a.2 n⟩⟩
+
+attribute [to_additive existing nSMul] nPow
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_pow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : S)
+    (n : ℕ) : ↑(x ^ n) = (x : M) ^ n :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk_pow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : M)
+    (hx : x ∈ S) (n : ℕ) : (⟨x, hx⟩ : S) ^ n = ⟨x ^ n, pow_mem hx n⟩ :=
+  rfl
+
+-- Prefer subclasses of `Monoid` over subclasses of `SubmonoidClass`.
+/-- A submonoid of a unital magma inherits a unital magma structure. -/
+@[to_additive
+      "An `AddSubmonoid` of a unital additive magma inherits a unital additive magma structure."]
+instance (priority := 75) toMulOneClass {M : Type*} [MulOneClass M] {A : Type*} [SetLike A M]
+    [SubmonoidClass A M] (S : A) : MulOneClass S :=
+    Subtype.coe_injective.mulOneClass (↑) rfl (fun _ _ => rfl)
+
+-- Prefer subclasses of `Monoid` over subclasses of `SubmonoidClass`.
+/-- A submonoid of a monoid inherits a monoid structure. -/
+@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure."]
+instance (priority := 75) toMonoid {M : Type*} [Monoid M] {A : Type*} [SetLike A M]
+    [SubmonoidClass A M] (S : A) : Monoid S :=
+  Subtype.coe_injective.monoid (↑) rfl (fun _ _ => rfl) (fun _ _ => rfl)
+
+-- Prefer subclasses of `Monoid` over subclasses of `SubmonoidClass`.
+/-- A submonoid of a `CommMonoid` is a `CommMonoid`. -/
+@[to_additive "An `AddSubmonoid` of an `AddCommMonoid` is an `AddCommMonoid`."]
+instance (priority := 75) toCommMonoid {M} [CommMonoid M] {A : Type*} [SetLike A M]
+    [SubmonoidClass A M] (S : A) : CommMonoid S :=
+  Subtype.coe_injective.commMonoid (↑) rfl (fun _ _ => rfl) fun _ _ => rfl
+
+/-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/
+@[to_additive "The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`."]
+def subtype : S' →* M where
+  toFun := Subtype.val; map_one' := rfl; map_mul' _ _ := by simp
+
+@[to_additive (attr := simp)]
+theorem coe_subtype : (SubmonoidClass.subtype S' : S' → M) = Subtype.val :=
+  rfl
+
+end SubmonoidClass
+
+namespace Submonoid
+
+variable {M : Type*} [MulOneClass M] (S : Submonoid M)
+
+/-- A submonoid of a monoid inherits a multiplication. -/
+@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits an addition."]
+instance mul : Mul S :=
+  ⟨fun a b => ⟨a.1 * b.1, S.mul_mem a.2 b.2⟩⟩
+
+/-- A submonoid of a monoid inherits a 1. -/
+@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits a zero."]
+instance one : One S :=
+  ⟨⟨_, S.one_mem⟩⟩
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_mul (x y : S) : (↑(x * y) : M) = ↑x * ↑y :=
+  rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_one : ((1 : S) : M) = 1 :=
+  rfl
+
+@[to_additive (attr := simp)]
+lemma mk_eq_one {a : M} {ha} : (⟨a, ha⟩ : S) = 1 ↔ a = 1 := by simp [← SetLike.coe_eq_coe]
+
+@[to_additive (attr := simp)]
+theorem mk_mul_mk (x y : M) (hx : x ∈ S) (hy : y ∈ S) :
+    (⟨x, hx⟩ : S) * ⟨y, hy⟩ = ⟨x * y, S.mul_mem hx hy⟩ :=
+  rfl
+
+@[to_additive]
+theorem mul_def (x y : S) : x * y = ⟨x * y, S.mul_mem x.2 y.2⟩ :=
+  rfl
+
+@[to_additive]
+theorem one_def : (1 : S) = ⟨1, S.one_mem⟩ :=
+  rfl
+
+/-- A submonoid of a unital magma inherits a unital magma structure. -/
+@[to_additive
+      "An `AddSubmonoid` of a unital additive magma inherits a unital additive magma structure."]
+instance toMulOneClass {M : Type*} [MulOneClass M] (S : Submonoid M) : MulOneClass S :=
+  Subtype.coe_injective.mulOneClass (↑) rfl fun _ _ => rfl
+
+@[to_additive]
+protected theorem pow_mem {M : Type*} [Monoid M] (S : Submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) :
+    x ^ n ∈ S :=
+  pow_mem hx n
+
+/-- A submonoid of a monoid inherits a monoid structure. -/
+@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure."]
+instance toMonoid {M : Type*} [Monoid M] (S : Submonoid M) : Monoid S :=
+  Subtype.coe_injective.monoid (↑) rfl (fun _ _ => rfl) fun _ _ => rfl
+
+/-- A submonoid of a `CommMonoid` is a `CommMonoid`. -/
+@[to_additive "An `AddSubmonoid` of an `AddCommMonoid` is an `AddCommMonoid`."]
+instance toCommMonoid {M} [CommMonoid M] (S : Submonoid M) : CommMonoid S :=
+  Subtype.coe_injective.commMonoid (↑) rfl (fun _ _ => rfl) fun _ _ => rfl
+
+/-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/
+@[to_additive "The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`."]
+def subtype : S →* M where
+  toFun := Subtype.val; map_one' := rfl; map_mul' _ _ := by simp
+
+@[to_additive (attr := simp)]
+theorem coe_subtype : ⇑S.subtype = Subtype.val :=
+  rfl
+
+end Submonoid
diff --git a/Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean b/Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean
index 15e285f0d6b07..aa2205e477ee9 100644
--- a/Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean
+++ b/Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
-import Mathlib.Algebra.Group.Submonoid.Operations
+import Mathlib.Algebra.Group.Submonoid.Defs
 import Mathlib.Algebra.GroupWithZero.Action.End
 
 /-!
diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean
index ee672456df581..de4a43436a3bd 100644
--- a/Mathlib/Algebra/Group/Submonoid/Operations.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Operations.lean
@@ -6,8 +6,8 @@ Amelia Livingston, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Action.Faithful
 import Mathlib.Algebra.Group.Nat
+import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Submonoid.Basic
-import Mathlib.Algebra.Group.Subsemigroup.Operations
 
 /-!
 # Operations on `Submonoid`s
@@ -407,158 +407,7 @@ theorem comap_strictMono_of_surjective : StrictMono (comap f) :=
 
 end GaloisInsertion
 
-end Submonoid
-
-namespace OneMemClass
-
-variable {A M₁ : Type*} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A)
-
-/-- A submonoid of a monoid inherits a 1. -/
-@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits a zero."]
-instance one : One S' :=
-  ⟨⟨1, OneMemClass.one_mem S'⟩⟩
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_one : ((1 : S') : M₁) = 1 :=
-  rfl
-
-variable {S'}
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_eq_one {x : S'} : (↑x : M₁) = 1 ↔ x = 1 :=
-  (Subtype.ext_iff.symm : (x : M₁) = (1 : S') ↔ x = 1)
-
-variable (S')
-
-@[to_additive]
-theorem one_def : (1 : S') = ⟨1, OneMemClass.one_mem S'⟩ :=
-  rfl
-
-end OneMemClass
-
-variable {A : Type*} [SetLike A M] [hA : SubmonoidClass A M] (S' : A)
-
-/-- An `AddSubmonoid` of an `AddMonoid` inherits a scalar multiplication. -/
-instance AddSubmonoidClass.nSMul {M} [AddMonoid M] {A : Type*} [SetLike A M]
-    [AddSubmonoidClass A M] (S : A) : SMul ℕ S :=
-  ⟨fun n a => ⟨n • a.1, nsmul_mem a.2 n⟩⟩
-
-namespace SubmonoidClass
-
-/-- A submonoid of a monoid inherits a power operator. -/
-instance nPow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow S ℕ :=
-  ⟨fun a n => ⟨a.1 ^ n, pow_mem a.2 n⟩⟩
-
-attribute [to_additive existing nSMul] nPow
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_pow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : S)
-    (n : ℕ) : ↑(x ^ n) = (x : M) ^ n :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk_pow {M} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] {S : A} (x : M)
-    (hx : x ∈ S) (n : ℕ) : (⟨x, hx⟩ : S) ^ n = ⟨x ^ n, pow_mem hx n⟩ :=
-  rfl
-
--- Prefer subclasses of `Monoid` over subclasses of `SubmonoidClass`.
-/-- A submonoid of a unital magma inherits a unital magma structure. -/
-@[to_additive
-      "An `AddSubmonoid` of a unital additive magma inherits a unital additive magma structure."]
-instance (priority := 75) toMulOneClass {M : Type*} [MulOneClass M] {A : Type*} [SetLike A M]
-    [SubmonoidClass A M] (S : A) : MulOneClass S :=
-    Subtype.coe_injective.mulOneClass (↑) rfl (fun _ _ => rfl)
-
--- Prefer subclasses of `Monoid` over subclasses of `SubmonoidClass`.
-/-- A submonoid of a monoid inherits a monoid structure. -/
-@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure."]
-instance (priority := 75) toMonoid {M : Type*} [Monoid M] {A : Type*} [SetLike A M]
-    [SubmonoidClass A M] (S : A) : Monoid S :=
-  Subtype.coe_injective.monoid (↑) rfl (fun _ _ => rfl) (fun _ _ => rfl)
-
--- Prefer subclasses of `Monoid` over subclasses of `SubmonoidClass`.
-/-- A submonoid of a `CommMonoid` is a `CommMonoid`. -/
-@[to_additive "An `AddSubmonoid` of an `AddCommMonoid` is an `AddCommMonoid`."]
-instance (priority := 75) toCommMonoid {M} [CommMonoid M] {A : Type*} [SetLike A M]
-    [SubmonoidClass A M] (S : A) : CommMonoid S :=
-  Subtype.coe_injective.commMonoid (↑) rfl (fun _ _ => rfl) fun _ _ => rfl
-
-/-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/
-@[to_additive "The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`."]
-def subtype : S' →* M where
-  toFun := Subtype.val; map_one' := rfl; map_mul' _ _ := by simp
-
-@[to_additive (attr := simp)]
-theorem coe_subtype : (SubmonoidClass.subtype S' : S' → M) = Subtype.val :=
-  rfl
-
-end SubmonoidClass
-
-namespace Submonoid
-
-/-- A submonoid of a monoid inherits a multiplication. -/
-@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits an addition."]
-instance mul : Mul S :=
-  ⟨fun a b => ⟨a.1 * b.1, S.mul_mem a.2 b.2⟩⟩
-
-/-- A submonoid of a monoid inherits a 1. -/
-@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits a zero."]
-instance one : One S :=
-  ⟨⟨_, S.one_mem⟩⟩
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_mul (x y : S) : (↑(x * y) : M) = ↑x * ↑y :=
-  rfl
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_one : ((1 : S) : M) = 1 :=
-  rfl
-
-@[to_additive (attr := simp)]
-lemma mk_eq_one {a : M} {ha} : (⟨a, ha⟩ : S) = 1 ↔ a = 1 := by simp [← SetLike.coe_eq_coe]
-
-@[to_additive (attr := simp)]
-theorem mk_mul_mk (x y : M) (hx : x ∈ S) (hy : y ∈ S) :
-    (⟨x, hx⟩ : S) * ⟨y, hy⟩ = ⟨x * y, S.mul_mem hx hy⟩ :=
-  rfl
-
-@[to_additive]
-theorem mul_def (x y : S) : x * y = ⟨x * y, S.mul_mem x.2 y.2⟩ :=
-  rfl
-
-@[to_additive]
-theorem one_def : (1 : S) = ⟨1, S.one_mem⟩ :=
-  rfl
-
-/-- A submonoid of a unital magma inherits a unital magma structure. -/
-@[to_additive
-      "An `AddSubmonoid` of a unital additive magma inherits a unital additive magma structure."]
-instance toMulOneClass {M : Type*} [MulOneClass M] (S : Submonoid M) : MulOneClass S :=
-  Subtype.coe_injective.mulOneClass (↑) rfl fun _ _ => rfl
-
-@[to_additive]
-protected theorem pow_mem {M : Type*} [Monoid M] (S : Submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) :
-    x ^ n ∈ S :=
-  pow_mem hx n
-
-/-- A submonoid of a monoid inherits a monoid structure. -/
-@[to_additive "An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure."]
-instance toMonoid {M : Type*} [Monoid M] (S : Submonoid M) : Monoid S :=
-  Subtype.coe_injective.monoid (↑) rfl (fun _ _ => rfl) fun _ _ => rfl
-
-/-- A submonoid of a `CommMonoid` is a `CommMonoid`. -/
-@[to_additive "An `AddSubmonoid` of an `AddCommMonoid` is an `AddCommMonoid`."]
-instance toCommMonoid {M} [CommMonoid M] (S : Submonoid M) : CommMonoid S :=
-  Subtype.coe_injective.commMonoid (↑) rfl (fun _ _ => rfl) fun _ _ => rfl
-
-/-- The natural monoid hom from a submonoid of monoid `M` to `M`. -/
-@[to_additive "The natural monoid hom from an `AddSubmonoid` of `AddMonoid` `M` to `M`."]
-def subtype : S →* M where
-  toFun := Subtype.val; map_one' := rfl; map_mul' _ _ := by simp
-
-@[to_additive (attr := simp)]
-theorem coe_subtype : ⇑S.subtype = Subtype.val :=
-  rfl
+variable {M : Type*} [MulOneClass M] (S : Submonoid M)
 
 /-- The top submonoid is isomorphic to the monoid. -/
 @[to_additive (attr := simps) "The top additive submonoid is isomorphic to the additive monoid."]
diff --git a/Mathlib/Algebra/Group/Subsemigroup/Defs.lean b/Mathlib/Algebra/Group/Subsemigroup/Defs.lean
index aa0008eee16ba..99b1585fb36fb 100644
--- a/Mathlib/Algebra/Group/Subsemigroup/Defs.lean
+++ b/Mathlib/Algebra/Group/Subsemigroup/Defs.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzza
 Amelia Livingston, Yury Kudryashov, Yakov Pechersky
 -/
 import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Algebra.Group.InjSurj
 import Mathlib.Data.SetLike.Basic
 
 /-!
@@ -225,3 +226,52 @@ theorem eq_of_eqOn_top {f g : M →ₙ* N} (h : Set.EqOn f g (⊤ : Subsemigroup
 end MulHom
 
 end NonAssoc
+
+namespace MulMemClass
+
+variable {A : Type*} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A)
+
+-- lower priority so other instances are found first
+/-- A submagma of a magma inherits a multiplication. -/
+@[to_additive "An additive submagma of an additive magma inherits an addition."]
+instance (priority := 900) mul : Mul S' :=
+  ⟨fun a b => ⟨a.1 * b.1, mul_mem a.2 b.2⟩⟩
+
+-- lower priority so later simp lemmas are used first; to appease simp_nf
+@[to_additive (attr := simp low, norm_cast)]
+theorem coe_mul (x y : S') : (↑(x * y) : M) = ↑x * ↑y :=
+  rfl
+
+-- lower priority so later simp lemmas are used first; to appease simp_nf
+@[to_additive (attr := simp low)]
+theorem mk_mul_mk (x y : M) (hx : x ∈ S') (hy : y ∈ S') :
+    (⟨x, hx⟩ : S') * ⟨y, hy⟩ = ⟨x * y, mul_mem hx hy⟩ :=
+  rfl
+
+@[to_additive]
+theorem mul_def (x y : S') : x * y = ⟨x * y, mul_mem x.2 y.2⟩ :=
+  rfl
+
+/-- A subsemigroup of a semigroup inherits a semigroup structure. -/
+@[to_additive "An `AddSubsemigroup` of an `AddSemigroup` inherits an `AddSemigroup` structure."]
+instance toSemigroup {M : Type*} [Semigroup M] {A : Type*} [SetLike A M] [MulMemClass A M]
+    (S : A) : Semigroup S :=
+  Subtype.coe_injective.semigroup Subtype.val fun _ _ => rfl
+
+/-- A subsemigroup of a `CommSemigroup` is a `CommSemigroup`. -/
+@[to_additive "An `AddSubsemigroup` of an `AddCommSemigroup` is an `AddCommSemigroup`."]
+instance toCommSemigroup {M} [CommSemigroup M] {A : Type*} [SetLike A M] [MulMemClass A M]
+    (S : A) : CommSemigroup S :=
+  Subtype.coe_injective.commSemigroup Subtype.val fun _ _ => rfl
+
+/-- The natural semigroup hom from a subsemigroup of semigroup `M` to `M`. -/
+@[to_additive "The natural semigroup hom from an `AddSubsemigroup` of
+`AddSubsemigroup` `M` to `M`."]
+def subtype : S' →ₙ* M where
+  toFun := Subtype.val; map_mul' := fun _ _ => rfl
+
+@[to_additive (attr := simp)]
+theorem coe_subtype : (MulMemClass.subtype S' : S' → M) = Subtype.val :=
+  rfl
+
+end MulMemClass
diff --git a/Mathlib/Algebra/Group/Subsemigroup/Operations.lean b/Mathlib/Algebra/Group/Subsemigroup/Operations.lean
index 533dcfa812d35..5f2d5a377ff34 100644
--- a/Mathlib/Algebra/Group/Subsemigroup/Operations.lean
+++ b/Mathlib/Algebra/Group/Subsemigroup/Operations.lean
@@ -417,55 +417,6 @@ end GaloisInsertion
 
 end Subsemigroup
 
-namespace MulMemClass
-
-variable {A : Type*} [Mul M] [SetLike A M] [hA : MulMemClass A M] (S' : A)
-
--- lower priority so other instances are found first
-/-- A submagma of a magma inherits a multiplication. -/
-@[to_additive "An additive submagma of an additive magma inherits an addition."]
-instance (priority := 900) mul : Mul S' :=
-  ⟨fun a b => ⟨a.1 * b.1, mul_mem a.2 b.2⟩⟩
-
--- lower priority so later simp lemmas are used first; to appease simp_nf
-@[to_additive (attr := simp low, norm_cast)]
-theorem coe_mul (x y : S') : (↑(x * y) : M) = ↑x * ↑y :=
-  rfl
-
--- lower priority so later simp lemmas are used first; to appease simp_nf
-@[to_additive (attr := simp low)]
-theorem mk_mul_mk (x y : M) (hx : x ∈ S') (hy : y ∈ S') :
-    (⟨x, hx⟩ : S') * ⟨y, hy⟩ = ⟨x * y, mul_mem hx hy⟩ :=
-  rfl
-
-@[to_additive]
-theorem mul_def (x y : S') : x * y = ⟨x * y, mul_mem x.2 y.2⟩ :=
-  rfl
-
-/-- A subsemigroup of a semigroup inherits a semigroup structure. -/
-@[to_additive "An `AddSubsemigroup` of an `AddSemigroup` inherits an `AddSemigroup` structure."]
-instance toSemigroup {M : Type*} [Semigroup M] {A : Type*} [SetLike A M] [MulMemClass A M]
-    (S : A) : Semigroup S :=
-  Subtype.coe_injective.semigroup Subtype.val fun _ _ => rfl
-
-/-- A subsemigroup of a `CommSemigroup` is a `CommSemigroup`. -/
-@[to_additive "An `AddSubsemigroup` of an `AddCommSemigroup` is an `AddCommSemigroup`."]
-instance toCommSemigroup {M} [CommSemigroup M] {A : Type*} [SetLike A M] [MulMemClass A M]
-    (S : A) : CommSemigroup S :=
-  Subtype.coe_injective.commSemigroup Subtype.val fun _ _ => rfl
-
-/-- The natural semigroup hom from a subsemigroup of semigroup `M` to `M`. -/
-@[to_additive "The natural semigroup hom from an `AddSubsemigroup` of
-`AddSubsemigroup` `M` to `M`."]
-def subtype : S' →ₙ* M where
-  toFun := Subtype.val; map_mul' := fun _ _ => rfl
-
-@[to_additive (attr := simp)]
-theorem coe_subtype : (MulMemClass.subtype S' : S' → M) = Subtype.val :=
-  rfl
-
-end MulMemClass
-
 namespace Subsemigroup
 
 variable [Mul M] [Mul N] [Mul P] (S : Subsemigroup M)
diff --git a/Mathlib/Algebra/MonoidAlgebra/Degree.lean b/Mathlib/Algebra/MonoidAlgebra/Degree.lean
index 616114af6f493..16c11daef0708 100644
--- a/Mathlib/Algebra/MonoidAlgebra/Degree.lean
+++ b/Mathlib/Algebra/MonoidAlgebra/Degree.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
+import Mathlib.Algebra.Group.Subsemigroup.Operations
 import Mathlib.Algebra.MonoidAlgebra.Support
 import Mathlib.Order.Filter.Extr
 
diff --git a/Mathlib/Algebra/Order/Monoid/Submonoid.lean b/Mathlib/Algebra/Order/Monoid/Submonoid.lean
index 7dd9498120011..450cea09f161c 100644
--- a/Mathlib/Algebra/Order/Monoid/Submonoid.lean
+++ b/Mathlib/Algebra/Order/Monoid/Submonoid.lean
@@ -3,8 +3,9 @@ Copyright (c) 2021 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.Order.Monoid.Basic
+import Mathlib.Algebra.Group.Submonoid.Defs
+import Mathlib.Order.Interval.Set.Basic
 
 /-!
 # Ordered instances on submonoids
diff --git a/Mathlib/Algebra/Order/Star/Basic.lean b/Mathlib/Algebra/Order/Star/Basic.lean
index 19279611c7f7f..42f4b5b776602 100644
--- a/Mathlib/Algebra/Order/Star/Basic.lean
+++ b/Mathlib/Algebra/Order/Star/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.NoZeroSMulDivisors.Defs
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.Nat
diff --git a/Mathlib/Algebra/Ring/Action/Subobjects.lean b/Mathlib/Algebra/Ring/Action/Subobjects.lean
index d2e0376c2b7b3..9a15aad35c85a 100644
--- a/Mathlib/Algebra/Ring/Action/Subobjects.lean
+++ b/Mathlib/Algebra/Ring/Action/Subobjects.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Group.Submonoid.DistribMulAction
 import Mathlib.Algebra.Ring.Action.Basic
 
diff --git a/Mathlib/Algebra/Ring/Subring/Units.lean b/Mathlib/Algebra/Ring/Subring/Units.lean
index 157cdab1d1c19..97205c69943ca 100644
--- a/Mathlib/Algebra/Ring/Subring/Units.lean
+++ b/Mathlib/Algebra/Ring/Subring/Units.lean
@@ -3,7 +3,8 @@ Copyright (c) 2021 Chris Birkbeck. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Defs
+import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.Order.GroupWithZero.Submonoid
 import Mathlib.Algebra.Order.Ring.Defs
 
diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean
index 32776d896fc45..f2e5c48eb5513 100644
--- a/Mathlib/Algebra/Star/SelfAdjoint.lean
+++ b/Mathlib/Algebra/Star/SelfAdjoint.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Frédéric Dupuis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Algebra.Module.Defs
 import Mathlib.Algebra.Star.Pi
 import Mathlib.Algebra.Star.Rat
diff --git a/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean b/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
index efe02380cebd5..dcc019f7b9497 100644
--- a/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
+++ b/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Rémi Bottinelli. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémi Bottinelli, Junyan Xu
 -/
-import Mathlib.Algebra.Group.Subgroup.Basic
+import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.CategoryTheory.Groupoid.VertexGroup
 import Mathlib.CategoryTheory.Groupoid.Basic
 import Mathlib.CategoryTheory.Groupoid
diff --git a/Mathlib/Combinatorics/Additive/FreimanHom.lean b/Mathlib/Combinatorics/Additive/FreimanHom.lean
index 70de5725f129a..dc169558a2b3a 100644
--- a/Mathlib/Combinatorics/Additive/FreimanHom.lean
+++ b/Mathlib/Combinatorics/Additive/FreimanHom.lean
@@ -6,7 +6,7 @@ Authors: Yaël Dillies, Bhavik Mehta
 import Mathlib.Algebra.BigOperators.Ring
 import Mathlib.Algebra.CharP.Basic
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
-import Mathlib.Algebra.Group.Submonoid.Operations
+import Mathlib.Algebra.Group.Submonoid.Defs
 import Mathlib.Algebra.Order.BigOperators.Group.Multiset
 import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.ZMod.Defs
diff --git a/Mathlib/GroupTheory/Subsemigroup/Center.lean b/Mathlib/GroupTheory/Subsemigroup/Center.lean
index d0970e7e4ca85..fefb61e0ba65c 100644
--- a/Mathlib/GroupTheory/Subsemigroup/Center.lean
+++ b/Mathlib/GroupTheory/Subsemigroup/Center.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser, Jireh Loreaux
 -/
 import Mathlib.Algebra.Group.Center
-import Mathlib.Algebra.Group.Subsemigroup.Operations
+import Mathlib.Algebra.Group.Subsemigroup.Defs
 
 /-!
 # Centers of semigroups, as subsemigroups.
diff --git a/Mathlib/GroupTheory/Subsemigroup/Centralizer.lean b/Mathlib/GroupTheory/Subsemigroup/Centralizer.lean
index 40211ea65474b..3f5aa2075a30e 100644
--- a/Mathlib/GroupTheory/Subsemigroup/Centralizer.lean
+++ b/Mathlib/GroupTheory/Subsemigroup/Centralizer.lean
@@ -3,8 +3,9 @@ Copyright (c) 2021 Thomas Browning. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Jireh Loreaux
 -/
-import Mathlib.GroupTheory.Subsemigroup.Center
 import Mathlib.Algebra.Group.Center
+import Mathlib.Algebra.Group.Subsemigroup.Basic
+import Mathlib.GroupTheory.Subsemigroup.Center
 
 /-!
 # Centralizers in semigroups, as subsemigroups.
diff --git a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
index c2104c2b98ebb..223521ff5f3a5 100644
--- a/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
+++ b/Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
@@ -5,6 +5,7 @@ Authors: Jireh Loreaux
 -/
 import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Algebra.Group.Subsemigroup.Membership
+import Mathlib.Algebra.Group.Subsemigroup.Operations
 import Mathlib.Algebra.GroupWithZero.Center
 import Mathlib.Algebra.Ring.Center
 import Mathlib.Algebra.Ring.Centralizer