C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f (coimage.π g ≫ Abelian.factorThruCoimage g) ↔ Exact f (coimage.π g)
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ Exact f (coimage.π g)
conv_lhs => rw [← Abelian.coimage.fac g]
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f (coimage.π g ≫ Abelian.factorThruCoimage g) ↔ Exact f (coimage.π g)
rw [exact_comp_mono_iff]