From 4d7e1edcb6765e6133db0c8cc6b64367a5785803 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Tue, 25 Nov 2025 21:53:13 +0800
Subject: [PATCH 1/6] add stupid lemma

---
 Mathlib/Algebra/Category/Grp/Preadditive.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Mathlib/Algebra/Category/Grp/Preadditive.lean b/Mathlib/Algebra/Category/Grp/Preadditive.lean
index a387bde9581f22..7d9ad04d3f5238 100644
--- a/Mathlib/Algebra/Category/Grp/Preadditive.lean
+++ b/Mathlib/Algebra/Category/Grp/Preadditive.lean
@@ -68,4 +68,10 @@ def homAddEquiv : (M ⟶ N) ≃+ (M →+ N) :=
   { ConcreteCategory.homEquiv (C := AddCommGrpCat) with
     map_add' _ _ := rfl }
 
+lemma subsingleton_of_isZero {G : AddCommGrpCat} (h : Limits.IsZero G) :
+    Subsingleton G := by
+  apply subsingleton_of_forall_eq 0 (fun g ↦ ?_)
+  rw [← AddMonoidHom.id_apply G g, ← AddCommGrpCat.hom_id]
+  simp [(CategoryTheory.Limits.IsZero.iff_id_eq_zero G).mp h]
+
 end AddCommGrpCat

From 946e85abbe858dd7b8ac75603f780c3b52dd65e8 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Wed, 26 Nov 2025 00:58:39 +0800
Subject: [PATCH 2/6] use another proof

and remove the old one
---
 Mathlib/Algebra/Category/Grp/Preadditive.lean |  6 ----
 Mathlib/Algebra/Category/Grp/Zero.lean        | 28 +++++++++++++++++++
 2 files changed, 28 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/Preadditive.lean b/Mathlib/Algebra/Category/Grp/Preadditive.lean
index 7d9ad04d3f5238..a387bde9581f22 100644
--- a/Mathlib/Algebra/Category/Grp/Preadditive.lean
+++ b/Mathlib/Algebra/Category/Grp/Preadditive.lean
@@ -68,10 +68,4 @@ def homAddEquiv : (M ⟶ N) ≃+ (M →+ N) :=
   { ConcreteCategory.homEquiv (C := AddCommGrpCat) with
     map_add' _ _ := rfl }
 
-lemma subsingleton_of_isZero {G : AddCommGrpCat} (h : Limits.IsZero G) :
-    Subsingleton G := by
-  apply subsingleton_of_forall_eq 0 (fun g ↦ ?_)
-  rw [← AddMonoidHom.id_apply G g, ← AddCommGrpCat.hom_id]
-  simp [(CategoryTheory.Limits.IsZero.iff_id_eq_zero G).mp h]
-
 end AddCommGrpCat
diff --git a/Mathlib/Algebra/Category/Grp/Zero.lean b/Mathlib/Algebra/Category/Grp/Zero.lean
index 7248c553f904c5..a95fba26f4787a 100644
--- a/Mathlib/Algebra/Category/Grp/Zero.lean
+++ b/Mathlib/Algebra/Category/Grp/Zero.lean
@@ -39,6 +39,20 @@ theorem isZero_of_subsingleton (G : GrpCat) [Subsingleton G] : IsZero G := by
 instance : HasZeroObject GrpCat :=
   ⟨⟨of PUnit, isZero_of_subsingleton _⟩⟩
 
+@[to_additive]
+lemma subsingleton_of_isZero {G : GrpCat} (h : Limits.IsZero G) :
+    Subsingleton G := by
+  apply subsingleton_of_forall_eq 1 (fun g ↦ ?_)
+  rcases h.1 (GrpCat.of (G × G)) with ⟨uniq⟩
+  have : ofHom (MonoidHom.inl G G) g = ofHom (MonoidHom.inr G G) g:= by
+    rw [IsZero.eq_of_src h (ofHom (MonoidHom.inl G G)) (ofHom (MonoidHom.inr G G))]
+  simp only [hom_ofHom, MonoidHom.inl_apply, MonoidHom.inr_apply, Prod.mk.injEq] at this
+  exact this.1
+
+@[to_additive]
+lemma isZero_iff_subsingleton {G : GrpCat} : Limits.IsZero G ↔ Subsingleton G :=
+    ⟨fun h ↦ subsingleton_of_isZero h, fun _ ↦ isZero_of_subsingleton G⟩
+
 end GrpCat
 
 namespace CommGrpCat
@@ -56,4 +70,18 @@ theorem isZero_of_subsingleton (G : CommGrpCat) [Subsingleton G] : IsZero G := b
 instance : HasZeroObject CommGrpCat :=
   ⟨⟨of PUnit, isZero_of_subsingleton _⟩⟩
 
+@[to_additive]
+lemma subsingleton_of_isZero {G : CommGrpCat} (h : Limits.IsZero G) :
+    Subsingleton G := by
+  apply subsingleton_of_forall_eq 1 (fun g ↦ ?_)
+  rcases h.1 (CommGrpCat.of (G × G)) with ⟨uniq⟩
+  have : ofHom (MonoidHom.inl G G) g= ofHom (MonoidHom.inr G G) g:= by
+    rw [IsZero.eq_of_src h (ofHom (MonoidHom.inl G G)) (ofHom (MonoidHom.inr G G))]
+  simp only [hom_ofHom, MonoidHom.inl_apply, MonoidHom.inr_apply, Prod.mk.injEq] at this
+  exact this.1
+
+@[to_additive]
+lemma isZero_iff_subsingleton {G : CommGrpCat} : Limits.IsZero G ↔ Subsingleton G :=
+    ⟨fun h ↦ subsingleton_of_isZero h, fun _ ↦ isZero_of_subsingleton G⟩
+
 end CommGrpCat

From 7f6103ed2a3eb42a8cdd3114125791ca566435ee Mon Sep 17 00:00:00 2001
From: Nailin Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Wed, 26 Nov 2025 18:18:38 +0800
Subject: [PATCH 3/6] fix first proof

Co-authored-by: Christian Merten <christian@merten.dev>
---
 Mathlib/Algebra/Category/Grp/Zero.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/Zero.lean b/Mathlib/Algebra/Category/Grp/Zero.lean
index a95fba26f4787a..5e77dd42b73932 100644
--- a/Mathlib/Algebra/Category/Grp/Zero.lean
+++ b/Mathlib/Algebra/Category/Grp/Zero.lean
@@ -73,12 +73,7 @@ instance : HasZeroObject CommGrpCat :=
 @[to_additive]
 lemma subsingleton_of_isZero {G : CommGrpCat} (h : Limits.IsZero G) :
     Subsingleton G := by
-  apply subsingleton_of_forall_eq 1 (fun g ↦ ?_)
-  rcases h.1 (CommGrpCat.of (G × G)) with ⟨uniq⟩
-  have : ofHom (MonoidHom.inl G G) g= ofHom (MonoidHom.inr G G) g:= by
-    rw [IsZero.eq_of_src h (ofHom (MonoidHom.inl G G)) (ofHom (MonoidHom.inr G G))]
-  simp only [hom_ofHom, MonoidHom.inl_apply, MonoidHom.inr_apply, Prod.mk.injEq] at this
-  exact this.1
+  (h.iso (isZero_of_subsingleton <| .of PUnit)).commGroupIsoToMulEquiv.subsingleton
 
 @[to_additive]
 lemma isZero_iff_subsingleton {G : CommGrpCat} : Limits.IsZero G ↔ Subsingleton G :=

From b306d5b025176f0ed6935971d9c4521408aa2b38 Mon Sep 17 00:00:00 2001
From: Nailin Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Wed, 26 Nov 2025 18:18:52 +0800
Subject: [PATCH 4/6] fix second proof

Co-authored-by: Christian Merten <christian@merten.dev>
---
 Mathlib/Algebra/Category/Grp/Zero.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/Zero.lean b/Mathlib/Algebra/Category/Grp/Zero.lean
index 5e77dd42b73932..e00388316e0832 100644
--- a/Mathlib/Algebra/Category/Grp/Zero.lean
+++ b/Mathlib/Algebra/Category/Grp/Zero.lean
@@ -42,12 +42,7 @@ instance : HasZeroObject GrpCat :=
 @[to_additive]
 lemma subsingleton_of_isZero {G : GrpCat} (h : Limits.IsZero G) :
     Subsingleton G := by
-  apply subsingleton_of_forall_eq 1 (fun g ↦ ?_)
-  rcases h.1 (GrpCat.of (G × G)) with ⟨uniq⟩
-  have : ofHom (MonoidHom.inl G G) g = ofHom (MonoidHom.inr G G) g:= by
-    rw [IsZero.eq_of_src h (ofHom (MonoidHom.inl G G)) (ofHom (MonoidHom.inr G G))]
-  simp only [hom_ofHom, MonoidHom.inl_apply, MonoidHom.inr_apply, Prod.mk.injEq] at this
-  exact this.1
+  (h.iso (isZero_of_subsingleton <| .of PUnit)).groupIsoToMulEquiv.subsingleton
 
 @[to_additive]
 lemma isZero_iff_subsingleton {G : GrpCat} : Limits.IsZero G ↔ Subsingleton G :=

From f2de9028044a0968ede42fc1853cf1d1b2ba0302 Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Wed, 26 Nov 2025 18:32:33 +0800
Subject: [PATCH 5/6] fix

---
 Mathlib/Algebra/Category/Grp/Zero.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/Zero.lean b/Mathlib/Algebra/Category/Grp/Zero.lean
index e00388316e0832..bfb1057ff0b83e 100644
--- a/Mathlib/Algebra/Category/Grp/Zero.lean
+++ b/Mathlib/Algebra/Category/Grp/Zero.lean
@@ -41,7 +41,7 @@ instance : HasZeroObject GrpCat :=
 
 @[to_additive]
 lemma subsingleton_of_isZero {G : GrpCat} (h : Limits.IsZero G) :
-    Subsingleton G := by
+    Subsingleton G :=
   (h.iso (isZero_of_subsingleton <| .of PUnit)).groupIsoToMulEquiv.subsingleton
 
 @[to_additive]
@@ -67,7 +67,7 @@ instance : HasZeroObject CommGrpCat :=
 
 @[to_additive]
 lemma subsingleton_of_isZero {G : CommGrpCat} (h : Limits.IsZero G) :
-    Subsingleton G := by
+    Subsingleton G :=
   (h.iso (isZero_of_subsingleton <| .of PUnit)).commGroupIsoToMulEquiv.subsingleton
 
 @[to_additive]

From c18d6783b1503bdb030951556c758afd1e74392e Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Wed, 26 Nov 2025 19:20:43 +0800
Subject: [PATCH 6/6] fix indent

---
 Mathlib/Algebra/Category/Grp/Zero.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/Category/Grp/Zero.lean b/Mathlib/Algebra/Category/Grp/Zero.lean
index bfb1057ff0b83e..4bd2af73259c54 100644
--- a/Mathlib/Algebra/Category/Grp/Zero.lean
+++ b/Mathlib/Algebra/Category/Grp/Zero.lean
@@ -46,7 +46,7 @@ lemma subsingleton_of_isZero {G : GrpCat} (h : Limits.IsZero G) :
 
 @[to_additive]
 lemma isZero_iff_subsingleton {G : GrpCat} : Limits.IsZero G ↔ Subsingleton G :=
-    ⟨fun h ↦ subsingleton_of_isZero h, fun _ ↦ isZero_of_subsingleton G⟩
+  ⟨fun h ↦ subsingleton_of_isZero h, fun _ ↦ isZero_of_subsingleton G⟩
 
 end GrpCat
 
@@ -72,6 +72,6 @@ lemma subsingleton_of_isZero {G : CommGrpCat} (h : Limits.IsZero G) :
 
 @[to_additive]
 lemma isZero_iff_subsingleton {G : CommGrpCat} : Limits.IsZero G ↔ Subsingleton G :=
-    ⟨fun h ↦ subsingleton_of_isZero h, fun _ ↦ isZero_of_subsingleton G⟩
+  ⟨fun h ↦ subsingleton_of_isZero h, fun _ ↦ isZero_of_subsingleton G⟩
 
 end CommGrpCat