no goals
V : Type ?u.24
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.op ≫ f.op = 0
rw [← op_comp, w, op_zero]
no goals
V : Type ?u.24
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_2
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op (_ : g.op ≫ f.op = 0) ≫ Subobject.arrow (kernelSubobject f.op) =
    ((imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).op ≫
          (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv) ≫
      Subobject.arrow (kernelSubobject f.op)
V : Type u_2
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op (_ : g.op ≫ f.op = 0) =
    (imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
      (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).op ≫
        (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv
ext
case h
V : Type u_2
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (imageSubobjectIso g.op).hom ≫ (imageUnopOp g.op).inv ≫ (factorThruImage g.op.unop).op =
    (imageSubobjectIso g.op).hom ≫ (imageOpOp g).inv ≫ (factorThruImage g).op
case h
V : Type u_2
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op (_ : g.op ≫ f.op = 0) ≫ Subobject.arrow (kernelSubobject f.op) =
    ((imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) (_ : f ≫ factorThruImage g = 0)).op ≫
          (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv) ≫
      Subobject.arrow (kernelSubobject f.op)
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelOpOp_inv, Category.assoc,
  imageToKernel_arrow, kernelSubobject_arrow', kernel.lift_ι, ← op_comp, cokernel.π_desc,
  ← imageSubobject_arrow, ← imageUnopOp_inv_comp_op_factorThruImage g.op]
no goals
case h
V : Type u_2
inst✝¹ : Category V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (imageSubobjectIso g.op).hom ≫ (imageUnopOp g.op).inv ≫ (factorThruImage g.op.unop).op =
    (imageSubobjectIso g.op).hom ≫ (imageOpOp g).inv ≫ (factorThruImage g).op
rfl