A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (kernelSubobjectIso g).hom ≫
      cokernel.π (kernel.lift g f w) ≫
        ((cokernelIsoOfEq (_ : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w)).inv ≫
            cokernel.desc (factorThruImage f ≫ imageToKernel' f g w) (cokernel.π (imageToKernel' f g w))
              (_ : (factorThruImage f ≫ imageToKernel' f g w) ≫ cokernel.π (imageToKernel' f g w) = 0)) ≫
          (homologyIsoCokernelImageToKernel' f g w).inv =
    π f g w
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (kernelSubobjectIso g).hom ≫ π' f g w = π f g w
dsimp [π', homologyIsoCokernelLift]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ ((((kernelSubobjectIso g).hom ≫ cokernel.π (kernel.lift g f w)) ≫
          (cokernelIsoOfEq (_ : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w)).inv) ≫
        cokernel.desc (factorThruImage f ≫ imageToKernel' f g w) (cokernel.π (imageToKernel' f g w))
          (_ : (factorThruImage f ≫ imageToKernel' f g w) ≫ cokernel.π (imageToKernel' f g w) = 0)) ≫
      (homologyIsoCokernelImageToKernel' f g w).inv =
    π f g w
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (kernelSubobjectIso g).hom ≫
      cokernel.π (kernel.lift g f w) ≫
        ((cokernelIsoOfEq (_ : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w)).inv ≫
            cokernel.desc (factorThruImage f ≫ imageToKernel' f g w) (cokernel.π (imageToKernel' f g w))
              (_ : (factorThruImage f ≫ imageToKernel' f g w) ≫ cokernel.π (imageToKernel' f g w) = 0)) ≫
          (homologyIsoCokernelImageToKernel' f g w).inv =
    π f g w
simp only [← Category.assoc]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (((kernelSubobjectIso g).hom ≫ cokernel.π (kernel.lift g f w)) ≫
        (cokernelIsoOfEq (_ : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w)).inv) ≫
      cokernel.desc (factorThruImage f ≫ imageToKernel' f g w) (cokernel.π (imageToKernel' f g w))
        (_ : (factorThruImage f ≫ imageToKernel' f g w) ≫ cokernel.π (imageToKernel' f g w) = 0) =
    π f g w ≫ (homologyIsoCokernelImageToKernel' f g w).hom
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ ((((kernelSubobjectIso g).hom ≫ cokernel.π (kernel.lift g f w)) ≫
          (cokernelIsoOfEq (_ : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w)).inv) ≫
        cokernel.desc (factorThruImage f ≫ imageToKernel' f g w) (cokernel.π (imageToKernel' f g w))
          (_ : (factorThruImage f ≫ imageToKernel' f g w) ≫ cokernel.π (imageToKernel' f g w) = 0)) ≫
      (homologyIsoCokernelImageToKernel' f g w).inv =
    π f g w
rw [Iso.comp_inv_eq]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (((kernelSubobjectIso g).hom ≫ cokernel.π (kernel.lift g f w)) ≫
        (cokernelIsoOfEq (_ : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w)).inv) ≫
      cokernel.desc (factorThruImage f ≫ imageToKernel' f g w) (cokernel.π (imageToKernel' f g w))
        (_ : (factorThruImage f ≫ imageToKernel' f g w) ≫ cokernel.π (imageToKernel' f g w) = 0) =
    cokernel.π (imageToKernel f g w) ≫
      cokernel.map (imageToKernel f g w) (imageToKernel' f g w) (imageSubobjectIso f).hom (kernelSubobjectIso g).hom
        (_ : imageToKernel f g w ≫ (kernelSubobjectIso g).hom = (imageSubobjectIso f).hom ≫ imageToKernel' f g w)
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (((kernelSubobjectIso g).hom ≫ cokernel.π (kernel.lift g f w)) ≫
        (cokernelIsoOfEq (_ : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w)).inv) ≫
      cokernel.desc (factorThruImage f ≫ imageToKernel' f g w) (cokernel.π (imageToKernel' f g w))
        (_ : (factorThruImage f ≫ imageToKernel' f g w) ≫ cokernel.π (imageToKernel' f g w) = 0) =
    π f g w ≫ (homologyIsoCokernelImageToKernel' f g w).hom
dsimp [π, homologyIsoCokernelImageToKernel']
no goals
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (((kernelSubobjectIso g).hom ≫ cokernel.π (kernel.lift g f w)) ≫
        (cokernelIsoOfEq (_ : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w)).inv) ≫
      cokernel.desc (factorThruImage f ≫ imageToKernel' f g w) (cokernel.π (imageToKernel' f g w))
        (_ : (factorThruImage f ≫ imageToKernel' f g w) ≫ cokernel.π (imageToKernel' f g w) = 0) =
    cokernel.π (imageToKernel f g w) ≫
      cokernel.map (imageToKernel f g w) (imageToKernel' f g w) (imageSubobjectIso f).hom (kernelSubobjectIso g).hom
        (_ : imageToKernel f g w ≫ (kernelSubobjectIso g).hom = (imageSubobjectIso f).hom ≫ imageToKernel' f g w)
simp