-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
w :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := image f) (factorThruImage f)
          (IsImage.lift (Image.isImage f) (imageStrongEpiMonoFactorisation f).toMonoFactorisation) :
        X ⟶ Abelian.image f)
      (equalizer.ι (cokernel.π f) 0 : equalizer (Y := cokernel f) (cokernel.π f) 0 ⟶ Y) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₁ :
  CategoryStruct.comp (Y := image f) (factorThruImage f)
        (image.lift (imageStrongEpiMonoFactorisation f).toMonoFactorisation) ≫
      equalizer.ι (cokernel.π f) 0 =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₂ :
  (imageStrongEpiMonoFactorisation f).e ≫ equalizer.ι (cokernel.π f) 0 =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₃ :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) (Abelian.factorThruImage f)
      (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)
w₄ :
  CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0) (Abelian.factorThruImage f)
      (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := image f) (factorThruImage f : X ⟶ image f)
      (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
          (kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0) :
        image f ⟶ Y)
w₅ :
  f =
    CategoryStruct.comp (Y := image f) (factorThruImage f : X ⟶ image f)
      (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
          (kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0) :
        image f ⟶ Y)
w₆ :
  f =
    CategoryStruct.comp (Y := image f) (factorThruImage f : X ⟶ image f)
      (CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
          (kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (kernel.ι (cokernel.π f)) :
        image f ⟶ Y)
w₇ : f = CategoryStruct.comp (Y := image f) (factorThruImage f) (Limits.image.ι f)
w₈ w₉ : f = f
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ Iso.inv (imageIsoImage f)) (equalizer.ι (cokernel.π f) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) (equalizer.ι (cokernel.π f) 0)

Tactic:
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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_e, CategoryTheory.Limits.equalizer_as_kernel, CategoryTheory.Limits.image.fac_lift, CategoryTheory.Limits.image.fac, CategoryTheory.Limits.image.isImage_lift, CategoryTheory.Limits.IsImage.isoExt_inv, CategoryTheory.Limits.kernel.lift_ι