-- Mathlib/CategoryTheory/Abelian/FunctorCategory.lean
theorem coimageImageComparison_app :
    coimageImageComparison (α.app X) =
      (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom

Proof state:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (cokernel.π (kernel.ι (α.app X)) ≫ coimageImageComparison (α.app X)) ≫ kernel.ι (cokernel.π (α.app X)) =
    (cokernel.π (kernel.ι (α.app X)) ≫
        (cokernel.desc (kernel.ι (α.app X)) (𝟙 (F.obj X) ≫ cokernel.π ((kernel.ι α).app X)) ⋯ ≫
            (PreservesCokernel.iso ((evaluation C D).obj X) (kernel.ι α)).inv) ≫
          (coimageImageComparison α).app X ≫
            (PreservesKernel.iso ((evaluation C D).obj X) (cokernel.π α)).hom ≫
              kernel.map ((cokernel.π α).app X) (cokernel.π (α.app X)) (𝟙 (G.obj X))
                (PreservesCokernel.iso ((evaluation C D).obj X) α).hom ⋯) ≫
      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]

Result:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ α.app X =
    cokernel.π ((kernel.ι α).app X) ≫
      cokernelComparison (kernel.ι α) ((evaluation C D).obj X) ≫
        (coimageImageComparison α).app X ≫
          kernelComparison (cokernel.π α) ((evaluation C D).obj X) ≫ kernel.ι ((cokernel.π α).app X)

Proof state:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ α.app X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))

Tactic:
conv_lhs => rw [← coimage_image_factorisation α]

Result:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coimage.π α ≫ coimageImageComparison α ≫ image.ι α).app X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))

Proof state:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coequalizer.π (kernel.ι (α.app X)) 0 ≫ coimageImageComparison (α.app X)) ≫ equalizer.ι (cokernel.π (α.app X)) 0 =
    (coequalizer.π (kernel.ι (α.app X)) 0 ≫
        (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom) ≫
      equalizer.ι (cokernel.π (α.app X)) 0

Tactic:
dsimp

Result:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (cokernel.π (kernel.ι (α.app X)) ≫ coimageImageComparison (α.app X)) ≫ kernel.ι (cokernel.π (α.app X)) =
    (cokernel.π (kernel.ι (α.app X)) ≫
        (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom) ≫
      kernel.ι (cokernel.π (α.app X))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ coimageImageComparison (α.app X) = (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom

Tactic:
ext

Result:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coequalizer.π (kernel.ι (α.app X)) 0 ≫ coimageImageComparison (α.app X)) ≫ equalizer.ι (cokernel.π (α.app X)) 0 =
    (coequalizer.π (kernel.ι (α.app X)) 0 ≫
        (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom) ≫
      equalizer.ι (cokernel.π (α.app X)) 0

Proof state:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coimage.π α ≫ coimageImageComparison α ≫ image.ι α).app X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))

Tactic:
rfl

Result:
no goals

Proof state:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (cokernel.π (kernel.ι (α.app X)) ≫ coimageImageComparison (α.app X)) ≫ kernel.ι (cokernel.π (α.app X)) =
    (cokernel.π (kernel.ι (α.app X)) ≫
        (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom) ≫
      kernel.ι (cokernel.π (α.app X))

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

Result:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (cokernel.π (kernel.ι (α.app X)) ≫ coimageImageComparison (α.app X)) ≫ kernel.ι (cokernel.π (α.app X)) =
    (cokernel.π (kernel.ι (α.app X)) ≫
        (cokernel.desc (kernel.ι (α.app X)) (𝟙 (F.obj X) ≫ cokernel.π ((kernel.ι α).app X)) ⋯ ≫
            (PreservesCokernel.iso ((evaluation C D).obj X) (kernel.ι α)).inv) ≫
          (coimageImageComparison α).app X ≫
            (PreservesKernel.iso ((evaluation C D).obj X) (cokernel.π α)).hom ≫
              kernel.map ((cokernel.π α).app X) (cokernel.π (α.app X)) (𝟙 (G.obj X))
                (PreservesCokernel.iso ((evaluation C D).obj X) α).hom ⋯) ≫
      kernel.ι (cokernel.π (α.app X))

Proof state:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ α.app X =
    cokernel.π ((kernel.ι α).app X) ≫
      cokernelComparison (kernel.ι α) ((evaluation C D).obj X) ≫
        (coimageImageComparison α).app X ≫
          kernelComparison (cokernel.π α) ((evaluation C D).obj X) ≫ kernel.ι ((cokernel.π α).app X)

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

Result:
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ α.app X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      (coimageImageComparison α).app X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))