case h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ coequalizer.π (kernel.ι (α.app X)) 0 ≫ coimageImageComparison (α.app X) =
    coequalizer.π (kernel.ι (α.app X)) 0 ≫
      (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ coimageImageComparison (α.app X) = (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom
apply coequalizer.hom_ext
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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
case h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ coequalizer.π (kernel.ι (α.app X)) 0 ≫ coimageImageComparison (α.app X) =
    coequalizer.π (kernel.ι (α.app X)) 0 ≫
      (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom
apply equalizer.hom_ext
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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))
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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
dsimp
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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))
              (_ : kernel.ι (α.app X) ≫ 𝟙 (F.obj X) ≫ cokernel.π ((kernel.ι α).app X) = 0) ≫
            (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
                (_ :
                  ((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom =
                    (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (α.app X))) ≫
      kernel.ι (cokernel.π (α.app X))
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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))
dsimp [imageObjIso, coimageObjIso, cokernel.map]
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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)
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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))
              (_ : kernel.ι (α.app X) ≫ 𝟙 (F.obj X) ≫ cokernel.π ((kernel.ι α).app X) = 0) ≫
            (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
                (_ :
                  ((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom =
                    (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (α.app X))) ≫
      kernel.ι (cokernel.π (α.app X))
simp only [coimage_image_factorisation, PreservesKernel.iso_hom, Category.assoc,
  kernel.lift_ι, Category.comp_id, PreservesCokernel.iso_inv,
  cokernel.π_desc_assoc, Category.id_comp]
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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.π α))
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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)
erw [kernelComparison_comp_ι _ ((evaluation C D).obj X),
  π_comp_cokernelComparison_assoc _ ((evaluation C D).obj X)]
no goals
case h.h
C : Type u
inst✝² : Category C
D : Type w
inst✝¹ : Category 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.π α))
conv_lhs => rw [← coimage_image_factorisation α]