C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ cokernel.π f = 0 ∧ kernel.ι (cokernel.π f) ≫ cokernel.π f = 0
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f (cokernel.π f)
rw [exact_iff]
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ cokernel.π f = 0 ∧ kernel.ι (cokernel.π f) ≫ cokernel.π f = 0
aesop_cat