awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h :
  Abelian.coimage f = (coimageStrongEpiMonoFactorisation f).I →
    Abelian.image f = (imageStrongEpiMonoFactorisation f).I →
      coimageImageComparison f =
        ((coimageStrongEpiMonoFactorisation f).toMonoIsImage.isoExt
            (imageStrongEpiMonoFactorisation f).toMonoIsImage).hom
⊢ IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (coimageImageComparison f)

Tactic:
convert!
    Iso.isIso_hom
      (IsImage.isoExt (coimageStrongEpiMonoFactorisation f).toMonoIsImage
        (imageStrongEpiMonoFactorisation f).toMonoIsImage)

Premises used: CategoryTheory.Abelian.imageStrongEpiMonoFactorisation, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation, CategoryTheory.Limits.IsImage.isoExt, CategoryTheory.Iso.isIso_hom, CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage
-- 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
e_3 : Abelian.coimage f = (coimageStrongEpiMonoFactorisation f).I
e_4 : Abelian.image f = (imageStrongEpiMonoFactorisation f).I
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
⊢ coimageImageComparison f =
    ((coimageStrongEpiMonoFactorisation f).toMonoIsImage.isoExt (imageStrongEpiMonoFactorisation f).toMonoIsImage).hom

Tactic:
ext
-- 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
e_3 : Abelian.coimage f = (coimageStrongEpiMonoFactorisation f).I
e_4 : Abelian.image f = (imageStrongEpiMonoFactorisation f).I
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
⊢ 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:
change _ = _ ≫ (imageStrongEpiMonoFactorisation f).m

Premises used: CategoryTheory.Abelian.imageStrongEpiMonoFactorisation, CategoryTheory.Limits.MonoFactorisation.m, CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation
-- 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
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) ≫
      (imageStrongEpiMonoFactorisation f).m

Tactic:
simp [-imageStrongEpiMonoFactorisation_m]

Premises used: CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_m
-- 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
⊢ Eq (α := kernel f ⟶ image f) (kernel.ι f ≫ factorThruImage f) 0

Tactic:
simp [← cancel_mono (Limits.image.ι f)]

Premises used: CategoryTheory.Limits.image.ι, CategoryTheory.cancel_mono
-- 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
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) ⋯) :
      X ⟶ image f)
⊢ Eq (α := Abelian.coimage f ⟶ image f) (Iso.hom (coimageIsoImage' f))
    (cokernel.desc (kernel.ι f) (factorThruImage f) ⋯)

Tactic:
ext
-- 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
⊢ 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) ⋯) :
      X ⟶ image f)

Tactic:
simp only [← cancel_mono (Limits.image.ι f), IsImage.isoExt_hom, cokernel.π_desc,
    Category.assoc, IsImage.lift_ι, coimageStrongEpiMonoFactorisation_m,
    Limits.image.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.ι, CategoryTheory.Limits.image.fac, CategoryTheory.cancel_mono, CategoryTheory.Limits.IsImage.isoExt_hom, CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Limits.IsImage.lift_ι, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_m
-- 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
⊢ Eq (α := X ⟶ Abelian.coimage f) (factorThruImage f ≫ Iso.inv (coimageIsoImage' f)) (cokernel.π (kernel.ι f))

Tactic:
simp only [IsImage.isoExt_inv, image.isImage_lift, image.fac_lift,
    coimageStrongEpiMonoFactorisation_e]

Premises used: CategoryTheory.Limits.image.fac_lift, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_e, CategoryTheory.Limits.image.isImage_lift, CategoryTheory.Limits.IsImage.isoExt_inv
-- 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
Z : C
g : Y ⟶ Z
⊢ Eq (α := Abelian.image f ⟶ Z) (image.ι f ≫ g) 0 ↔ f ≫ g = 0

Tactic:
simp [← cancel_epi (Abelian.factorThruImage _)]

Premises used: CategoryTheory.Abelian.factorThruImage, CategoryTheory.cancel_epi
-- 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
Z : C
g : Y ⟶ Z
⊢ Eq (α := X ⟶ Abelian.coimage g) (f ≫ coimage.π g) 0 ↔ f ≫ g = 0

Tactic:
simp [← cancel_mono (Abelian.factorThruCoimage _)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Abelian.factorThruCoimage
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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 (α := Abelian.image f.hom ⟶ cokernel g.hom) ((image.ι f.hom ≫ Arrow.Hom.right u) ≫ cokernel.π g.hom) 0

Tactic:
simp [← Arrow.w_assoc u]

Premises used: CategoryTheory.Arrow.w_assoc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
simp : Eq (α := kernel f.hom ⟶ g.right) ((kernel.ι f.hom ≫ Arrow.Hom.left u) ≫ g.hom) 0
⊢ Eq (α := kernel f.hom ⟶ Abelian.coimage g.hom) (kernel.ι f.hom ≫ Arrow.Hom.left u ≫ coimage.π g.hom) 0

Tactic:
simp [← Category.assoc, coimage.comp_π_eq_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.coimage.comp_π_eq_zero
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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 ⟶ g.right) ((kernel.ι f.hom ≫ Arrow.Hom.left u) ≫ g.hom) 0

Tactic:
simp
-- 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
⊢ Eq (α := Abelian.image f ⟶ Y) (Iso.hom (imageIsoImage f) ≫ Limits.image.ι f) (kernel.ι (cokernel.π f))

Tactic:
simp only [IsImage.isoExt_hom, IsImage.lift_ι, imageStrongEpiMonoFactorisation_m]

Premises used: CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_m, CategoryTheory.Limits.IsImage.isoExt_hom, CategoryTheory.Limits.IsImage.lift_ι
-- 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
Z : C
g : Y ⟶ Z
⊢ Eq (α := image f ⟶ cokernel f) (Limits.image.ι f ≫ cokernel.π f) 0

Tactic:
simp [← cancel_epi (factorThruImage f)]

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.cancel_epi
-- 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)
      (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)
⊢ Eq (α := image f ⟶ Abelian.image f) (Iso.inv (imageIsoImage f)) (kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯)

Tactic:
ext
-- 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
inst_2 : Epi f
T : C
g : X ⟶ T
hg : Eq (α := kernel f ⟶ T) (kernel.ι f ≫ g) 0
⊢ f ≫ epiDesc f g hg = g

Tactic:
(epiIsCokernelOfKernel _ (limit.isLimit _)).fac (CokernelCofork.ofπ _ hg) WalkingParallelPair.one

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Abelian.epiDesc, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Abelian.epiIsCokernelOfKernel, CategoryTheory.Limits.CokernelCofork.ofπ
-- 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
inst_2 : Mono f
T : C
g : T ⟶ Y
hg : Eq (α := T ⟶ cokernel f) (g ≫ cokernel.π f) 0
⊢ monoLift f g hg ≫ f = g

Tactic:
(monoIsKernelOfCokernel _ (colimit.isColimit _)).fac (KernelFork.ofι _ hg)
    WalkingParallelPair.zero

Premises used: CategoryTheory.Limits.KernelFork.ofι, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Abelian.monoLift, CategoryTheory.Abelian.monoIsKernelOfCokernel, CategoryTheory.Limits.WalkingParallelPair.zero, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
⊢ (parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).map WalkingParallelPairHom.left ≫
      Iso.hom (asIso (cokernelComparison i F)) =
    Iso.hom
        (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F).map WalkingParallelPairHom.left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
⊢ (parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).map WalkingParallelPairHom.right ≫
      Iso.hom (asIso (cokernelComparison i F)) =
    Iso.hom
        (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F).map WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
e : parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0 ≅
  parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext
    (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
refine : IsLimit ((Cone.postcompose e.inv).obj (F.mapCone (KernelFork.ofι i ⋯)))
⊢ IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F) (F.mapCone (KernelFork.ofι i ⋯))

Tactic:
refine IsLimit.postcomposeInvEquiv e _ ?_

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
e : parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0 ≅
  parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext
    (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (F :=
  parallelPair (Y :=
    Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
    (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
  (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
refine :
  Iso.hom
        (Iso.refl
          (Cone.pt (F :=
            parallelPair (Y :=
              Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
              (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
            (KernelFork.ofι (F.map i) ⋯))) ≫
      Fork.ι ((Cone.postcompose e.inv).obj (F.mapCone (KernelFork.ofι i ⋯))) =
    Fork.ι (KernelFork.ofι (F.map i) ⋯)
⊢ IsLimit ((Cone.postcompose e.inv).obj (F.mapCone (KernelFork.ofι i ⋯)))

Tactic:
refine IsLimit.ofIsoLimit hi (Fork.ext (Iso.refl _) ?_)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Fork.ext, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
e : parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0 ≅
  parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext
    (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (F :=
  parallelPair (Y :=
    Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
    (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
  (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
change : 𝟙 (F.obj X) ≫ F.map i ≫ 𝟙 (F.obj Y) = F.map i
⊢ Iso.hom
        (Iso.refl
          (Cone.pt (F :=
            parallelPair (Y :=
              Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
              (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
            (KernelFork.ofι (F.map i) ⋯))) ≫
      Fork.ι ((Cone.postcompose e.inv).obj (F.mapCone (KernelFork.ofι i ⋯))) =
    Fork.ι (KernelFork.ofι (F.map i) ⋯)

Tactic:
change 𝟙 _ ≫ F.map i ≫ 𝟙 _ = F.map i

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
i : X ⟶ Y
inst_4 : HasCokernel i
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Mono (F.map i)
inst_7 : PreservesColimit (parallelPair i 0) F
e : parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0 ≅
  parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext
    (Iso.refl ((parallelPair (Y := cokernel (F.map i)) (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (F :=
  parallelPair (Y :=
    Cocone.pt (F := parallelPair (F.map i) 0) (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯))
    (Cofork.π (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯)) 0)
  (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (P := cokernel (F.map i)) (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
rw : 𝟙 (F.obj X) ≫ F.map i = F.map i
rw₁ rw₂ : F.map i = F.map i
⊢ 𝟙 (F.obj X) ≫ F.map i ≫ 𝟙 (F.obj Y) = F.map i

Tactic:
rw [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
⊢ (parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) =
    Iso.hom (asIso (kernelComparison p F)) ≫
      (parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0).map WalkingParallelPairHom.left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
⊢ (parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) =
    Iso.hom (asIso (kernelComparison p F)) ≫
      (parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0).map WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
e : parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F ≅ parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
refine : IsColimit ((Cocone.precompose e.inv).obj (F.mapCocone (CokernelCofork.ofπ p ⋯)))
⊢ IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F) (F.mapCocone (CokernelCofork.ofπ p ⋯))

Tactic:
refine IsColimit.precomposeInvEquiv e _ ?_

Premises used: DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeInvEquiv
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
e : parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F ≅ parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (F :=
  parallelPair (X := Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
    (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
  (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
refine :
  Cofork.π (CokernelCofork.ofπ (F.map p) ⋯) ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt (F :=
            parallelPair (X :=
              Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
              (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
            (CokernelCofork.ofπ (F.map p) ⋯))) =
    Cofork.π ((Cocone.precompose e.inv).obj (F.mapCocone (CokernelCofork.ofπ p ⋯)))
⊢ IsColimit ((Cocone.precompose e.inv).obj (F.mapCocone (CokernelCofork.ofπ p ⋯)))

Tactic:
refine IsColimit.ofIsoColimit hp (Cofork.ext (Iso.refl _) ?_)

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.refl, CategoryTheory.Limits.Cofork.ext