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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ g ≫ β.right = α.right ≫ g'
simp [h, β.w.symm]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (fun e => (kernelSubobjectIso g).hom ≫ e) (π' f g w ≫ map w w' α β h) =
    (fun e => (kernelSubobjectIso g).hom ≫ e)
      (kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w')

case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ Function.Injective fun e => (kernelSubobjectIso g).hom ≫ e
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ π' f g w ≫ map w w' α β h = kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w'
apply_fun fun e => (kernelSubobjectIso _).hom ≫ e
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ Function.Injective fun e => (kernelSubobjectIso g).hom ≫ e

A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (fun e => (kernelSubobjectIso g).hom ≫ e) (π' f g w ≫ map w w' α β h) =
    (fun e => (kernelSubobjectIso g).hom ≫ e)
      (kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (fun e => (kernelSubobjectIso g).hom ≫ e) (π' f g w ≫ map w w' α β h) =
    (fun e => (kernelSubobjectIso g).hom ≫ e)
      (kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w')

case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ Function.Injective fun e => (kernelSubobjectIso g).hom ≫ e
swap
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (kernelSubobjectIso g).hom ≫
      π' f g w ≫
        cokernel.desc (imageToKernel f g w) (kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w'))
          (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') = 0) =
    (kernelSubobjectIso g).hom ≫ kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (fun e => (kernelSubobjectIso g).hom ≫ e) (π' f g w ≫ map w w' α β h) =
    (fun e => (kernelSubobjectIso g).hom ≫ e)
      (kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w')
dsimp [map]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ π f g w ≫
      cokernel.desc (imageToKernel f g w) (kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w'))
        (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') = 0) =
    (kernelSubobjectIso g).hom ≫ kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (kernelSubobjectIso g).hom ≫
      π' f g w ≫
        cokernel.desc (imageToKernel f g w) (kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w'))
          (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') = 0) =
    (kernelSubobjectIso g).hom ≫ kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w'
simp only [π'_eq_π_assoc]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ cokernel.π (imageToKernel f g w) ≫
      cokernel.desc (imageToKernel f g w) (kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w'))
        (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') = 0) =
    (kernelSubobjectIso g).hom ≫ kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ π f g w ≫
      cokernel.desc (imageToKernel f g w) (kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w'))
        (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') = 0) =
    (kernelSubobjectIso g).hom ≫ kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w'
dsimp [π]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') =
    (kernelSubobjectIso g).hom ≫ kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ cokernel.π (imageToKernel f g w) ≫
      cokernel.desc (imageToKernel f g w) (kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w'))
        (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') = 0) =
    (kernelSubobjectIso g).hom ≫ kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w'
simp only [cokernel.π_desc]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ ((kernelSubobjectIso g).inv ≫ kernelSubobjectMap β) ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') =
    (kernelSubobjectIso g).hom ≫ kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w'
rw [← Iso.inv_comp_eq, ← 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ ((kernelSubobjectIso g).inv ≫ kernelSubobjectMap β) ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ ((kernelSubobjectIso g).inv ≫ kernelSubobjectMap β) ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w'
have :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map _ _ β.left β.right β.w.symm ≫ (kernelSubobjectIso _).inv := by
  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]
  refine Limits.equalizer.hom_ext ?_
  dsimp
  simp
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ (kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
          (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
        (kernelSubobjectIso (Arrow.mk g').hom).inv) ≫
      cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ ((kernelSubobjectIso g).inv ≫ kernelSubobjectMap β) ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' f' g' w'
rw [this]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ (kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
          (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
        (kernelSubobjectIso (Arrow.mk g').hom).inv) ≫
      cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ kernel.map g g' β.left β.right (_ : g ≫ β.right = β.left ≫ g') ≫
      (kernelSubobjectIso g').inv ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫
      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
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫ π' 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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ kernel.map g g' β.left β.right (_ : g ≫ β.right = β.left ≫ g') ≫
      (kernelSubobjectIso g').inv ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫
      cokernel.π (imageToKernel' f' g' w') ≫ (homologyIsoCokernelImageToKernel' f' g' w').inv
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ kernel.map g g' β.left β.right (_ : g ≫ β.right = β.left ≫ g') ≫
      (kernelSubobjectIso g').inv ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫
      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
simp only [cokernelIsoOfEq_inv_comp_desc, cokernel.π_desc_assoc]
case e_a
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ kernel.map g g' β.left β.right (_ : g ≫ β.right = β.left ≫ g') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g')

case e_a
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ (kernelSubobjectIso g').inv ≫ cokernel.π (imageToKernel f' g' w') =
    cokernel.π (imageToKernel' f' g' w') ≫ (homologyIsoCokernelImageToKernel' f' g' w').inv
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ kernel.map g g' β.left β.right (_ : g ≫ β.right = β.left ≫ g') ≫
      (kernelSubobjectIso g').inv ≫ cokernel.π (imageToKernel f' g' w') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g') ≫
      cokernel.π (imageToKernel' f' g' w') ≫ (homologyIsoCokernelImageToKernel' f' g' w').inv
congr 1
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
i j : kernel g ⟶ homology f' g' w'
hh : (fun e => (kernelSubobjectIso g).hom ≫ e) i = (fun e => (kernelSubobjectIso g).hom ≫ e) j
⊢ i = j
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ Function.Injective fun e => (kernelSubobjectIso g).hom ≫ e
intro i j hh
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
i j : kernel g ⟶ homology f' g' w'
hh :
  (kernelSubobjectIso g).inv ≫ (fun e => (kernelSubobjectIso g).hom ≫ e) i =
    (kernelSubobjectIso g).inv ≫ (fun e => (kernelSubobjectIso g).hom ≫ e) j
⊢ i = j
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
i j : kernel g ⟶ homology f' g' w'
hh : (fun e => (kernelSubobjectIso g).hom ≫ e) i = (fun e => (kernelSubobjectIso g).hom ≫ e) j
⊢ i = j
apply_fun fun e => (kernelSubobjectIso _).inv ≫ e  at hh
no goals
case inj
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
i j : kernel g ⟶ homology f' g' w'
hh :
  (kernelSubobjectIso g).inv ≫ (fun e => (kernelSubobjectIso g).hom ≫ e) i =
    (kernelSubobjectIso g).inv ≫ (fun e => (kernelSubobjectIso g).hom ≫ e) j
⊢ i = j
simpa using hh
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ kernelSubobjectMap β ≫ (kernelSubobjectIso (Arrow.mk g').hom).hom =
    (kernelSubobjectIso g).hom ≫
      kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom)
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (kernelSubobjectMap β ≫ (kernelSubobjectIso (Arrow.mk g').hom).hom) ≫ equalizer.ι (Arrow.mk g').hom 0 =
    ((kernelSubobjectIso g).hom ≫
        kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
          (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom)) ≫
      equalizer.ι (Arrow.mk g').hom 0
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ kernelSubobjectMap β ≫ (kernelSubobjectIso (Arrow.mk g').hom).hom =
    (kernelSubobjectIso g).hom ≫
      kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom)
refine Limits.equalizer.hom_ext ?_
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (kernelSubobjectMap β ≫ (kernelSubobjectIso g').hom) ≫ kernel.ι g' =
    ((kernelSubobjectIso g).hom ≫ kernel.map g g' β.left β.right (_ : g ≫ β.right = β.left ≫ g')) ≫ kernel.ι g'
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (kernelSubobjectMap β ≫ (kernelSubobjectIso (Arrow.mk g').hom).hom) ≫ equalizer.ι (Arrow.mk g').hom 0 =
    ((kernelSubobjectIso g).hom ≫
        kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
          (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom)) ≫
      equalizer.ι (Arrow.mk g').hom 0
dsimp
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
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
⊢ (kernelSubobjectMap β ≫ (kernelSubobjectIso g').hom) ≫ kernel.ι g' =
    ((kernelSubobjectIso g).hom ≫ kernel.map g g' β.left β.right (_ : g ≫ β.right = β.left ≫ g')) ≫ kernel.ι g'
simp
case e_a.e_p
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ β.left = α.right
case e_a
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ kernel.map g g' β.left β.right (_ : g ≫ β.right = β.left ≫ g') =
    kernel.map g g' α.right β.right (_ : g ≫ β.right = α.right ≫ g')
congr
no goals
case e_a.e_p
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ β.left = α.right
exact h.symm
case e_a
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ cokernel.π (imageToKernel f' g' w') ≫ (homologyIsoCokernelImageToKernel' f' g' w').hom =
    (kernelSubobjectIso g').hom ≫ cokernel.π (imageToKernel' f' g' w')
case e_a
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ (kernelSubobjectIso g').inv ≫ cokernel.π (imageToKernel f' g' w') =
    cokernel.π (imageToKernel' f' g' w') ≫ (homologyIsoCokernelImageToKernel' f' g' w').inv
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]
case e_a
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ 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') =
    (kernelSubobjectIso g').hom ≫ cokernel.π (imageToKernel' f' g' w')
case e_a
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ cokernel.π (imageToKernel f' g' w') ≫ (homologyIsoCokernelImageToKernel' f' g' w').hom =
    (kernelSubobjectIso g').hom ≫ cokernel.π (imageToKernel' f' g' w')
dsimp [homologyIsoCokernelImageToKernel']
no goals
case e_a
A : Type u
inst✝¹ : Category A
inst✝ : Abelian A
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
X' Y' Z' : A
f' : X' ⟶ Y'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
β : Arrow.mk g ⟶ Arrow.mk g'
h : α.right = β.left
this :
  (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
    kernel.map (Arrow.mk g).hom (Arrow.mk g').hom β.left β.right
        (_ : (Arrow.mk g).hom ≫ (𝟭 A).map β.right = (𝟭 A).map β.left ≫ (Arrow.mk g').hom) ≫
      (kernelSubobjectIso (Arrow.mk g').hom).inv
⊢ 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') =
    (kernelSubobjectIso g').hom ≫ cokernel.π (imageToKernel' f' g' w')
simp