awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
aux :
  ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
      Cofork.π s
A : CokernelCofork (X := kernel f) (kernel.ι f)
g : Cocone.pt (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯) ⟶ A.pt
hg : f ≫ g = Cofork.π A
refine_2 :
  f ≫ g =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
⊢ g =
    (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
      A
have refine_2₁ : Cofork.π A =
  f ≫
    (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
      A
Tactic: rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
aux :
  ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
      Cofork.π s
A : CokernelCofork (X := kernel f) (kernel.ι f)
g : Cocone.pt (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯) ⟶ A.pt
hg : f ≫ g = Cofork.π A
refine_2 :
  f ≫ g =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
refine_2₁ :
  Cofork.π A =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
⊢ g =
    (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
      A
have refine_2₂ : Cofork.π (CokernelCofork.ofπ f sorry) ≫
    inv (imageMonoFactorisation f).m ≫
      CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
        (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A) =
  f ≫
    (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
      A
Tactic: rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
aux :
  ∀ (s : CokernelCofork (X := kernel f) (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
      Cofork.π s
A : CokernelCofork (X := kernel f) (kernel.ι f)
g : Cocone.pt (F := parallelPair (X := kernel f) (kernel.ι f) 0) (CokernelCofork.ofπ f ⋯) ⟶ A.pt
hg : f ≫ g = Cofork.π A
refine_2 :
  f ≫ g =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
refine_2₁ :
  Cofork.π A =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
refine_2₂ :
  Cofork.π (CokernelCofork.ofπ f ⋯) ≫
      inv (imageMonoFactorisation f).m ≫
        CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
          (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A) =
    f ≫
      (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
          inv (imageMonoFactorisation f).m ≫
            CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
              (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
        A
⊢ g =
    (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
      A
have refine_2₃ : f ≫
    inv (imageMonoFactorisation f).m ≫
      CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
        (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A) =
  f ≫
    (fun (A : CokernelCofork (X := kernel f) (kernel.ι f)) ↦
        inv (imageMonoFactorisation f).m ≫
          CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
            (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) A))
      A
Tactic: rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : CokernelCofork (X := kernel f) (kernel.ι f)
⊢ Cofork.π (CokernelCofork.ofπ f ⋯) ≫
      inv (imageMonoFactorisation f).m ≫
        CategoryStruct.comp (Y := Abelian.coimage f) (inv (coimageImageComparison f))
          (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
    Cofork.π s
have refine_1 : CategoryStruct.comp (Y := Abelian.coimage f) ((f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f))
    (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
  Cofork.π s
Tactic: simp only [CokernelCofork.π_ofπ, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : CokernelCofork (X := kernel f) (kernel.ι f)
⊢ CategoryStruct.comp (Y := Abelian.coimage f) ((f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f))
      (colimit.desc (parallelPair (X := kernel f) (kernel.ι f) 0) s) =
    Cofork.π s
have h : (X ⟶ s.pt) = ((parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt) →
  X = (parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one →
    Eq (α := X ⟶ Abelian.coimage f) ((f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f))
      (colimit.ι (parallelPair (X := kernel f) (kernel.ι f) 0) WalkingParallelPair.one)
Tactic: convert! colimit.ι_desc s WalkingParallelPair.one using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
inst_3 : HasCokernels.{v, u} C
inst_4 : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
inst_5 : HasFiniteProducts.{v, u} C
X Y : C
f : X ⟶ Y
m : Epi f
this_1 : HasImages.{v, u} C
this_2 : HasEqualizers.{v, u} C
this : HasZeroObject.{v, u} C
s : CokernelCofork (X := kernel f) (kernel.ι f)
e_1 : (X ⟶ s.pt) = ((parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3 : X = (parallelPair (X := kernel f) (kernel.ι f) 0).obj WalkingParallelPair.one
⊢ Eq (α := X ⟶ Abelian.coimage f) ((f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f))
    (colimit.ι (parallelPair (X := kernel f) (kernel.ι f) 0) WalkingParallelPair.one)
have h : (imageMonoFactorisation f).e ≫ (imageMonoFactorisation f).m = f
Tactic: rw [IsIso.comp_inv_eq, IsIso.comp_inv_eq, eq_comm, ← imageMonoFactorisation_e']
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
⊢ IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)
have h : Abelian.coimage f = (coimageStrongEpiMonoFactorisation f).I →
  Abelian.image f = (imageStrongEpiMonoFactorisation f).I →
    coimageImageComparison f =
      ((coimageStrongEpiMonoFactorisation f).toMonoIsImage.isoExt (imageStrongEpiMonoFactorisation f).toMonoIsImage).hom
Tactic: convert!
    Iso.isIso_hom
      (IsImage.isoExt (coimageStrongEpiMonoFactorisation f).toMonoIsImage
        (imageStrongEpiMonoFactorisation f).toMonoIsImage)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
e_3 : Abelian.coimage f = (coimageStrongEpiMonoFactorisation f).I
e_4 : Abelian.image f = (imageStrongEpiMonoFactorisation f).I
⊢ coimageImageComparison f =
    ((coimageStrongEpiMonoFactorisation f).toMonoIsImage.isoExt (imageStrongEpiMonoFactorisation f).toMonoIsImage).hom
have h : CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
    (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (coimageImageComparison f))
    (equalizer.ι (cokernel.π f) 0) =
  (coequalizer.π (kernel.ι f) 0 ≫
      ((coimageStrongEpiMonoFactorisation f).toMonoIsImage.isoExt
          (imageStrongEpiMonoFactorisation f).toMonoIsImage).hom) ≫
    equalizer.ι (cokernel.π f) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
e_3 : Abelian.coimage f = (coimageStrongEpiMonoFactorisation f).I
e_4 : Abelian.image f = (imageStrongEpiMonoFactorisation f).I
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
        (coimageImageComparison f))
      (equalizer.ι (cokernel.π f) 0) =
    (coequalizer.π (kernel.ι f) 0 ≫
        ((coimageStrongEpiMonoFactorisation f).toMonoIsImage.isoExt
            (imageStrongEpiMonoFactorisation f).toMonoIsImage).hom) ≫
      equalizer.ι (cokernel.π f) 0
have h : CategoryStruct.comp (Y := equalizer (Y := cokernel f) (cokernel.π f) 0)
    (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (coimageImageComparison f))
    (equalizer.ι (cokernel.π f) 0) =
  (coequalizer.π (kernel.ι f) 0 ≫
      ((coimageStrongEpiMonoFactorisation f).toMonoIsImage.isoExt
          (imageStrongEpiMonoFactorisation f).toMonoIsImage).hom) ≫
    (imageStrongEpiMonoFactorisation f).m
Tactic: change _ = _ ≫ (imageStrongEpiMonoFactorisation f).m
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := Abelian.coimage f ⟶ image f) (Iso.hom (coimageIsoImage' f))
    (cokernel.desc (kernel.ι f) (factorThruImage f) ⋯)
have h : Eq (α := X ⟶ image f)
  (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (Iso.hom (coimageIsoImage' f)) :
    X ⟶ image f)
  (CategoryStruct.comp (Y := coequalizer (X := kernel f) (kernel.ι f) 0) (coequalizer.π (kernel.ι f) 0)
      (cokernel.desc (kernel.ι f) (factorThruImage f) sorry) :
    X ⟶ image f)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f_1 : X ⟶ Y
Z : C
g_1 : Y ⟶ Z
f g : Arrow.{v, u} C
u : f ⟶ g
⊢ Eq (α := kernel f.hom ⟶ Abelian.coimage g.hom) (kernel.ι f.hom ≫ Arrow.Hom.left u ≫ coimage.π g.hom) 0
have simp : Eq (α := kernel f.hom ⟶ g.right) ((kernel.ι f.hom ≫ Arrow.Hom.left u) ≫ g.hom) 0
Tactic: simp [← Category.assoc, coimage.comp_π_eq_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq (α := image f ⟶ Abelian.image f) (Iso.inv (imageIsoImage f)) (kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯)
have w : 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) sorry) (equalizer.ι (cokernel.π f) 0)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X Y : C
f : X ⟶ Y
⊢ 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)
have 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) sorry) (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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)
⊢ 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)
have 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) sorry) (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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)
⊢ 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)
have 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) sorry) (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
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)
⊢ 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)
have 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) sorry) (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]