-- Mathlib/CategoryTheory/Simple.lean
theorem simple_of_cosimple (X : C) (h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0) :
    Simple X :=
  ⟨fun {Y} f I => by
    classical
      fconstructor
      · intros
        have hx := cokernel.π_of_epi f
        by_contra h
        subst h
        exact (h _).mp (cokernel.π_of_zero _ _) hx
      · intro hf
        suffices Epi f by exact isIso_of_mono_of_epi _
        apply Preadditive.epi_of_cokernel_zero
        by_contra h'
        exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')⟩

Proof state:
case mpr.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
h' : ¬cokernel.π f = 0
⊢ False

Tactic:
exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
intro hf

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ IsIso f

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ IsIso f

Tactic:
suffices Epi f by exact isIso_of_mono_of_epi _

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ Epi f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f ↔ f ≠ 0

Tactic:
fconstructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f → f ≠ 0

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ f ≠ 0 → IsIso f

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ Epi f

Tactic:
apply Preadditive.epi_of_cokernel_zero

Result:
case mpr.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ cokernel.π f = 0

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f → f ≠ 0

Tactic:
intros

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
⊢ f ≠ 0

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
I : Mono 0
a✝ : IsIso 0
hx : cokernel.π 0 = 0
⊢ False

Tactic:
exact (h _).mp (cokernel.π_of_zero _ _) hx

Result:
no goals

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
⊢ f ≠ 0

Tactic:
have hx := cokernel.π_of_epi f

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
hx : cokernel.π f = 0
⊢ f ≠ 0

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
hx : cokernel.π f = 0
⊢ f ≠ 0

Tactic:
by_contra h

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h✝ : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
hx : cokernel.π f = 0
h : f = 0
⊢ False

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h✝ : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
hx : cokernel.π f = 0
h : f = 0
⊢ False

Tactic:
subst h

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
I : Mono 0
a✝ : IsIso 0
hx : cokernel.π 0 = 0
⊢ False

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
this : Epi f
⊢ IsIso f

Tactic:
exact isIso_of_mono_of_epi _

Result:
no goals

Proof state:
case mpr.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ cokernel.π f = 0

Tactic:
by_contra h'

Result:
case mpr.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
h' : ¬cokernel.π f = 0
⊢ False