case w
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
⊢ ∀ (X Y : C), Zero.zero = Zero.zero
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
⊢ I = J
apply ext_aux
case w
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero = Zero.zero
case w
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
⊢ ∀ (X Y : C), Zero.zero = Zero.zero
intro X Y
case w
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero
case w
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero = Zero.zero
have : (I.Zero X Y).zero ≫ (J.Zero Y Y).zero = (I.Zero X Y).zero := by
  apply I.zero_comp X (J.Zero Y Y).zero
case w
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
that : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero
case w
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero
have that : (I.Zero X Y).zero ≫ (J.Zero Y Y).zero = (J.Zero X Y).zero := by
  apply J.comp_zero (I.Zero X Y).zero Y
no goals
case w
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
that : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero = Zero.zero
rw[←this,←that]
no goals
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero ≫ Zero.zero = Zero.zero
apply I.zero_comp X (J.Zero Y Y).zero
no goals
C : Type u
inst✝¹ : Category C
D : Type u'
inst✝ : Category D
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero ≫ Zero.zero = Zero.zero
apply J.comp_zero (I.Zero X Y).zero Y