case refine'_1
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ f = default

case refine'_2
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
X Y : C
hY : IsZero Y
e : X ≅ Y
⊢ IsZero X
refine' ⟨fun Z => ⟨⟨⟨e.hom ≫ hY.to_ Z⟩, fun f => _⟩⟩,
  fun Z => ⟨⟨⟨hY.from_ Z ≫ e.inv⟩, fun f => _⟩⟩⟩
case refine'_1
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default
case refine'_1
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ f = default
rw [← cancel_epi e.inv]
no goals
case refine'_1
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default
apply hY.eq_of_src
case refine'_2
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom
case refine'_2
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f = default
rw [← cancel_mono e.hom]
no goals
case refine'_2
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom
apply hY.eq_of_tgt