diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean
index 51f6a636dc1ffb..a121785d4facd6 100644
--- a/Mathlib/Algebra/Group/Subgroup/Ker.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Ker.lean
@@ -233,6 +233,9 @@ def ker (f : G →* M) : Subgroup G :=
         f x⁻¹ = f x * f x⁻¹ := by rw [hx, one_mul]
         _ = 1 := by rw [← map_mul, mul_inv_cancel, map_one] }
 
+@[to_additive (attr := simp)]
+theorem ker_toSubmonoid (f : G →* M) : f.ker.toSubmonoid = MonoidHom.mker f := rfl
+
 @[to_additive (attr := simp)]
 theorem mem_ker {f : G →* M} {x : G} : x ∈ f.ker ↔ f x = 1 :=
   Iff.rfl
@@ -261,7 +264,8 @@ instance decidableMemKer [DecidableEq M] (f : G →* M) : DecidablePred (· ∈
   decidable_of_iff (f x = 1) f.mem_ker
 
 @[to_additive]
-theorem comap_ker (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker :=
+theorem comap_ker {P : Type*} [MulOneClass P] (g : N →* P) (f : G →* N) :
+    g.ker.comap f = (g.comp f).ker :=
   rfl
 
 @[to_additive (attr := simp)]
diff --git a/Mathlib/Algebra/Group/Subgroup/Map.lean b/Mathlib/Algebra/Group/Subgroup/Map.lean
index 0e5739cd49434e..fa191bdb13bf40 100644
--- a/Mathlib/Algebra/Group/Subgroup/Map.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Map.lean
@@ -116,6 +116,10 @@ def map (f : G →* N) (H : Subgroup G) : Subgroup N :=
 theorem coe_map (f : G →* N) (K : Subgroup G) : (K.map f : Set N) = f '' K :=
   rfl
 
+@[to_additive (attr := simp)]
+theorem map_toSubmonoid (f : G →* G') (K : Subgroup G):
+  (Subgroup.map f K).toSubmonoid = Submonoid.map f K.toSubmonoid := rfl
+
 @[to_additive (attr := simp)]
 theorem mem_map {f : G →* N} {K : Subgroup G} {y : N} : y ∈ K.map f ↔ ∃ x ∈ K, f x = y := Iff.rfl
 
diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean
index 9fd3c53bf0f6b8..42bd77d0fe52ed 100644
--- a/Mathlib/Algebra/Group/Submonoid/Operations.lean
+++ b/Mathlib/Algebra/Group/Submonoid/Operations.lean
@@ -1042,4 +1042,9 @@ theorem map_comap_eq_self {f : F} {S : Submonoid N} (h : S ≤ MonoidHom.mrange
     (S.comap f).map f = S := by
   simpa only [inf_of_le_left h] using map_comap_eq f S
 
+@[to_additive]
+theorem map_comap_eq_self_of_surjective {f : F} (h : Function.Surjective f) {S : Submonoid N} :
+    map f (comap f S) = S :=
+  map_comap_eq_self (MonoidHom.mrange_eq_top_of_surjective _ h ▸ le_top)
+
 end Submonoid
diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean
index 797b1031e00802..12e821417ec92e 100644
--- a/Mathlib/Data/Quot.lean
+++ b/Mathlib/Data/Quot.lean
@@ -297,6 +297,17 @@ theorem Quotient.lift_comp_mk {_ : Setoid α} (f : α → β) (h : ∀ a b : α,
     Quotient.lift f h ∘ Quotient.mk _ = f :=
   rfl
 
+@[simp]
+theorem Quotient.lift_surjective_iff {α β : Sort*} {s : Setoid α} (f : α → β)
+    (h : ∀ (a b : α), a ≈ b → f a = f b) :
+    Function.Surjective (Quotient.lift f h : Quotient s → β) ↔ Function.Surjective f :=
+  Quot.surjective_lift h
+
+theorem Quotient.lift_surjective {α β : Sort*} {s : Setoid α} (f : α → β)
+    (h : ∀ (a b : α), a ≈ b → f a = f b) (hf : Function.Surjective f):
+    Function.Surjective (Quotient.lift f h : Quotient s → β) :=
+  (Quot.surjective_lift h).mpr hf
+
 @[simp]
 theorem Quotient.lift₂_mk {α : Sort*} {β : Sort*} {γ : Sort*} {_ : Setoid α} {_ : Setoid β}
     (f : α → β → γ)
diff --git a/Mathlib/GroupTheory/QuotientGroup/Defs.lean b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
index afcc0795577ba2..7e033f722b0da7 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Defs.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
@@ -238,11 +238,27 @@ theorem lift_mk' {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (mk
   rfl
 -- TODO: replace `mk` with `mk'`)
 
+@[to_additive (attr := simp)]
+theorem lift_comp_mk' (φ : G →* M) (HN : N ≤ φ.ker) :
+    (QuotientGroup.lift N φ HN).comp (QuotientGroup.mk' N) = φ :=
+  rfl
+
 @[to_additive (attr := simp)]
 theorem lift_quot_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) :
     lift N φ HN (Quot.mk _ g : Q) = φ g :=
   rfl
 
+@[to_additive]
+theorem lift_surjective_of_surjective (φ : G →* M) (hφ : Function.Surjective φ) (HN : N ≤ φ.ker) :
+    Function.Surjective (QuotientGroup.lift N φ HN) :=
+  Quotient.lift_surjective _ _ hφ
+
+@[to_additive]
+theorem ker_lift (φ : G →* M) (HN : N ≤ φ.ker) :
+    (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker := by
+  rw [← congrArg MonoidHom.ker (lift_comp_mk' N φ HN), ← MonoidHom.comap_ker,
+    Subgroup.map_comap_eq_self_of_surjective (mk'_surjective N)]
+
 /-- A group homomorphism `f : G →* H` induces a map `G/N →* H/M` if `N ⊆ f⁻¹(M)`. -/
 @[to_additive
       "An `AddGroup` homomorphism `f : G →+ H` induces a map `G/N →+ H/M` if `N ⊆ f⁻¹(M)`."]
@@ -263,6 +279,18 @@ theorem map_mk' (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f)
     map N M f h (mk' _ x) = ↑(f x) :=
   rfl
 
+@[to_additive]
+theorem map_surjective_of_surjective (M : Subgroup H) [M.Normal] (f : G →* H)
+    (hf : Function.Surjective (mk ∘ f : G → H ⧸ M)) (h : N ≤ M.comap f) :
+    Function.Surjective (map N M f h) :=
+  lift_surjective_of_surjective _ _ hf _
+
+@[to_additive]
+theorem ker_map (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) :
+    (map N M f h).ker = Subgroup.map (mk' N) (M.comap f) := by
+  simp_rw [← ker_mk' M, MonoidHom.comap_ker]
+  exact QuotientGroup.ker_lift _ _ _
+
 @[to_additive]
 theorem map_id_apply (h : N ≤ Subgroup.comap (MonoidHom.id _) N := (Subgroup.comap_id N).le) (x) :
     map N N (MonoidHom.id _) h x = x :=