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