chore(Group/Subsemigroup/Basic): split off Defs file (#17725)

The criteria for including a result in `Algebra.Group.Subsemigroup.Basic`:

* Can it be defined with only `Defs` imports?
* Is it needed for a subsequent `def` or `instance`?

This mostly prepares for splitting `Submonoid.Basic`.

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

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,23 +232,13 @@ 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."]
 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 :=