C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
w : f ≠ 0
I : IsIso (cokernel.π f)
⊢ Mono (cokernel.π f)
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
w : f ≠ 0
I : IsIso (cokernel.π f)
⊢ Mono (cokernel.π f)
skip
no goals
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
w : f ≠ 0
I : IsIso (cokernel.π f)
⊢ Mono (cokernel.π f)
infer_instance