case refine'_1
G : CommGroupCat
inst✝ : Subsingleton ↑G
X : CommGroupCat
f : G ⟶ X
⊢ f = default

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