C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X Y : C
inst✝ : HasImage 0
⊢ lift (monoFactorisationZero X Y) ≫ (monoFactorisationZero X Y).m = 0
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X Y : C
inst✝ : HasImage 0
⊢ ι 0 = 0
rw [← image.lift_fac (monoFactorisationZero X Y)]
no goals
C : Type u
inst✝⁴ : Category C
D : Type u'
inst✝³ : Category D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X Y : C
inst✝ : HasImage 0
⊢ lift (monoFactorisationZero X Y) ≫ (monoFactorisationZero X Y).m = 0
simp