C : Type u_2
inst✝¹ : Category 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 = A.unop.op))).hom) ≫
          cokernel.desc ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = A.unop.op))
            (cokernel.π (kernel.ι g ≫ eqToHom (_ : A = A.unop.op)))
            (_ :
              ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = A.unop.op)) ≫
                  cokernel.π (kernel.ι g ≫ eqToHom (_ : A = A.unop.op)) =
                0)) ≫
        cokernel.desc (kernel.ι g ≫ eqToHom (_ : A = A.unop.op))
          (inv (eqToHom (_ : A = A.unop.op)) ≫ cokernel.π (kernel.ι g))
          (_ :
            (kernel.ι g ≫ eqToHom (_ : A = A.unop.op)) ≫ inv (eqToHom (_ : A = A.unop.op)) ≫ cokernel.π (kernel.ι g) =
              0)) ≫
      cokernel.desc (kernel.ι g) (factorThruImage g) (_ : kernel.ι g ≫ factorThruImage g = 0) =
    factorThruImage g
C : Type u_2
inst✝¹ : Category 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
simp only [imageUnopOp, Iso.trans, Iso.symm, Iso.op, cokernelOpOp_inv, cokernelEpiComp_hom,
  cokernelCompIsIso_hom, Abelian.coimageIsoImage'_hom, ← Category.assoc, ← op_comp]
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (eqToHom (_ : A = A.unop.op)) ≫ factorThruImage g = factorThruImage g
C : Type u_2
inst✝¹ : Category 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 = A.unop.op))).hom) ≫
          cokernel.desc ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = A.unop.op))
            (cokernel.π (kernel.ι g ≫ eqToHom (_ : A = A.unop.op)))
            (_ :
              ((cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom (_ : A = A.unop.op)) ≫
                  cokernel.π (kernel.ι g ≫ eqToHom (_ : A = A.unop.op)) =
                0)) ≫
        cokernel.desc (kernel.ι g ≫ eqToHom (_ : A = A.unop.op))
          (inv (eqToHom (_ : A = A.unop.op)) ≫ cokernel.π (kernel.ι g))
          (_ :
            (kernel.ι g ≫ eqToHom (_ : A = A.unop.op)) ≫ inv (eqToHom (_ : A = A.unop.op)) ≫ cokernel.π (kernel.ι g) =
              0)) ≫
      cokernel.desc (kernel.ι g) (factorThruImage g) (_ : kernel.ι g ≫ factorThruImage g = 0) =
    factorThruImage g
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]
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (𝟙 A) ≫ factorThruImage g = factorThruImage g
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (eqToHom (_ : A = A.unop.op)) ≫ factorThruImage g = factorThruImage g
simp only [eqToHom_refl]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ inv (𝟙 A) ≫ factorThruImage g = factorThruImage g
erw [IsIso.inv_id, Category.id_comp]