no goals
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
⊢ f = 0
classical
  by_contra h
  exact w (isIso_of_mono_of_nonzero h)
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
h : ¬f = 0
⊢ False
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
⊢ f = 0
by_contra h
no goals
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
h : ¬f = 0
⊢ False
exact w (isIso_of_mono_of_nonzero h)