no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Limits.image.ι f ≫ cokernel.π f = 0
simp [← cancel_epi (factorThruImage f)]
case w
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ factorThruImage f ≫ (imageIsoImage f).inv =
    factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) (_ : Limits.image.ι f ≫ cokernel.π f = 0)
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (imageIsoImage f).inv = kernel.lift (cokernel.π f) (Limits.image.ι f) (_ : Limits.image.ι f ≫ cokernel.π f = 0)
apply image.ext
case w.h
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (factorThruImage f ≫ (imageIsoImage f).inv) ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) (_ : Limits.image.ι f ≫ cokernel.π f = 0)) ≫
      equalizer.ι (cokernel.π f) 0
case w
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ factorThruImage f ≫ (imageIsoImage f).inv =
    factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) (_ : Limits.image.ι f ≫ cokernel.π f = 0)
apply equalizer.hom_ext
no goals
case w.h
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (factorThruImage f ≫ (imageIsoImage f).inv) ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) (_ : Limits.image.ι f ≫ cokernel.π f = 0)) ≫
      equalizer.ι (cokernel.π f) 0
rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift,
  imageStrongEpiMonoFactorisation_e, Category.assoc, kernel.lift_ι, equalizer_as_kernel,
  kernel.lift_ι, Limits.image.fac]