no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
⊢ cokernel.π f = 0
classical
  by_contra h
  haveI := isIso_of_epi_of_nonzero h
  exact w (eq_zero_of_mono_cokernel f)
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
⊢ False
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
⊢ cokernel.π f = 0
by_contra h
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
this : IsIso (cokernel.π f)
⊢ False
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
⊢ False
haveI := isIso_of_epi_of_nonzero h
no goals
C : Type u
inst✝² : Category C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
this : IsIso (cokernel.π f)
⊢ False
exact w (eq_zero_of_mono_cokernel f)