[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.28, u_1} C
inst✝ : Abelian C
⊢ Abelian Cᵒᵖ
[PROOFSTEP]
exact
  { normalMonoOfMono := fun f => normalMonoOfNormalEpiUnop _ (normalEpiOfEpi f.unop)
    normalEpiOfEpi := fun f => normalEpiOfNormalMonoUnop _ (normalMonoOfMono f.unop) }
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f).op ≫ f.op = 0
[PROOFSTEP]
simp [← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f ≫ (kernel.ι f.op).unop = 0
[PROOFSTEP]
rw [← f.unop_op, ← unop_comp, f.unop_op]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι f.op ≫ f.op).unop = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)).unop ≫
      cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0) =
    𝟙 (kernel f.op).unop
[PROOFSTEP]
rw [← unop_id, ← (cokernel.desc f _ _).unop_op, ← unop_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ ((cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0)).op ≫
        kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)).unop =
    (𝟙 (kernel f.op)).unop
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0)).op ≫
      kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0) =
    𝟙 (kernel f.op)
[PROOFSTEP]
ext
[GOAL]
case e_f.h
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ ((cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0)).op ≫
        kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)) ≫
      equalizer.ι f.op 0 =
    𝟙 (kernel f.op) ≫ equalizer.ι f.op 0
[PROOFSTEP]
simp [← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0) ≫
      (kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)).unop =
    𝟙 (cokernel f)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.2286, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ coequalizer.π f 0 ≫
      cokernel.desc f (kernel.ι f.op).unop (_ : f ≫ (kernel.ι f.op).unop = 0) ≫
        (kernel.lift f.op (cokernel.π f).op (_ : (f ≫ cokernel.π f).op = 0)).unop =
    coequalizer.π f 0 ≫ 𝟙 (cokernel f)
[PROOFSTEP]
simp [← unop_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f.op).unop ≫ f = 0
[PROOFSTEP]
rw [← f.unop_op, ← unop_comp, f.unop_op]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (f.op ≫ cokernel.π f.op).unop = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f.op ≫ (kernel.ι f).op = 0
[PROOFSTEP]
simp [← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0) ≫
      (cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0)).unop =
    𝟙 (cokernel f.op).unop
[PROOFSTEP]
rw [← unop_id, ← (kernel.lift f _ _).unop_op, ← unop_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0) ≫
        (kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0)).op).unop =
    (𝟙 (cokernel f.op)).unop
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0) ≫
      (kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0)).op =
    𝟙 (cokernel f.op)
[PROOFSTEP]
ext
[GOAL]
case e_f.h
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ coequalizer.π f.op 0 ≫
      cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0) ≫
        (kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0)).op =
    coequalizer.π f.op 0 ≫ 𝟙 (cokernel f.op)
[PROOFSTEP]
simp [← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0)).unop ≫
      kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0) =
    𝟙 (kernel f)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{?u.7588, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ ((cokernel.desc f.op (kernel.ι f).op (_ : (kernel.ι f ≫ f).op = 0)).unop ≫
        kernel.lift f (cokernel.π f.op).unop (_ : (cokernel.π f.op).unop ≫ f = 0)) ≫
      equalizer.ι f 0 =
    𝟙 (kernel f) ≫ equalizer.ι f 0
[PROOFSTEP]
simp [← unop_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f.op).unop = (cokernelOpUnop f).hom ≫ kernel.ι f ≫ eqToHom (_ : X = (Opposite.op X).unop)
[PROOFSTEP]
simp [cokernelOpUnop]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι f.op).unop = eqToHom (_ : (Opposite.op Y).unop = Y) ≫ cokernel.π f ≫ (kernelOpUnop f).inv
[PROOFSTEP]
simp [kernelOpUnop]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι g.unop).op = eqToHom (_ : Opposite.op B.unop = B) ≫ cokernel.π g ≫ (kernelUnopOp g).inv
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π g.unop).op = (cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (image.ι g.unop).op ≫ (imageUnopOp g).hom = factorThruImage g
[PROOFSTEP]
simp only [imageUnopOp, Iso.trans, Iso.symm, Iso.op, cokernelOpOp_inv, cokernelEpiComp_hom, cokernelCompIsIso_hom,
  Abelian.coimageIsoImage'_hom, ← Category.assoc, ← op_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (((((kernel.lift (cokernel.π g.unop) (cokernel.π (cokernel.π g.unop).op).unop
                    (_ : (cokernel.π (cokernel.π g.unop).op).unop ≫ cokernel.π g.unop = 0) ≫
                  (Abelian.imageIsoImage g.unop).hom) ≫
                image.ι g.unop).op ≫
            (cokernelIsoOfEq
                (_ :
                  (cokernel.π g.unop).op =
                    (cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop))).hom) ≫
          cokernel.desc ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop))
            (cokernel.π (kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)))
            (_ :
              ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)) ≫
                  cokernel.π (kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)) =
                0)) ≫
        cokernel.desc (kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop))
          (inv (eqToHom (_ : A = Opposite.op A.unop)) ≫ cokernel.π (kernel.ι g))
          (_ :
            (kernel.ι g ≫ eqToHom (_ : A = Opposite.op A.unop)) ≫
                inv (eqToHom (_ : A = Opposite.op A.unop)) ≫ cokernel.π (kernel.ι g) =
              0)) ≫
      cokernel.desc (kernel.ι g) (factorThruImage g) (_ : kernel.ι g ≫ factorThruImage g = 0) =
    factorThruImage g
[PROOFSTEP]
simp only [Category.assoc, Abelian.imageIsoImage_hom_comp_image_ι, kernel.lift_ι, Quiver.Hom.op_unop,
  cokernelIsoOfEq_hom_comp_desc_assoc, cokernel.π_desc_assoc, cokernel.π_desc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (eqToHom (_ : A = Opposite.op A.unop)) ≫ factorThruImage g = factorThruImage g
[PROOFSTEP]
simp only [eqToHom_refl]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (𝟙 A) ≫ factorThruImage g = factorThruImage g
[PROOFSTEP]
erw [IsIso.inv_id, Category.id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (imageUnopOp g).hom ≫ image.ι g = (factorThruImage g.unop).op
[PROOFSTEP]
simp only [← cancel_epi (image.ι g.unop).op, ← Category.assoc, image_ι_op_comp_imageUnopOp_hom, ← op_comp, image.fac,
  Quiver.Hom.op_unop]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ factorThruImage g ≫ (imageUnopOp g).inv = (image.ι g.unop).op
[PROOFSTEP]
rw [Iso.comp_inv_eq, image_ι_op_comp_imageUnopOp_hom]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (imageUnopOp g).inv ≫ (factorThruImage g.unop).op = image.ι g
[PROOFSTEP]
rw [Iso.inv_comp_eq, imageUnopOp_hom_comp_image_ι]
