no goals
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊥
⊢ f = 0
simpa [h, bot_factors_iff_zero] using mk_factors_self f
no goals
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ (isoZeroOfMonoEqZero h ≪≫ HasZeroObject.zeroIsoInitial).hom ≫ initial.to Y = f
simp [h]