diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean
index 4a227bec8ac9b..06d576a2260d7 100644
--- a/Mathlib/GroupTheory/Subgroup/Basic.lean
+++ b/Mathlib/GroupTheory/Subgroup/Basic.lean
@@ -2893,6 +2893,11 @@ theorem _root_.Subgroup.ker_inclusion {H K : Subgroup G} (h : H ≤ K) : (inclus
 #align subgroup.ker_inclusion Subgroup.ker_inclusion
 #align add_subgroup.ker_inclusion AddSubgroup.ker_inclusion
 
+@[to_additive]
+theorem ker_prod {M N : Type*} [MulOneClass M] [MulOneClass N] (f : G →* M) (g : G →* N) :
+    (f.prod g).ker = f.ker ⊓ g.ker :=
+  SetLike.ext fun _ => Prod.mk_eq_one
+
 @[to_additive]
 theorem prodMap_comap_prod {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N)
     (g : G' →* N') (S : Subgroup N) (S' : Subgroup N') :
diff --git a/Mathlib/GroupTheory/Subgroup/Finite.lean b/Mathlib/GroupTheory/Subgroup/Finite.lean
index 679066e4d247c..947efc4cf1206 100644
--- a/Mathlib/GroupTheory/Subgroup/Finite.lean
+++ b/Mathlib/GroupTheory/Subgroup/Finite.lean
@@ -173,6 +173,9 @@ theorem card_le_one_iff_eq_bot [Fintype H] : Fintype.card H ≤ 1 ↔ H = ⊥ :=
 #align subgroup.card_le_one_iff_eq_bot Subgroup.card_le_one_iff_eq_bot
 #align add_subgroup.card_nonpos_iff_eq_bot AddSubgroup.card_le_one_iff_eq_bot
 
+@[to_additive] lemma eq_bot_iff_card [Fintype H] : H = ⊥ ↔ Fintype.card H = 1 :=
+  ⟨by rintro rfl;  exact card_bot, eq_bot_of_card_eq _⟩
+
 @[to_additive one_lt_card_iff_ne_bot]
 theorem one_lt_card_iff_ne_bot [Fintype H] : 1 < Fintype.card H ↔ H ≠ ⊥ :=
   lt_iff_not_le.trans H.card_le_one_iff_eq_bot.not
diff --git a/Mathlib/GroupTheory/Submonoid/Membership.lean b/Mathlib/GroupTheory/Submonoid/Membership.lean
index e1fd3ddb157c2..497f36f39665a 100644
--- a/Mathlib/GroupTheory/Submonoid/Membership.lean
+++ b/Mathlib/GroupTheory/Submonoid/Membership.lean
@@ -342,6 +342,39 @@ theorem closure_singleton_one : closure ({1} : Set M) = ⊥ := by
   simp [eq_bot_iff_forall, mem_closure_singleton]
 #align submonoid.closure_singleton_one Submonoid.closure_singleton_one
 
+section Submonoid
+variable {S : Submonoid M} [Fintype S]
+open Fintype
+
+/- curly brackets `{}` are used here instead of instance brackets `[]` because
+  the instance in a goal is often not the same as the one inferred by type class inference.  -/
+@[to_additive]
+theorem card_bot {_ : Fintype (⊥ : Submonoid M)} : card (⊥ : Submonoid M) = 1 :=
+  card_eq_one_iff.2
+    ⟨⟨(1 : M), Set.mem_singleton 1⟩, fun ⟨_y, hy⟩ => Subtype.eq <| mem_bot.1 hy⟩
+
+@[to_additive]
+theorem eq_bot_of_card_le (h : card S ≤ 1) : S = ⊥ :=
+  let _ := card_le_one_iff_subsingleton.mp h
+  eq_bot_of_subsingleton S
+
+@[to_additive]
+theorem eq_bot_of_card_eq (h : card S = 1) : S = ⊥ :=
+  S.eq_bot_of_card_le (le_of_eq h)
+
+@[to_additive card_le_one_iff_eq_bot]
+theorem card_le_one_iff_eq_bot : card S ≤ 1 ↔ S = ⊥ :=
+  ⟨fun h =>
+    (eq_bot_iff_forall _).2 fun x hx => by
+      simpa [Subtype.ext_iff] using card_le_one_iff.1 h ⟨x, hx⟩ 1,
+    fun h => by simp [h]⟩
+
+@[to_additive]
+lemma eq_bot_iff_card : S = ⊥ ↔ card S = 1 :=
+  ⟨by rintro rfl;  exact card_bot, eq_bot_of_card_eq⟩
+
+end Submonoid
+
 @[to_additive]
 theorem _root_.FreeMonoid.mrange_lift {α} (f : α → M) :
     mrange (FreeMonoid.lift f) = closure (Set.range f) := by
diff --git a/Mathlib/GroupTheory/Submonoid/Operations.lean b/Mathlib/GroupTheory/Submonoid/Operations.lean
index c12e88636dbfd..f0c1d6d43154e 100644
--- a/Mathlib/GroupTheory/Submonoid/Operations.lean
+++ b/Mathlib/GroupTheory/Submonoid/Operations.lean
@@ -1372,6 +1372,13 @@ theorem eq_bot_iff_forall : S = ⊥ ↔ ∀ x ∈ S, x = (1 : M) :=
 #align submonoid.eq_bot_iff_forall Submonoid.eq_bot_iff_forall
 #align add_submonoid.eq_bot_iff_forall AddSubmonoid.eq_bot_iff_forall
 
+@[to_additive]
+theorem eq_bot_of_subsingleton [Subsingleton S] : S = ⊥ := by
+  rw [eq_bot_iff_forall]
+  intro y hy
+  change ((⟨y, hy⟩ : S) : M) = (1 : S)
+  rw [Subsingleton.elim (⟨y, hy⟩ : S) 1]
+
 @[to_additive]
 theorem nontrivial_iff_exists_ne_one (S : Submonoid M) : Nontrivial S ↔ ∃ x ∈ S, x ≠ (1 : M) :=
   calc
diff --git a/Mathlib/GroupTheory/Sylow.lean b/Mathlib/GroupTheory/Sylow.lean
index d89667509b347..81ef351ccf18b 100644
--- a/Mathlib/GroupTheory/Sylow.lean
+++ b/Mathlib/GroupTheory/Sylow.lean
@@ -500,9 +500,6 @@ theorem QuotientGroup.card_preimage_mk [Fintype G] (s : Subgroup G) (t : Set (G
 #align quotient_group.card_preimage_mk QuotientGroup.card_preimage_mk
 
 namespace Sylow
-
-open Subgroup Submonoid MulAction
-
 theorem mem_fixedPoints_mul_left_cosets_iff_mem_normalizer {H : Subgroup G} [Finite (H : Set G)]
     {x : G} : (x : G ⧸ H) ∈ MulAction.fixedPoints H (G ⧸ H) ↔ x ∈ normalizer H :=
   ⟨fun hx =>