[GOAL]
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
⊢ ((evaluation C D).obj X).map (kernel.ι α) ≫ (Iso.refl (((evaluation C D).obj X).obj F)).hom =
    (PreservesKernel.iso ((evaluation C D).obj X) α).hom ≫ kernel.ι (NatTrans.app α X)
[PROOFSTEP]
dsimp
[GOAL]
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
⊢ NatTrans.app (kernel.ι α) X ≫ 𝟙 (F.obj X) =
    (PreservesKernel.iso ((evaluation C D).obj X) α).hom ≫ kernel.ι (NatTrans.app α X)
[PROOFSTEP]
simp only [Category.comp_id, PreservesKernel.iso_hom]
[GOAL]
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
⊢ NatTrans.app (kernel.ι α) X = kernelComparison α ((evaluation C D).obj X) ≫ kernel.ι (NatTrans.app α X)
[PROOFSTEP]
exact (kernelComparison_comp_ι _ ((evaluation C D).obj X)).symm
[GOAL]
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
⊢ ((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.π (NatTrans.app α X)
[PROOFSTEP]
apply (cancel_mono (PreservesCokernel.iso ((evaluation C D).obj X) α).inv).1
[GOAL]
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
⊢ (((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom) ≫
      (PreservesCokernel.iso ((evaluation C D).obj X) α).inv =
    ((Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (NatTrans.app α X)) ≫
      (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
[PROOFSTEP]
simp only [Category.assoc, Iso.hom_inv_id]
[GOAL]
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
⊢ ((evaluation C D).obj X).map (cokernel.π α) ≫ 𝟙 (((evaluation C D).obj X).obj (cokernel α)) =
    (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫
      cokernel.π (NatTrans.app α X) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
[PROOFSTEP]
dsimp
[GOAL]
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
⊢ NatTrans.app (cokernel.π α) X ≫ 𝟙 ((cokernel α).obj X) =
    𝟙 (G.obj X) ≫ cokernel.π (NatTrans.app α X) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
[PROOFSTEP]
simp only [PreservesCokernel.iso_inv, Category.id_comp, Category.comp_id]
[GOAL]
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
⊢ NatTrans.app (cokernel.π α) X = cokernel.π (NatTrans.app α X) ≫ cokernelComparison α ((evaluation C D).obj X)
[PROOFSTEP]
exact (π_comp_cokernelComparison _ ((evaluation C D).obj X)).symm
[GOAL]
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 (NatTrans.app α X) =
    (coimageObjIso α X).inv ≫ NatTrans.app (coimageImageComparison α) X ≫ (imageObjIso α X).hom
[PROOFSTEP]
ext
[GOAL]
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.ι (NatTrans.app α X)) 0 ≫ coimageImageComparison (NatTrans.app α X)) ≫
      equalizer.ι (cokernel.π (NatTrans.app α X)) 0 =
    (coequalizer.π (kernel.ι (NatTrans.app α X)) 0 ≫
        (coimageObjIso α X).inv ≫ NatTrans.app (coimageImageComparison α) X ≫ (imageObjIso α X).hom) ≫
      equalizer.ι (cokernel.π (NatTrans.app α X)) 0
[PROOFSTEP]
dsimp
[GOAL]
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.ι (NatTrans.app α X)) ≫ coimageImageComparison (NatTrans.app α X)) ≫
      kernel.ι (cokernel.π (NatTrans.app α X)) =
    (cokernel.π (kernel.ι (NatTrans.app α X)) ≫
        (coimageObjIso α X).inv ≫ NatTrans.app (coimageImageComparison α) X ≫ (imageObjIso α X).hom) ≫
      kernel.ι (cokernel.π (NatTrans.app α X))
[PROOFSTEP]
dsimp [imageObjIso, coimageObjIso, cokernel.map]
[GOAL]
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.ι (NatTrans.app α X)) ≫ coimageImageComparison (NatTrans.app α X)) ≫
      kernel.ι (cokernel.π (NatTrans.app α X)) =
    (cokernel.π (kernel.ι (NatTrans.app α X)) ≫
        (cokernel.desc (kernel.ι (NatTrans.app α X)) (𝟙 (F.obj X) ≫ cokernel.π (NatTrans.app (kernel.ι α) X))
              (_ : kernel.ι (NatTrans.app α X) ≫ 𝟙 (F.obj X) ≫ cokernel.π (NatTrans.app (kernel.ι α) X) = 0) ≫
            (PreservesCokernel.iso ((evaluation C D).obj X) (kernel.ι α)).inv) ≫
          NatTrans.app (coimageImageComparison α) X ≫
            (PreservesKernel.iso ((evaluation C D).obj X) (cokernel.π α)).hom ≫
              kernel.map (NatTrans.app (cokernel.π α) X) (cokernel.π (NatTrans.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.π (NatTrans.app α X))) ≫
      kernel.ι (cokernel.π (NatTrans.app α X))
[PROOFSTEP]
simp only [coimage_image_factorisation, PreservesKernel.iso_hom, Category.assoc, kernel.lift_ι, Category.comp_id,
  PreservesCokernel.iso_inv, cokernel.π_desc_assoc, Category.id_comp]
[GOAL]
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
⊢ NatTrans.app α X =
    cokernel.π (NatTrans.app (kernel.ι α) X) ≫
      cokernelComparison (kernel.ι α) ((evaluation C D).obj X) ≫
        NatTrans.app (coimageImageComparison α) X ≫
          kernelComparison (cokernel.π α) ((evaluation C D).obj X) ≫ kernel.ι (NatTrans.app (cokernel.π α) X)
[PROOFSTEP]
erw [kernelComparison_comp_ι _ ((evaluation C D).obj X), π_comp_cokernelComparison_assoc _ ((evaluation C D).obj X)]
[GOAL]
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
⊢ NatTrans.app α X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      NatTrans.app (coimageImageComparison α) X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))
[PROOFSTEP]
conv_lhs => rw [← coimage_image_factorisation α]
[GOAL]
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
| NatTrans.app α X
[PROOFSTEP]
rw [← coimage_image_factorisation α]
[GOAL]
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
| NatTrans.app α X
[PROOFSTEP]
rw [← coimage_image_factorisation α]
[GOAL]
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
| NatTrans.app α X
[PROOFSTEP]
rw [← coimage_image_factorisation α]
[GOAL]
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
⊢ NatTrans.app (coimageImageComparison α) X =
    (coimageObjIso α X).hom ≫ coimageImageComparison (NatTrans.app α X) ≫ (imageObjIso α X).inv
[PROOFSTEP]
simp only [coimageImageComparison_app, Iso.hom_inv_id_assoc, Iso.hom_inv_id, Category.assoc, Category.comp_id]
[GOAL]
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
⊢ IsIso (coimageImageComparison α)
[PROOFSTEP]
have : ∀ X : C, IsIso ((Abelian.coimageImageComparison α).app X) :=
  by
  intros
  rw [coimageImageComparison_app']
  infer_instance
[GOAL]
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
⊢ ∀ (X : C), IsIso (NatTrans.app (coimageImageComparison α) X)
[PROOFSTEP]
intros
[GOAL]
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 X✝ : C
⊢ IsIso (NatTrans.app (coimageImageComparison α) X✝)
[PROOFSTEP]
rw [coimageImageComparison_app']
[GOAL]
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 X✝ : C
⊢ IsIso ((coimageObjIso α X✝).hom ≫ coimageImageComparison (NatTrans.app α X✝) ≫ (imageObjIso α X✝).inv)
[PROOFSTEP]
infer_instance
[GOAL]
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
this : ∀ (X : C), IsIso (NatTrans.app (coimageImageComparison α) X)
⊢ IsIso (coimageImageComparison α)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
