no goals
V : Type ?u.7533
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.unop ≫ f.unop = 0
rw [← unop_comp, w, unop_zero]
no goals
V : Type ?u.7533
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ factorThruImage g = 0
rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]
case h
V : Type u_1
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop (_ : g.unop ≫ f.unop = 0) ≫ Subobject.arrow (kernelSubobject f.unop) =
    ((imageSubobjectIso g.unop ≪≫ (imageUnopUnop g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).unop ≫
          (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv) ≫
      Subobject.arrow (kernelSubobject f.unop)
V : Type u_1
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop (_ : g.unop ≫ f.unop = 0) =
    (imageSubobjectIso g.unop ≪≫ (imageUnopUnop g).symm).hom ≫
      (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).unop ≫
        (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv
ext
case h
V : Type u_1
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop (_ : g.unop ≫ f.unop = 0) ≫ Subobject.arrow (kernelSubobject f.unop) =
    ((imageSubobjectIso g.unop ≪≫ (Iso.unop (imageUnopOp g)).symm).hom ≫
        (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).unop ≫
          (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv) ≫
      Subobject.arrow (kernelSubobject f.unop)
case h
V : Type u_1
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop (_ : g.unop ≫ f.unop = 0) ≫ Subobject.arrow (kernelSubobject f.unop) =
    ((imageSubobjectIso g.unop ≪≫ (imageUnopUnop g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).unop ≫
          (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv) ≫
      Subobject.arrow (kernelSubobject f.unop)
dsimp only [imageUnopUnop]
no goals
case h
V : Type u_1
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop (_ : g.unop ≫ f.unop = 0) ≫ Subobject.arrow (kernelSubobject f.unop) =
    ((imageSubobjectIso g.unop ≪≫ (Iso.unop (imageUnopOp g)).symm).hom ≫
        (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).unop ≫
          (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv) ≫
      Subobject.arrow (kernelSubobject f.unop)
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelUnopUnop_inv, Category.assoc,
  imageToKernel_arrow, kernelSubobject_arrow', kernel.lift_ι, cokernel.π_desc, Iso.unop_inv,
  ← unop_comp, factorThruImage_comp_imageUnopOp_inv, Quiver.Hom.unop_op, imageSubobject_arrow]