[GOAL]
G : GroupCat
inst✝ : Subsingleton ↑G
⊢ IsZero G
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : G ⟶ X
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.w
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : G ⟶ X
x : ↑G
⊢ ↑f x = ↑default x
[PROOFSTEP]
have : x = 1 := Subsingleton.elim _ _
[GOAL]
case refine'_1.w
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ ↑f x = ↑default x
[PROOFSTEP]
rw [this, map_one, map_one]
[GOAL]
case refine'_2
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : X ⟶ G
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w
G : GroupCat
inst✝ : Subsingleton ↑G
X : GroupCat
f : X ⟶ G
x✝ : ↑X
⊢ ↑f x✝ = ↑default x✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
G : CommGroupCat
inst✝ : Subsingleton ↑G
⊢ IsZero G
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : G ⟶ X
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.w
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : G ⟶ X
x : ↑G
⊢ ↑f x = ↑default x
[PROOFSTEP]
have : x = 1 := Subsingleton.elim _ _
[GOAL]
case refine'_1.w
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ ↑f x = ↑default x
[PROOFSTEP]
rw [this, map_one, map_one]
[GOAL]
case refine'_2
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : X ⟶ G
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : X ⟶ G
x✝ : ↑X
⊢ ↑f x✝ = ↑default x✝
[PROOFSTEP]
apply Subsingleton.elim
