awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : Functor.Full (F C)
this : Functor.Full (C := AsSmall C) (G C)
⊢ Functor.Full (C := AsSmall C) (D := ModuleCat (EmbeddingRing.{v, u} C)) (G C ⋙ H C)

Tactic:
have : (G C ⋙ H C).Full := IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding _
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : Functor.Full (F C)
this_2 : Functor.Full (C := AsSmall C) (G C)
this : Functor.Full (C := AsSmall C) (D := ModuleCat (EmbeddingRing.{v, u} C)) (G C ⋙ H C)
⊢ Functor.Full (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ PreservesFiniteLimits (C := C) (Equivalence.functor AsSmall.equiv)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ PreservesFiniteLimits (F C)

Tactic:
have : PreservesFiniteLimits (F C) := by rw [F]; infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : PreservesFiniteLimits (F C)
⊢ PreservesFiniteLimits (C := AsSmall C) (Functor.rightOp Ind.yoneda)

Tactic:
apply preservesFiniteLimits_rightOp

Premises used: CategoryTheory.Limits.preservesFiniteLimits_rightOp
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : PreservesFiniteLimits (F C)
⊢ PreservesFiniteLimits (C := AsSmall C) (G C)

Tactic:
have : PreservesFiniteLimits (G C) := by rw [G]; apply preservesFiniteLimits_rightOp
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : PreservesFiniteLimits (F C)
this : PreservesFiniteLimits (C := AsSmall C) (G C)
⊢ PreservesFiniteLimits (C := (Ind (AsSmall C)ᵒᵖ)ᵒᵖ) (D := ModuleCat (EmbeddingRing.{v, u} C)) (H C)

Tactic:
have : PreservesFiniteLimits (H C) :=
    IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding _
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : PreservesFiniteLimits (F C)
this_2 : PreservesFiniteLimits (C := AsSmall C) (G C)
this : PreservesFiniteLimits (C := (Ind (AsSmall C)ᵒᵖ)ᵒᵖ) (D := ModuleCat (EmbeddingRing.{v, u} C)) (H C)
⊢ PreservesFiniteLimits (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ PreservesFiniteColimits (C := C) (Equivalence.functor AsSmall.equiv)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ PreservesFiniteColimits (F C)

Tactic:
have : PreservesFiniteColimits (F C) := by rw [F]; infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : PreservesFiniteColimits (F C)
⊢ PreservesFiniteColimits (C := AsSmall C) (Functor.rightOp Ind.yoneda)

Tactic:
apply preservesFiniteColimits_rightOp

Premises used: CategoryTheory.Limits.preservesFiniteColimits_rightOp
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this : PreservesFiniteColimits (F C)
⊢ PreservesFiniteColimits (C := AsSmall C) (G C)

Tactic:
have : PreservesFiniteColimits (G C) := by rw [G]; apply preservesFiniteColimits_rightOp
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : PreservesFiniteColimits (F C)
this : PreservesFiniteColimits (C := AsSmall C) (G C)
⊢ PreservesFiniteColimits (C := (Ind (AsSmall C)ᵒᵖ)ᵒᵖ) (D := ModuleCat (EmbeddingRing.{v, u} C)) (H C)

Tactic:
have : PreservesFiniteColimits (H C) :=
    IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding _
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
this_1 : PreservesFiniteColimits (F C)
this_2 : PreservesFiniteColimits (C := AsSmall C) (G C)
this : PreservesFiniteColimits (C := (Ind (AsSmall C)ᵒᵖ)ᵒᵖ) (D := ModuleCat (EmbeddingRing.{v, u} C)) (H C)
⊢ PreservesFiniteColimits (D := ModuleCat (EmbeddingRing.{v, u} C)) (F C ⋙ G C ⋙ H C)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.FreydMitchell
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ ∃ (R : Type (max u v)) (x : Ring R) (F : C ⥤ ModuleCat R),
    F.Full ∧ F.Faithful ∧ PreservesFiniteLimits F ∧ PreservesFiniteColimits F

Tactic:
⟨_, _, FreydMitchell.functor C, inferInstance, inferInstance, inferInstance, inferInstance⟩

Premises used: CategoryTheory.Abelian.FreydMitchell.functor, inferInstance, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
dsimp :
  Eq (α := (kernel α).obj X ⟶ F.obj X) (NatTrans.app (kernel.ι α) X ≫ 𝟙 (F.obj X))
    (CategoryStruct.comp (Y := kernel (α.app X)) (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) α))
      (kernel.ι (α.app X)))
⊢ Eq (α := Functor.obj (Functor.obj (evaluation C D) X) (kernel α) ⟶ F.obj X)
    (Functor.map (Functor.obj (evaluation C D) X) (kernel.ι α) ≫
      Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) F)))
    (CategoryStruct.comp (Y := kernel (α.app X)) (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) α))
      (kernel.ι (α.app X)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
simp :
  Eq (α := (kernel α).obj X ⟶ F.obj X) (NatTrans.app (kernel.ι α) X)
    (CategoryStruct.comp (Y := kernel (α.app X)) (kernelComparison α (Functor.obj (evaluation C D) X))
      (kernel.ι (α.app X)))
⊢ Eq (α := (kernel α).obj X ⟶ F.obj X) (NatTrans.app (kernel.ι α) X ≫ 𝟙 (F.obj X))
    (CategoryStruct.comp (Y := kernel (α.app X)) (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) α))
      (kernel.ι (α.app X)))

Tactic:
simp only [Category.comp_id, PreservesKernel.iso_hom]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.PreservesKernel.iso_hom
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := (kernel α).obj X ⟶ F.obj X) (NatTrans.app (kernel.ι α) X)
    (CategoryStruct.comp (Y := kernel (α.app X)) (kernelComparison α (Functor.obj (evaluation C D) X))
      (kernel.ι (α.app X)))

Tactic:
(kernelComparison_comp_ι _ ((evaluation C D).obj X)).symm

Premises used: CategoryTheory.Limits.kernelComparison_comp_ι, CategoryTheory.evaluation, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := (kernel α).obj X ⟶ F.obj X) (NatTrans.app (kernel.ι α) X)
    (CategoryStruct.comp (Y := kernel (α.app X)) (kernelComparison α (Functor.obj (evaluation C D) X))
      (kernel.ι (α.app X)))

Tactic:
exact (kernelComparison_comp_ι _ ((evaluation C D).obj X)).symm

Premises used: CategoryTheory.Limits.kernelComparison_comp_ι, CategoryTheory.evaluation, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
apply :
  Eq (α := Functor.obj (Functor.obj (evaluation C D) X) G ⟶ Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
    (CategoryStruct.comp (Y :=
      cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
      (CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
        (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α))
        (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
      (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
    (CategoryStruct.comp (Y :=
      cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
      (Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫ cokernel.π (α.app X))
      (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
⊢ Eq (α := Functor.obj (Functor.obj (evaluation C D) X) G ⟶ cokernel (α.app X))
    (CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
      (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α))
      (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
    (Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫ cokernel.π (α.app X))

Tactic:
apply (cancel_mono (PreservesCokernel.iso ((evaluation C D).obj X) α).inv).1

Premises used: CategoryTheory.Limits.PreservesCokernel.iso, CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.evaluation, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
simp :
  Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α) ≫
      𝟙 (Functor.obj (Functor.obj (evaluation C D) X) (cokernel α)) =
    Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫
      CategoryStruct.comp (Y :=
        cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
        (cokernel.π (α.app X)) (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α))
⊢ Eq (α := Functor.obj (Functor.obj (evaluation C D) X) G ⟶ Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
    (CategoryStruct.comp (Y :=
      cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
      (CategoryStruct.comp (Y := Functor.obj (Functor.obj (evaluation C D) X) (cokernel α))
        (Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α))
        (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
      (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))
    (CategoryStruct.comp (Y :=
      cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
      (Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫ cokernel.π (α.app X))
      (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)))

Tactic:
simp only [Category.assoc, Iso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
dsimp :
  NatTrans.app (cokernel.π α) X ≫ 𝟙 ((cokernel α).obj X) =
    𝟙 (G.obj X) ≫
      CategoryStruct.comp (Y := cokernel (α.app X)) (cokernel.π (α.app X))
        (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α))
⊢ Functor.map (Functor.obj (evaluation C D) X) (cokernel.π α) ≫
      𝟙 (Functor.obj (Functor.obj (evaluation C D) X) (cokernel α)) =
    Iso.hom (Iso.refl (Functor.obj (Functor.obj (evaluation C D) X) G)) ≫
      CategoryStruct.comp (Y :=
        cokernel (X := Functor.obj (Functor.obj (evaluation C D) X) F) (Functor.map (Functor.obj (evaluation C D) X) α))
        (cokernel.π (α.app X)) (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
simp :
  Eq (α := G.obj X ⟶ (cokernel α).obj X) (NatTrans.app (cokernel.π α) X)
    (CategoryStruct.comp (Y := cokernel (α.app X)) (cokernel.π (α.app X))
      (cokernelComparison α (Functor.obj (evaluation C D) X)))
⊢ NatTrans.app (cokernel.π α) X ≫ 𝟙 ((cokernel α).obj X) =
    𝟙 (G.obj X) ≫
      CategoryStruct.comp (Y := cokernel (α.app X)) (cokernel.π (α.app X))
        (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α))

Tactic:
simp only [PreservesCokernel.iso_inv, Category.id_comp, Category.comp_id]

Premises used: CategoryTheory.Limits.PreservesCokernel.iso_inv, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := G.obj X ⟶ (cokernel α).obj X) (NatTrans.app (cokernel.π α) X)
    (CategoryStruct.comp (Y := cokernel (α.app X)) (cokernel.π (α.app X))
      (cokernelComparison α (Functor.obj (evaluation C D) X)))

Tactic:
(π_comp_cokernelComparison _ ((evaluation C D).obj X)).symm

Premises used: CategoryTheory.Limits.π_comp_cokernelComparison, CategoryTheory.evaluation, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
⊢ Eq (α := G.obj X ⟶ (cokernel α).obj X) (NatTrans.app (cokernel.π α) X)
    (CategoryStruct.comp (Y := cokernel (α.app X)) (cokernel.π (α.app X))
      (cokernelComparison α (Functor.obj (evaluation C D) X)))

Tactic:
exact (π_comp_cokernelComparison _ ((evaluation C D).obj X)).symm

Premises used: CategoryTheory.Limits.π_comp_cokernelComparison, CategoryTheory.evaluation, Eq.symm, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
h :
  CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (coequalizer.π (kernel.ι (α.app X)) 0) (coimageImageComparison (α.app X)))
      (equalizer.ι (cokernel.π (α.app X)) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (coequalizer.π (kernel.ι (α.app X)) 0 ≫
        Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))
      (equalizer.ι (cokernel.π (α.app X)) 0)
⊢ Eq (α := Abelian.coimage (α.app X) ⟶ Abelian.image (α.app X)) (coimageImageComparison (α.app X))
    (Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
h :
  CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (cokernel.π (kernel.ι (α.app X))) (coimageImageComparison (α.app X)))
      (kernel.ι (cokernel.π (α.app X))) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (cokernel.π (kernel.ι (α.app X)) ≫
        Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))
      (kernel.ι (cokernel.π (α.app X)))
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (coequalizer.π (kernel.ι (α.app X)) 0) (coimageImageComparison (α.app X)))
      (equalizer.ι (cokernel.π (α.app X)) 0) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (coequalizer.π (kernel.ι (α.app X)) 0 ≫
        Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))
      (equalizer.ι (cokernel.π (α.app X)) 0)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
h :
  CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (cokernel.π (kernel.ι (α.app X))) (coimageImageComparison (α.app X)))
      (kernel.ι (cokernel.π (α.app X))) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (cokernel.π (kernel.ι (α.app X)))
        (CategoryStruct.comp (Y := (Abelian.coimage α).obj X)
          (CategoryStruct.comp (Y := cokernel (X := (kernel α).obj X) (NatTrans.app (kernel.ι α) X))
            (cokernel.desc (kernel.ι (α.app X)) (𝟙 (F.obj X) ≫ cokernel.π (NatTrans.app (kernel.ι α) X)) ⋯)
            (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) (kernel.ι α))))
          (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
            (CategoryStruct.comp (Y := kernel (Y := (cokernel α).obj X) (NatTrans.app (cokernel.π α) X))
              (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) (cokernel.π α)))
              (kernel.map (NatTrans.app (cokernel.π α) X) (cokernel.π (α.app X)) (𝟙 (G.obj X))
                (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)) ⋯)))))
      (kernel.ι (cokernel.π (α.app X)))
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (cokernel.π (kernel.ι (α.app X))) (coimageImageComparison (α.app X)))
      (kernel.ι (cokernel.π (α.app X))) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (cokernel.π (kernel.ι (α.app X)) ≫
        Iso.inv (coimageObjIso α X) ≫ NatTrans.app (coimageImageComparison α) X ≫ Iso.hom (imageObjIso α X))
      (kernel.ι (cokernel.π (α.app X)))

Tactic:
dsimp [imageObjIso, coimageObjIso, cokernel.map]

Premises used: CategoryTheory.Abelian.FunctorCategory.imageObjIso, CategoryTheory.Limits.cokernel.map, CategoryTheory.Abelian.FunctorCategory.coimageObjIso
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
h :
  α.app X =
    CategoryStruct.comp (Y := cokernel (X := (kernel α).obj X) (NatTrans.app (kernel.ι α) X))
      (cokernel.π (NatTrans.app (kernel.ι α) X))
      (CategoryStruct.comp (Y := (Abelian.coimage α).obj X)
        (cokernelComparison (kernel.ι α) (Functor.obj (evaluation C D) X))
        (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
          (CategoryStruct.comp (Y := kernel (Y := (cokernel α).obj X) (NatTrans.app (cokernel.π α) X))
            (kernelComparison (cokernel.π α) (Functor.obj (evaluation C D) X))
            (kernel.ι (NatTrans.app (cokernel.π α) X)))))
⊢ CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (cokernel.π (kernel.ι (α.app X))) (coimageImageComparison (α.app X)))
      (kernel.ι (cokernel.π (α.app X))) =
    CategoryStruct.comp (Y := equalizer (Y := cokernel (α.app X)) (cokernel.π (α.app X)) 0)
      (CategoryStruct.comp (Y := coequalizer (X := kernel (α.app X)) (kernel.ι (α.app X)) 0)
        (cokernel.π (kernel.ι (α.app X)))
        (CategoryStruct.comp (Y := (Abelian.coimage α).obj X)
          (CategoryStruct.comp (Y := cokernel (X := (kernel α).obj X) (NatTrans.app (kernel.ι α) X))
            (cokernel.desc (kernel.ι (α.app X)) (𝟙 (F.obj X) ≫ cokernel.π (NatTrans.app (kernel.ι α) X)) ⋯)
            (Iso.inv (PreservesCokernel.iso (Functor.obj (evaluation C D) X) (kernel.ι α))))
          (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
            (CategoryStruct.comp (Y := kernel (Y := (cokernel α).obj X) (NatTrans.app (cokernel.π α) X))
              (Iso.hom (PreservesKernel.iso (Functor.obj (evaluation C D) X) (cokernel.π α)))
              (kernel.map (NatTrans.app (cokernel.π α) X) (cokernel.π (α.app X)) (𝟙 (G.obj X))
                (Iso.hom (PreservesCokernel.iso (Functor.obj (evaluation C D) X) α)) ⋯)))))
      (kernel.ι (cokernel.π (α.app X)))

Tactic:
simp only [coimage_image_factorisation, PreservesKernel.iso_hom, Category.assoc,
    kernel.lift_ι, Category.comp_id, PreservesCokernel.iso_inv,
    cokernel.π_desc_assoc, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PreservesCokernel.iso_inv, CategoryTheory.Abelian.coimage_image_factorisation, CategoryTheory.Limits.cokernel.π_desc_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.PreservesKernel.iso_hom, CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.FunctorCategory
Goal:
C : Type u
inst : Category.{v, u} C
D : Type w
inst_1 : Category.{z, w} D
inst_2 : Abelian.{z, w} D
F G : Functor.{v, z, u, w} C D
α : F ⟶ G
X : C
h :
  α.app X =
    CategoryStruct.comp (Y := cokernel (X := (kernel α).obj X) (NatTrans.app (kernel.ι α) X))
      (cokernel.π (NatTrans.app (kernel.ι α) X))
      (CategoryStruct.comp (Y := (Abelian.coimage α).obj X)
        (cokernelComparison (kernel.ι α) (Functor.obj (evaluation C D) X))
        (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
          (Functor.map (Functor.obj (evaluation C D) X) (kernel.ι (cokernel.π α)))))
⊢ α.app X =
    CategoryStruct.comp (Y := cokernel (X := (kernel α).obj X) (NatTrans.app (kernel.ι α) X))
      (cokernel.π (NatTrans.app (kernel.ι α) X))
      (CategoryStruct.comp (Y := (Abelian.coimage α).obj X)
        (cokernelComparison (kernel.ι α) (Functor.obj (evaluation C D) X))
        (CategoryStruct.comp (Y := (Abelian.image α).obj X) (NatTrans.app (coimageImageComparison α) X)
          (CategoryStruct.comp (Y := kernel (Y := (cokernel α).obj X) (NatTrans.app (cokernel.π α) X))
            (kernelComparison (cokernel.π α) (Functor.obj (evaluation C D) X))
            (kernel.ι (NatTrans.app (cokernel.π α) X)))))

Tactic:
erw [kernelComparison_comp_ι _ ((evaluation C D).obj X)]

Premises used: CategoryTheory.Limits.kernelComparison_comp_ι, CategoryTheory.evaluation, CategoryTheory.Functor.obj