From bb5cf65b2100527ac34ec90158cc30ba141459b5 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Fri, 21 Mar 2025 18:20:06 +0100
Subject: [PATCH 1/6] first commit

---
 Mathlib/GroupTheory/QuotientGroup/Defs.lean | 38 ++++++++++++++++++---
 1 file changed, 34 insertions(+), 4 deletions(-)

diff --git a/Mathlib/GroupTheory/QuotientGroup/Defs.lean b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
index a890944dddb048..53f578ba9410f3 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Defs.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
@@ -150,6 +150,13 @@ theorem mk_zpow (a : G) (n : ℤ) : ((a ^ n : G) : Q) = (a : Q) ^ n :=
 
 @[to_additive (attr := simp)] lemma map_mk'_self : N.map (mk' N) = ⊥ := by aesop
 
+omit nN in
+private theorem lift_aux (φ : G →* M) (HN : N ≤ φ.ker) {x y : G} (h : x⁻¹ * y ∈ N) :
+    φ x = φ y :=
+  calc
+    φ x = φ (y * (x⁻¹ * y)⁻¹) := by rw [mul_inv_rev, inv_inv, mul_inv_cancel_left]
+    _ = φ y := by rw [φ.map_mul, HN (N.inv_mem h), mul_one]
+
 /-- A group homomorphism `φ : G →* M` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
 group homomorphism `G/N →* M`. -/
 @[to_additive "An `AddGroup` homomorphism `φ : G →+ M` with `N ⊆ ker(φ)` descends (i.e. `lift`s)
@@ -157,10 +164,7 @@ group homomorphism `G/N →* M`. -/
 def lift (φ : G →* M) (HN : N ≤ φ.ker) : Q →* M :=
   (QuotientGroup.con N).lift φ fun x y h => by
     simp only [QuotientGroup.con, leftRel_apply, Con.rel_mk] at h
-    rw [Con.ker_rel]
-    calc
-      φ x = φ (y * (x⁻¹ * y)⁻¹) := by rw [mul_inv_rev, inv_inv, mul_inv_cancel_left]
-      _ = φ y := by rw [φ.map_mul, HN (N.inv_mem h), mul_one]
+    exact (Con.ker_rel _).mpr <| lift_aux N φ HN h
 
 @[to_additive (attr := simp)]
 theorem lift_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : lift N φ HN (g : Q) = φ g :=
@@ -176,6 +180,20 @@ 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) :=
+  fun x ↦ ⟨mk (hφ x).choose, by rw [lift_mk, (hφ x).choose_spec]⟩
+
+@[to_additive]
+theorem lift_ker (φ : G →* M) (HN : N ≤ φ.ker) :
+    (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker := by
+  ext x
+  obtain ⟨a, rfl⟩ := QuotientGroup.mk_surjective x
+  simp only [Subgroup.mem_map, MonoidHom.mem_ker, lift_mk, mk'_apply]
+  exact ⟨fun ha ↦ ⟨a, ha, rfl⟩,
+    fun ⟨b, h₁, h₂⟩ ↦ by rwa [← lift_aux N φ HN (QuotientGroup.eq.mp h₂)]⟩
+
 /-- 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)`."]
@@ -196,6 +214,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 map_ker (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.lift_ker _ _ _
+
 @[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 :=

From 0c440f56591e1b1e6b7e948801ca770a45f5d638 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Wed, 26 Mar 2025 08:48:54 +0100
Subject: [PATCH 2/6] fix names

---
 Mathlib/GroupTheory/QuotientGroup/Defs.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/GroupTheory/QuotientGroup/Defs.lean b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
index 736756ea27a70e..6062e5951bac3e 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Defs.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
@@ -249,7 +249,7 @@ theorem lift_surjective_of_surjective (φ : G →* M) (hφ : Function.Surjective
   fun x ↦ ⟨mk (hφ x).choose, by rw [lift_mk, (hφ x).choose_spec]⟩
 
 @[to_additive]
-theorem lift_ker (φ : G →* M) (HN : N ≤ φ.ker) :
+theorem ker_lift (φ : G →* M) (HN : N ≤ φ.ker) :
     (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker := by
   ext x
   obtain ⟨a, rfl⟩ := QuotientGroup.mk_surjective x
@@ -284,10 +284,10 @@ theorem map_surjective_of_surjective (M : Subgroup H) [M.Normal] (f : G →* H)
   lift_surjective_of_surjective _ _ hf _
 
 @[to_additive]
-theorem map_ker (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) :
+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.lift_ker _ _ _
+  exact QuotientGroup.ker_lift _ _ _
 
 @[to_additive]
 theorem map_id_apply (h : N ≤ Subgroup.comap (MonoidHom.id _) N := (Subgroup.comap_id N).le) (x) :

From 5abdc6cde2388801925beb0c8d2cfd60cd66c52e Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Mon, 28 Apr 2025 13:47:54 +0200
Subject: [PATCH 3/6] review

---
 Mathlib/Data/Quot.lean                      | 10 ++++++++++
 Mathlib/GroupTheory/QuotientGroup/Defs.lean |  2 +-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean
index 797b1031e00802..9d43b12a86fdd6 100644
--- a/Mathlib/Data/Quot.lean
+++ b/Mathlib/Data/Quot.lean
@@ -297,6 +297,16 @@ theorem Quotient.lift_comp_mk {_ : Setoid α} (f : α → β) (h : ∀ a b : α,
     Quotient.lift f h ∘ Quotient.mk _ = f :=
   rfl
 
+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 bc77f042d64270..54fa24a04121b7 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Defs.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
@@ -246,7 +246,7 @@ theorem lift_quot_mk {φ : G →* M} (HN : N ≤ φ.ker) (g : G) :
 @[to_additive]
 theorem lift_surjective_of_surjective (φ : G →* M) (hφ : Function.Surjective φ) (HN : N ≤ φ.ker) :
     Function.Surjective (QuotientGroup.lift N φ HN) :=
-  fun x ↦ ⟨mk (hφ x).choose, by rw [lift_mk, (hφ x).choose_spec]⟩
+  Quotient.lift_surjective _ _ hφ
 
 @[to_additive]
 theorem ker_lift (φ : G →* M) (HN : N ≤ φ.ker) :

From 87c5fc2b393f487e9359bc9273393c952c351675 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Mon, 28 Apr 2025 15:00:43 +0200
Subject: [PATCH 4/6] new proof of ker_lift

---
 Mathlib/Algebra/Group/Subgroup/Ker.lean         |  3 +++
 Mathlib/Algebra/Group/Subgroup/Map.lean         |  4 ++++
 Mathlib/Algebra/Group/Submonoid/Operations.lean |  5 +++++
 Mathlib/GroupTheory/QuotientGroup/Defs.lean     | 13 ++++++++-----
 4 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean
index 51f6a636dc1ffb..a99e9644168d10 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
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/GroupTheory/QuotientGroup/Defs.lean b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
index 54fa24a04121b7..a7fbf6ea192cb8 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Defs.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
@@ -238,6 +238,11 @@ 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 :=
@@ -251,11 +256,9 @@ theorem lift_surjective_of_surjective (φ : G →* M) (hφ : Function.Surjective
 @[to_additive]
 theorem ker_lift (φ : G →* M) (HN : N ≤ φ.ker) :
     (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker := by
-  ext x
-  obtain ⟨a, rfl⟩ := QuotientGroup.mk_surjective x
-  simp_rw [Subgroup.mem_map, MonoidHom.mem_ker, lift_mk, mk'_apply]
-  exact ⟨fun ha ↦ ⟨a, ha, rfl⟩, fun ⟨b, h₁, h₂⟩ ↦ by
-    rwa [show φ a = φ b from congr_arg (lift N φ HN) h₂.symm]⟩
+  rw [← Subgroup.toSubmonoid_inj, Subgroup.map_toSubmonoid, MonoidHom.ker_toSubmonoid,
+    MonoidHom.ker_toSubmonoid, ← congr_arg MonoidHom.mker (lift_comp_mk' N φ HN),
+    ← MonoidHom.comap_mker, Submonoid.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

From f40516bb937c46cad02fbb89f9e2c1c248628e53 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 29 Apr 2025 18:27:03 -0500
Subject: [PATCH 5/6] Golf

---
 Mathlib/Algebra/Group/Subgroup/Ker.lean     | 3 ++-
 Mathlib/GroupTheory/QuotientGroup/Defs.lean | 5 ++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Algebra/Group/Subgroup/Ker.lean b/Mathlib/Algebra/Group/Subgroup/Ker.lean
index a99e9644168d10..a121785d4facd6 100644
--- a/Mathlib/Algebra/Group/Subgroup/Ker.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Ker.lean
@@ -264,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/GroupTheory/QuotientGroup/Defs.lean b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
index a7fbf6ea192cb8..7e033f722b0da7 100644
--- a/Mathlib/GroupTheory/QuotientGroup/Defs.lean
+++ b/Mathlib/GroupTheory/QuotientGroup/Defs.lean
@@ -256,9 +256,8 @@ theorem lift_surjective_of_surjective (φ : G →* M) (hφ : Function.Surjective
 @[to_additive]
 theorem ker_lift (φ : G →* M) (HN : N ≤ φ.ker) :
     (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker := by
-  rw [← Subgroup.toSubmonoid_inj, Subgroup.map_toSubmonoid, MonoidHom.ker_toSubmonoid,
-    MonoidHom.ker_toSubmonoid, ← congr_arg MonoidHom.mker (lift_comp_mk' N φ HN),
-    ← MonoidHom.comap_mker, Submonoid.map_comap_eq_self_of_surjective (mk'_surjective N)]
+  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

From 652a2ba6990bb13194e8140cf0a98e5c08f570fb Mon Sep 17 00:00:00 2001
From: Xavier Roblot <roblot@math.univ-lyon1.fr>
Date: Wed, 30 Apr 2025 10:45:46 +0200
Subject: [PATCH 6/6] make it a simp?

---
 Mathlib/Data/Quot.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Data/Quot.lean b/Mathlib/Data/Quot.lean
index 9d43b12a86fdd6..12e821417ec92e 100644
--- a/Mathlib/Data/Quot.lean
+++ b/Mathlib/Data/Quot.lean
@@ -297,6 +297,7 @@ 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 :=