case tfae_3_to_2
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f 0 → cokernel.π f = 0

C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
tfae_have 3 → 2
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
⊢ Epi f → Exact f 0

C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
tfae_1_to_3 : Epi f → Exact f 0
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
tfae_have 1 → 3
case tfae_2_to_1
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
tfae_1_to_3 : Epi f → Exact f 0
⊢ cokernel.π f = 0 → Epi f

C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
tfae_1_to_3 : Epi f → Exact f 0
tfae_2_to_1 : cokernel.π f = 0 → Epi f
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
tfae_1_to_3 : Epi f → Exact f 0
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
tfae_have 2 → 1
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
tfae_1_to_3 : Epi f → Exact f 0
tfae_2_to_1 : cokernel.π f = 0 → Epi f
⊢ TFAE [Epi f, cokernel.π f = 0, Exact f 0]
tfae_finish
case tfae_3_to_2
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ 0 = 0 ∧ kernel.ι 0 ≫ cokernel.π f = 0 → cokernel.π f = 0
case tfae_3_to_2
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f 0 → cokernel.π f = 0
rw [exact_iff]
case tfae_3_to_2.intro
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : kernel.ι 0 ≫ cokernel.π f = 0
⊢ cokernel.π f = 0
case tfae_3_to_2
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ 0 = 0 ∧ kernel.ι 0 ≫ cokernel.π f = 0 → cokernel.π f = 0
rintro ⟨-, h⟩
no goals
case tfae_3_to_2.intro
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : kernel.ι 0 ≫ cokernel.π f = 0
⊢ cokernel.π f = 0
exact zero_of_epi_comp _ h
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
⊢ Epi f → f ≫ 0 = 0 ∧ kernel.ι 0 ≫ cokernel.π f = 0
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
⊢ Epi f → Exact f 0
rw [exact_iff]
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
✝ : Epi f
⊢ f ≫ 0 = 0 ∧ kernel.ι 0 ≫ cokernel.π f = 0
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
⊢ Epi f → f ≫ 0 = 0 ∧ kernel.ι 0 ≫ cokernel.π f = 0
intro
no goals
case tfae_1_to_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
✝ : Epi f
⊢ f ≫ 0 = 0 ∧ kernel.ι 0 ≫ cokernel.π f = 0
exact ⟨by simp, by simp [cokernel.π_of_epi]⟩
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
✝ : Epi f
⊢ f ≫ 0 = 0
simp
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
✝ : Epi f
⊢ kernel.ι 0 ≫ cokernel.π f = 0
simp [cokernel.π_of_epi]
no goals
case tfae_2_to_1
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_3_to_2 : Exact f 0 → cokernel.π f = 0
tfae_1_to_3 : Epi f → Exact f 0
⊢ cokernel.π f = 0 → Epi f
exact epi_of_cokernel_π_eq_zero _