diff --git a/Mathlib.lean b/Mathlib.lean
index c52aa83a52c78..8dff03b97436a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -292,6 +292,7 @@ import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.Group.Submonoid.Pointwise
 import Mathlib.Algebra.Group.Submonoid.Units
 import Mathlib.Algebra.Group.Subsemigroup.Basic
+import Mathlib.Algebra.Group.Subsemigroup.Defs
 import Mathlib.Algebra.Group.Subsemigroup.Membership
 import Mathlib.Algebra.Group.Subsemigroup.Operations
 import Mathlib.Algebra.Group.Support
diff --git a/Mathlib/Algebra/Group/Subsemigroup/Basic.lean b/Mathlib/Algebra/Group/Subsemigroup/Basic.lean
index c5801a38f6bdb..fa82da88595fa 100644
--- a/Mathlib/Algebra/Group/Subsemigroup/Basic.lean
+++ b/Mathlib/Algebra/Group/Subsemigroup/Basic.lean
@@ -4,23 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
 Amelia Livingston, Yury Kudryashov, Yakov Pechersky
 -/
-import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Algebra.Group.Subsemigroup.Defs
 import Mathlib.Data.Set.Lattice
-import Mathlib.Data.SetLike.Basic
 
 /-!
-# Subsemigroups: definition and `CompleteLattice` structure
+# Subsemigroups: `CompleteLattice` structure
 
-This file defines bundled multiplicative and additive subsemigroups. We also define
-a `CompleteLattice` structure on `Subsemigroup`s,
+This file defines a `CompleteLattice` structure on `Subsemigroup`s,
 and define the closure of a set as the minimal subsemigroup that includes this set.
 
 ## Main definitions
 
-* `Subsemigroup M`: the type of bundled subsemigroup of a magma `M`; the underlying set is given in
-  the `carrier` field of the structure, and should be accessed through coercion as in `(S : Set M)`.
-* `AddSubsemigroup M` : the type of bundled subsemigroups of an additive magma `M`.
-
 For each of the following definitions in the `Subsemigroup` namespace, there is a corresponding
 definition in the `AddSubsemigroup` namespace.
 
@@ -56,143 +50,9 @@ section NonAssoc
 variable [Mul M] {s : Set M}
 variable [Add A] {t : Set A}
 
-/-- `MulMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(*)` -/
-class MulMemClass (S : Type*) (M : outParam Type*) [Mul M] [SetLike S M] : Prop where
-  /-- A substructure satisfying `MulMemClass` is closed under multiplication. -/
-  mul_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
-
-export MulMemClass (mul_mem)
-
-/-- `AddMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(+)` -/
-class AddMemClass (S : Type*) (M : outParam Type*) [Add M] [SetLike S M] : Prop where
-  /-- A substructure satisfying `AddMemClass` is closed under addition. -/
-  add_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s
-
-export AddMemClass (add_mem)
-
-attribute [to_additive] MulMemClass
-
-attribute [aesop safe apply (rule_sets := [SetLike])] mul_mem add_mem
-
-/-- A subsemigroup of a magma `M` is a subset closed under multiplication. -/
-structure Subsemigroup (M : Type*) [Mul M] where
-  /-- The carrier of a subsemigroup. -/
-  carrier : Set M
-  /-- The product of two elements of a subsemigroup belongs to the subsemigroup. -/
-  mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier
-
-/-- An additive subsemigroup of an additive magma `M` is a subset closed under addition. -/
-structure AddSubsemigroup (M : Type*) [Add M] where
-  /-- The carrier of an additive subsemigroup. -/
-  carrier : Set M
-  /-- The sum of two elements of an additive subsemigroup belongs to the subsemigroup. -/
-  add_mem' {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier
-
-attribute [to_additive AddSubsemigroup] Subsemigroup
-
 namespace Subsemigroup
 
-@[to_additive]
-instance : SetLike (Subsemigroup M) M :=
-  ⟨Subsemigroup.carrier, fun p q h => by cases p; cases q; congr⟩
-
-@[to_additive]
-instance : MulMemClass (Subsemigroup M) M where mul_mem := fun {_ _ _} => Subsemigroup.mul_mem' _
-
-initialize_simps_projections Subsemigroup (carrier → coe)
-initialize_simps_projections AddSubsemigroup (carrier → coe)
-
-@[to_additive (attr := simp)]
-theorem mem_carrier {s : Subsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s :=
-  Iff.rfl
-
-@[to_additive (attr := simp)]
-theorem mem_mk {s : Set M} {x : M} (h_mul) : x ∈ mk s h_mul ↔ x ∈ s :=
-  Iff.rfl
-
-@[to_additive (attr := simp, norm_cast)]
-theorem coe_set_mk (s : Set M) (h_mul) : (mk s h_mul : Set M) = s :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mk_le_mk {s t : Set M} (h_mul) (h_mul') : mk s h_mul ≤ mk t h_mul' ↔ s ⊆ t :=
-  Iff.rfl
-
-/-- Two subsemigroups are equal if they have the same elements. -/
-@[to_additive (attr := ext) "Two `AddSubsemigroup`s are equal if they have the same elements."]
-theorem ext {S T : Subsemigroup M} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T :=
-  SetLike.ext h
-
-/-- Copy a subsemigroup replacing `carrier` with a set that is equal to it. -/
-@[to_additive "Copy an additive subsemigroup replacing `carrier` with a set that is equal to it."]
-protected def copy (S : Subsemigroup M) (s : Set M) (hs : s = S) :
-    Subsemigroup M where
-  carrier := s
-  mul_mem' := hs.symm ▸ S.mul_mem'
-
-variable {S : Subsemigroup M}
-
-@[to_additive (attr := simp)]
-theorem coe_copy {s : Set M} (hs : s = S) : (S.copy s hs : Set M) = s :=
-  rfl
-
-@[to_additive]
-theorem copy_eq {s : Set M} (hs : s = S) : S.copy s hs = S :=
-  SetLike.coe_injective hs
-
-variable (S)
-
-/-- A subsemigroup is closed under multiplication. -/
-@[to_additive "An `AddSubsemigroup` is closed under addition."]
-protected theorem mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S :=
-  Subsemigroup.mul_mem' S
-
-/-- The subsemigroup `M` of the magma `M`. -/
-@[to_additive "The additive subsemigroup `M` of the magma `M`."]
-instance : Top (Subsemigroup M) :=
-  ⟨{  carrier := Set.univ
-      mul_mem' := fun _ _ => Set.mem_univ _ }⟩
-
-/-- The trivial subsemigroup `∅` of a magma `M`. -/
-@[to_additive "The trivial `AddSubsemigroup` `∅` of an additive magma `M`."]
-instance : Bot (Subsemigroup M) :=
-  ⟨{  carrier := ∅
-      mul_mem' := False.elim }⟩
-
-@[to_additive]
-instance : Inhabited (Subsemigroup M) :=
-  ⟨⊥⟩
-
-@[to_additive]
-theorem not_mem_bot {x : M} : x ∉ (⊥ : Subsemigroup M) :=
-  Set.not_mem_empty x
-
-@[to_additive (attr := simp)]
-theorem mem_top (x : M) : x ∈ (⊤ : Subsemigroup M) :=
-  Set.mem_univ x
-
-@[to_additive (attr := simp)]
-theorem coe_top : ((⊤ : Subsemigroup M) : Set M) = Set.univ :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem coe_bot : ((⊥ : Subsemigroup M) : Set M) = ∅ :=
-  rfl
-
-/-- The inf of two subsemigroups is their intersection. -/
-@[to_additive "The inf of two `AddSubsemigroup`s is their intersection."]
-instance : Inf (Subsemigroup M) :=
-  ⟨fun S₁ S₂ =>
-    { carrier := S₁ ∩ S₂
-      mul_mem' := fun ⟨hx, hx'⟩ ⟨hy, hy'⟩ => ⟨S₁.mul_mem hx hy, S₂.mul_mem hx' hy'⟩ }⟩
-
-@[to_additive (attr := simp)]
-theorem coe_inf (p p' : Subsemigroup M) : ((p ⊓ p' : Subsemigroup M) : Set M) = (p : Set M) ∩ p' :=
-  rfl
-
-@[to_additive (attr := simp)]
-theorem mem_inf {p p' : Subsemigroup M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' :=
-  Iff.rfl
+variable (S : Subsemigroup M)
 
 @[to_additive]
 instance : InfSet (Subsemigroup M) :=
@@ -235,19 +95,6 @@ instance : CompleteLattice (Subsemigroup M) :=
     inf_le_left := fun _ _ _ => And.left
     inf_le_right := fun _ _ _ => And.right }
 
-@[to_additive]
-theorem subsingleton_of_subsingleton [Subsingleton (Subsemigroup M)] : Subsingleton M := by
-  constructor; intro x y
-  have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
-  exact absurd (this x) not_mem_bot
-
-@[to_additive]
-instance [hn : Nonempty M] : Nontrivial (Subsemigroup M) :=
-  ⟨⟨⊥, ⊤, fun h => by
-      obtain ⟨x⟩ := id hn
-      refine absurd (?_ : x ∈ ⊥) not_mem_bot
-      simp [h]⟩⟩
-
 /-- The `Subsemigroup` generated by a set. -/
 @[to_additive "The `AddSubsemigroup` generated by a set"]
 def closure (s : Set M) : Subsemigroup M :=
@@ -385,12 +232,6 @@ variable [Mul N]
 
 open Subsemigroup
 
-/-- The subsemigroup of elements `x : M` such that `f x = g x` -/
-@[to_additive "The additive subsemigroup of elements `x : M` such that `f x = g x`"]
-def eqLocus (f g : M →ₙ* N) : Subsemigroup M where
-  carrier := { x | f x = g x }
-  mul_mem' (hx : _ = _) (hy : _ = _) := by simp [*]
-
 /-- If two mul homomorphisms are equal on a set, then they are equal on its subsemigroup closure. -/
 @[to_additive "If two add homomorphisms are equal on a set,
   then they are equal on its additive subsemigroup closure."]
@@ -398,10 +239,6 @@ theorem eqOn_closure {f g : M →ₙ* N} {s : Set M} (h : Set.EqOn f g s) :
     Set.EqOn f g (closure s) :=
   show closure s ≤ f.eqLocus g from closure_le.2 h
 
-@[to_additive]
-theorem eq_of_eqOn_top {f g : M →ₙ* N} (h : Set.EqOn f g (⊤ : Subsemigroup M)) : f = g :=
-  ext fun _ => h trivial
-
 @[to_additive]
 theorem eq_of_eqOn_dense {s : Set M} (hs : closure s = ⊤) {f g : M →ₙ* N} (h : s.EqOn f g) :
     f = g :=
diff --git a/Mathlib/Algebra/Group/Subsemigroup/Defs.lean b/Mathlib/Algebra/Group/Subsemigroup/Defs.lean
new file mode 100644
index 0000000000000..946d325924172
--- /dev/null
+++ b/Mathlib/Algebra/Group/Subsemigroup/Defs.lean
@@ -0,0 +1,229 @@
+/-
+Copyright (c) 2018 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
+Amelia Livingston, Yury Kudryashov, Yakov Pechersky
+-/
+import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Data.SetLike.Basic
+
+/-!
+# Subsemigroups: definition
+
+This file defines bundled multiplicative and additive subsemigroups.
+
+## Main definitions
+
+* `Subsemigroup M`: the type of bundled subsemigroup of a magma `M`; the underlying set is given in
+  the `carrier` field of the structure, and should be accessed through coercion as in `(S : Set M)`.
+* `AddSubsemigroup M` : the type of bundled subsemigroups of an additive magma `M`.
+
+For each of the following definitions in the `Subsemigroup` namespace, there is a corresponding
+definition in the `AddSubsemigroup` namespace.
+
+* `Subsemigroup.copy` : copy of a subsemigroup with `carrier` replaced by a set that is equal but
+  possibly not definitionally equal to the carrier of the original `Subsemigroup`.
+
+Similarly, for each of these definitions in the `MulHom` namespace, there is a corresponding
+definition in the `AddHom` namespace.
+
+* `MulHom.eqLocus f g`: the subsemigroup of those `x` such that `f x = g x`
+
+## Implementation notes
+
+Subsemigroup inclusion is denoted `≤` rather than `⊆`, although `∈` is defined as
+membership of a subsemigroup's underlying set.
+
+Note that `Subsemigroup M` does not actually require `Semigroup M`,
+instead requiring only the weaker `Mul M`.
+
+This file is designed to have very few dependencies. In particular, it should not use natural
+numbers.
+
+## Tags
+subsemigroup, subsemigroups
+-/
+
+assert_not_exists CompleteLattice
+assert_not_exists MonoidWithZero
+
+-- Only needed for notation
+variable {M : Type*} {N : Type*} {A : Type*}
+
+section NonAssoc
+
+variable [Mul M] {s : Set M}
+variable [Add A] {t : Set A}
+
+/-- `MulMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(*)` -/
+class MulMemClass (S : Type*) (M : outParam Type*) [Mul M] [SetLike S M] : Prop where
+  /-- A substructure satisfying `MulMemClass` is closed under multiplication. -/
+  mul_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
+
+export MulMemClass (mul_mem)
+
+/-- `AddMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(+)` -/
+class AddMemClass (S : Type*) (M : outParam Type*) [Add M] [SetLike S M] : Prop where
+  /-- A substructure satisfying `AddMemClass` is closed under addition. -/
+  add_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s
+
+export AddMemClass (add_mem)
+
+attribute [to_additive] MulMemClass
+
+attribute [aesop safe apply (rule_sets := [SetLike])] mul_mem add_mem
+
+/-- A subsemigroup of a magma `M` is a subset closed under multiplication. -/
+structure Subsemigroup (M : Type*) [Mul M] where
+  /-- The carrier of a subsemigroup. -/
+  carrier : Set M
+  /-- The product of two elements of a subsemigroup belongs to the subsemigroup. -/
+  mul_mem' {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier
+
+/-- An additive subsemigroup of an additive magma `M` is a subset closed under addition. -/
+structure AddSubsemigroup (M : Type*) [Add M] where
+  /-- The carrier of an additive subsemigroup. -/
+  carrier : Set M
+  /-- The sum of two elements of an additive subsemigroup belongs to the subsemigroup. -/
+  add_mem' {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier
+
+attribute [to_additive AddSubsemigroup] Subsemigroup
+
+namespace Subsemigroup
+
+@[to_additive]
+instance : SetLike (Subsemigroup M) M :=
+  ⟨Subsemigroup.carrier, fun p q h => by cases p; cases q; congr⟩
+
+@[to_additive]
+instance : MulMemClass (Subsemigroup M) M where mul_mem := fun {_ _ _} => Subsemigroup.mul_mem' _
+
+initialize_simps_projections Subsemigroup (carrier → coe)
+initialize_simps_projections AddSubsemigroup (carrier → coe)
+
+@[to_additive (attr := simp)]
+theorem mem_carrier {s : Subsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s :=
+  Iff.rfl
+
+@[to_additive (attr := simp)]
+theorem mem_mk {s : Set M} {x : M} (h_mul) : x ∈ mk s h_mul ↔ x ∈ s :=
+  Iff.rfl
+
+@[to_additive (attr := simp, norm_cast)]
+theorem coe_set_mk (s : Set M) (h_mul) : (mk s h_mul : Set M) = s :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mk_le_mk {s t : Set M} (h_mul) (h_mul') : mk s h_mul ≤ mk t h_mul' ↔ s ⊆ t :=
+  Iff.rfl
+
+/-- Two subsemigroups are equal if they have the same elements. -/
+@[to_additive (attr := ext) "Two `AddSubsemigroup`s are equal if they have the same elements."]
+theorem ext {S T : Subsemigroup M} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T :=
+  SetLike.ext h
+
+/-- Copy a subsemigroup replacing `carrier` with a set that is equal to it. -/
+@[to_additive "Copy an additive subsemigroup replacing `carrier` with a set that is equal to it."]
+protected def copy (S : Subsemigroup M) (s : Set M) (hs : s = S) :
+    Subsemigroup M where
+  carrier := s
+  mul_mem' := hs.symm ▸ S.mul_mem'
+
+variable {S : Subsemigroup M}
+
+@[to_additive (attr := simp)]
+theorem coe_copy {s : Set M} (hs : s = S) : (S.copy s hs : Set M) = s :=
+  rfl
+
+@[to_additive]
+theorem copy_eq {s : Set M} (hs : s = S) : S.copy s hs = S :=
+  SetLike.coe_injective hs
+
+variable (S)
+
+/-- A subsemigroup is closed under multiplication. -/
+@[to_additive "An `AddSubsemigroup` is closed under addition."]
+protected theorem mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S :=
+  Subsemigroup.mul_mem' S
+
+/-- The subsemigroup `M` of the magma `M`. -/
+@[to_additive "The additive subsemigroup `M` of the magma `M`."]
+instance : Top (Subsemigroup M) :=
+  ⟨{  carrier := Set.univ
+      mul_mem' := fun _ _ => Set.mem_univ _ }⟩
+
+/-- The trivial subsemigroup `∅` of a magma `M`. -/
+@[to_additive "The trivial `AddSubsemigroup` `∅` of an additive magma `M`."]
+instance : Bot (Subsemigroup M) :=
+  ⟨{  carrier := ∅
+      mul_mem' := False.elim }⟩
+
+@[to_additive]
+instance : Inhabited (Subsemigroup M) :=
+  ⟨⊥⟩
+
+@[to_additive]
+theorem not_mem_bot {x : M} : x ∉ (⊥ : Subsemigroup M) :=
+  Set.not_mem_empty x
+
+@[to_additive (attr := simp)]
+theorem mem_top (x : M) : x ∈ (⊤ : Subsemigroup M) :=
+  Set.mem_univ x
+
+@[to_additive (attr := simp)]
+theorem coe_top : ((⊤ : Subsemigroup M) : Set M) = Set.univ :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem coe_bot : ((⊥ : Subsemigroup M) : Set M) = ∅ :=
+  rfl
+
+/-- The inf of two subsemigroups is their intersection. -/
+@[to_additive "The inf of two `AddSubsemigroup`s is their intersection."]
+instance : Inf (Subsemigroup M) :=
+  ⟨fun S₁ S₂ =>
+    { carrier := S₁ ∩ S₂
+      mul_mem' := fun ⟨hx, hx'⟩ ⟨hy, hy'⟩ => ⟨S₁.mul_mem hx hy, S₂.mul_mem hx' hy'⟩ }⟩
+
+@[to_additive (attr := simp)]
+theorem coe_inf (p p' : Subsemigroup M) : ((p ⊓ p' : Subsemigroup M) : Set M) = (p : Set M) ∩ p' :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem mem_inf {p p' : Subsemigroup M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' :=
+  Iff.rfl
+
+@[to_additive]
+theorem subsingleton_of_subsingleton [Subsingleton (Subsemigroup M)] : Subsingleton M := by
+  constructor; intro x y
+  have : ∀ a : M, a ∈ (⊥ : Subsemigroup M) := by simp [Subsingleton.elim (⊥ : Subsemigroup M) ⊤]
+  exact absurd (this x) not_mem_bot
+
+@[to_additive]
+instance [hn : Nonempty M] : Nontrivial (Subsemigroup M) :=
+  ⟨⟨⊥, ⊤, fun h => by
+      obtain ⟨x⟩ := id hn
+      refine absurd (?_ : x ∈ ⊥) not_mem_bot
+      simp [h]⟩⟩
+
+end Subsemigroup
+
+namespace MulHom
+
+variable [Mul N]
+
+open Subsemigroup
+
+/-- The subsemigroup of elements `x : M` such that `f x = g x` -/
+@[to_additive "The additive subsemigroup of elements `x : M` such that `f x = g x`"]
+def eqLocus (f g : M →ₙ* N) : Subsemigroup M where
+  carrier := { x | f x = g x }
+  mul_mem' (hx : _ = _) (hy : _ = _) := by simp [*]
+
+@[to_additive]
+theorem eq_of_eqOn_top {f g : M →ₙ* N} (h : Set.EqOn f g (⊤ : Subsemigroup M)) : f = g :=
+  ext fun _ => h trivial
+
+end MulHom
+
+end NonAssoc