[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ kernel.lift g f w ≫ kernel.ι g = f
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ Mono (imageToKernel f g w)
[PROOFSTEP]
dsimp only [imageToKernel]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ Mono (Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g))
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ imageToKernel f g w ≫ Subobject.arrow (kernelSubobject g) = Subobject.arrow (imageSubobject f)
[PROOFSTEP]
simp [imageToKernel]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝² : HasImage f
g : B ⟶ C
inst✝¹ : HasKernel g
inst✝ : ConcreteCategory V
w : f ≫ g = 0
x : (forget V).obj (Subobject.underlying.obj (imageSubobject f))
⊢ ↑(Subobject.arrow (kernelSubobject g)) (↑(imageToKernel f g w) x) = ↑(Subobject.arrow (imageSubobject f)) x
[PROOFSTEP]
rw [← comp_apply, imageToKernel_arrow]
  -- This is less useful as a `simp` lemma than it initially appears,
  -- as it "loses" the information the morphism factors through the image.
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ factorThruImageSubobject f ≫ imageToKernel f g w = factorThruKernelSubobject g f w
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ (factorThruImageSubobject f ≫ imageToKernel f g w) ≫ Subobject.arrow (kernelSubobject g) =
    factorThruKernelSubobject g f w ≫ Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasZeroObject V
w : 0 ≫ g = 0
⊢ imageToKernel 0 g w = 0
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasZeroObject V
w : 0 ≫ g = 0
⊢ imageToKernel 0 g w ≫ Subobject.arrow (kernelSubobject g) = 0 ≫ Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w = Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w ≫ Subobject.arrow (kernelSubobject 0) =
    (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))) ≫
      Subobject.arrow (kernelSubobject 0)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ f ≫ g ≫ h = 0
[PROOFSTEP]
simp [reassoc_of% w]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) =
    imageToKernel f g w ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h))
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫ Subobject.arrow (kernelSubobject (g ≫ h)) =
    (imageToKernel f g w ≫
        Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h))
          (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h))) ≫
      Subobject.arrow (kernelSubobject (g ≫ h))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ (h ≫ f) ≫ g = 0
[PROOFSTEP]
simp [w]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ imageToKernel (h ≫ f) g (_ : (h ≫ f) ≫ g = 0) =
    Subobject.ofLE (imageSubobject (h ≫ f)) (imageSubobject f) (_ : imageSubobject (h ≫ f) ≤ imageSubobject f) ≫
      imageToKernel f g w
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ imageToKernel (h ≫ f) g (_ : (h ≫ f) ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) =
    (Subobject.ofLE (imageSubobject (h ≫ f)) (imageSubobject f) (_ : imageSubobject (h ≫ f) ≤ imageSubobject f) ≫
        imageToKernel f g w) ≫
      Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ (f ≫ g) ≫ h = 0 ≫ h
[PROOFSTEP]
simpa using w
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ imageToKernel f (g ≫ h) w =
    imageToKernel f g (_ : f ≫ g = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).inv
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ imageToKernel f (g ≫ h) w ≫ Subobject.arrow (kernelSubobject (g ≫ h)) =
    (imageToKernel f g (_ : f ≫ g = 0) ≫
        (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
            (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).inv) ≫
      Subobject.arrow (kernelSubobject (g ≫ h))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ h ≫ f ≫ g = h ≫ 0
[PROOFSTEP]
simpa using w
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ imageToKernel (h ≫ f) g w =
    Subobject.ofLE (imageSubobject (h ≫ f)) (imageSubobject f) (_ : imageSubobject (h ≫ f) ≤ imageSubobject f) ≫
      imageToKernel f g (_ : f ≫ g = 0)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ imageToKernel (h ≫ f) g w ≫ Subobject.arrow (kernelSubobject g) =
    (Subobject.ofLE (imageSubobject (h ≫ f)) (imageSubobject f) (_ : imageSubobject (h ≫ f) ≤ imageSubobject f) ≫
        imageToKernel f g (_ : f ≫ g = 0)) ≫
      Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ f ≫ g = 0
[PROOFSTEP]
simpa using w
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ imageToKernel (f ≫ i.hom) (i.inv ≫ g) w =
    (imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g (_ : f ≫ g = 0) ≫ (kernelSubobjectIsoComp i.inv g).inv
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ imageToKernel (f ≫ i.hom) (i.inv ≫ g) w ≫ Subobject.arrow (kernelSubobject (i.inv ≫ g)) =
    ((imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g (_ : f ≫ g = 0) ≫ (kernelSubobjectIsoComp i.inv g).inv) ≫
      Subobject.arrow (kernelSubobject (i.inv ≫ g))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasZeroObject V
inst✝ : Mono g
⊢ 0 ≫ g = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
⊢ f ≫ 0 = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
⊢ Epi (imageToKernel f 0 (_ : f ≫ 0 = 0))
[PROOFSTEP]
simp only [imageToKernel_zero_right]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
⊢ Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
[PROOFSTEP]
haveI := epi_image_of_epi f
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
this : Epi (image.ι f)
⊢ Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
[PROOFSTEP]
rw [← imageSubobject_arrow]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
this : Epi (image.ι f)
⊢ Epi (((imageSubobjectIso f).hom ≫ image.ι f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
[PROOFSTEP]
refine' @epi_comp _ _ _ _ _ _ (epi_comp _ _) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝² : HasImage f
g : B ⟶ C
inst✝¹ : HasKernel g
w : f ≫ g = 0
inst✝ : HasCokernel (imageToKernel f g w)
D : V
k : Subobject.underlying.obj (kernelSubobject g) ⟶ D
p : imageToKernel f g w ≫ k = 0
⊢ π f g w ≫ desc f g w k p = k
[PROOFSTEP]
simp [homology.π, homology.desc]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝⁶ : HasImage f
g : B ⟶ C
inst✝⁵ : HasKernel g
w : f ≫ g = 0
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f 0 (_ : f ≫ 0 = 0))
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ imageToKernel f 0 (_ : f ≫ 0 = 0) ≫ (kernelSubobjectIso 0 ≪≫ kernelZeroIsoSource).hom =
    (imageSubobjectIso f).hom ≫ image.ι f
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝⁵ : HasImage f
g : B ⟶ C
inst✝⁴ : HasKernel g
w : f ≫ g = 0
inst✝³ : HasCokernel (imageToKernel f g w)
inst✝² : HasZeroObject V
inst✝¹ : HasImage 0
inst✝ : HasCokernel (imageToKernel 0 0 (_ : 0 ≫ 0 = 0))
⊢ imageToKernel 0 0 (_ : 0 ≫ 0 = 0) ≫ Subobject.arrow (kernelSubobject 0) = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁴ : Category.{v, u} V
inst✝¹³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹² : HasImage f
g : B ⟶ C
inst✝¹¹ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁰ : HasImage f'
g' : B' ⟶ C'
inst✝⁹ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝⁸ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝⁷ : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝⁶ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝⁵ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁴ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝³ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝² : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝¹ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
p : α.right = β.left
⊢ imageToKernel f g w ≫ kernelSubobjectMap β = imageSubobjectMap α ≫ imageToKernel f' g' w'
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹⁴ : Category.{v, u} V
inst✝¹³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹² : HasImage f
g : B ⟶ C
inst✝¹¹ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁰ : HasImage f'
g' : B' ⟶ C'
inst✝⁹ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝⁸ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝⁷ : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝⁶ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝⁵ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁴ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝³ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝² : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝¹ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
p : α.right = β.left
⊢ (imageToKernel f g w ≫ kernelSubobjectMap β) ≫ Subobject.arrow (kernelSubobject g') =
    (imageSubobjectMap α ≫ imageToKernel f' g' w') ≫ Subobject.arrow (kernelSubobject g')
[PROOFSTEP]
simp [p]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
⊢ imageToKernel f g w ≫ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') = 0
[PROOFSTEP]
rw [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
⊢ imageSubobjectMap α ≫ imageToKernel f' g' w' ≫ cokernel.π (imageToKernel f' g' w') = 0
[PROOFSTEP]
simp only [cokernel.condition, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
⊢ π f g w ≫ map w w' α β p = kernelSubobjectMap β ≫ π f' g' w'
[PROOFSTEP]
simp only [homology.π, homology.map, cokernel.π_desc]
[GOAL]
ι : Type u_1
V : Type u
inst✝²⁰ : Category.{v, u} V
inst✝¹⁹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁸ : HasImage f
g : B ⟶ C
inst✝¹⁷ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁶ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁵ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹⁴ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹³ : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹² : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹¹ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝¹⁰ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁹ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁸ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁷ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁶ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁵ : HasCokernel (imageToKernel f g w)
inst✝⁴ : HasCokernel (imageToKernel f' g' w')
inst✝³ : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝² : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝¹ : HasCokernel (imageToKernel f₃ g₃ w₃)
inst✝ : ConcreteCategory V
p : α.right = β.left
x : (forget V).obj (Subobject.underlying.obj (kernelSubobject g))
⊢ ↑(map w w' α β p) (↑(π f g w) x) = ↑(π f' g' w') (↑(kernelSubobjectMap β) x)
[PROOFSTEP]
simp only [← comp_apply, homology.π_map w w' α β p]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
D : V
k : Subobject.underlying.obj (kernelSubobject g') ⟶ D
z : imageToKernel f' g' w' ≫ k = 0
⊢ imageToKernel f g w ≫ kernelSubobjectMap β ≫ k = 0
[PROOFSTEP]
simp only [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p, z, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
D : V
k : Subobject.underlying.obj (kernelSubobject g') ⟶ D
z : imageToKernel f' g' w' ≫ k = 0
⊢ map w w' α β p ≫ desc f' g' w' k z =
    desc f g w (kernelSubobjectMap β ≫ k) (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ k = 0)
[PROOFSTEP]
ext
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
D : V
k : Subobject.underlying.obj (kernelSubobject g') ⟶ D
z : imageToKernel f' g' w' ≫ k = 0
⊢ π f g w ≫ map w w' α β p ≫ desc f' g' w' k z =
    π f g w ≫ desc f g w (kernelSubobjectMap β ≫ k) (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ k = 0)
[PROOFSTEP]
simp only [homology.π_desc, homology.π_map_assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
⊢ map w w (𝟙 (Arrow.mk f)) (𝟙 (Arrow.mk g)) (_ : (𝟙 (Arrow.mk f)).right = (𝟙 (Arrow.mk f)).right) = 𝟙 (homology f g w)
[PROOFSTEP]
ext
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
⊢ π f g w ≫ map w w (𝟙 (Arrow.mk f)) (𝟙 (Arrow.mk g)) (_ : (𝟙 (Arrow.mk f)).right = (𝟙 (Arrow.mk f)).right) =
    π f g w ≫ 𝟙 (homology f g w)
[PROOFSTEP]
simp only [homology.π_map, kernelSubobjectMap_id, Category.id_comp, Category.comp_id]
[GOAL]
ι : Type u_1
V✝ : Type u
inst✝²⁰ : Category.{v, u} V✝
inst✝¹⁹ : HasZeroMorphisms V✝
A B C : V✝
f : A ⟶ B
inst✝¹⁸ : HasImage f
g : B ⟶ C
inst✝¹⁷ : HasKernel g
w : f ≫ g = 0
A' B' C' : V✝
f' : A' ⟶ B'
inst✝¹⁶ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁵ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹⁴ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁✝ B₁✝ C₁✝ : V✝
f₁✝ : A₁✝ ⟶ B₁✝
inst✝¹³ : HasImage f₁✝
g₁✝ : B₁✝ ⟶ C₁✝
inst✝¹² : HasKernel g₁✝
w₁ : f₁✝ ≫ g₁✝ = 0
A₂✝ B₂✝ C₂✝ : V✝
f₂✝ : A₂✝ ⟶ B₂✝
inst✝¹¹ : HasImage f₂✝
g₂✝ : B₂✝ ⟶ C₂✝
inst✝¹⁰ : HasKernel g₂✝
w₂ : f₂✝ ≫ g₂✝ = 0
A₃✝ B₃✝ C₃✝ : V✝
f₃✝ : A₃✝ ⟶ B₃✝
inst✝⁹ : HasImage f₃✝
g₃✝ : B₃✝ ⟶ C₃✝
inst✝⁸ : HasKernel g₃✝
w₃ : f₃✝ ≫ g₃✝ = 0
α₁✝ : Arrow.mk f₁✝ ⟶ Arrow.mk f₂✝
inst✝⁷ : HasImageMap α₁✝
β₁✝ : Arrow.mk g₁✝ ⟶ Arrow.mk g₂✝
α₂✝ : Arrow.mk f₂✝ ⟶ Arrow.mk f₃✝
inst✝⁶ : HasImageMap α₂✝
β₂✝ : Arrow.mk g₂✝ ⟶ Arrow.mk g₃✝
inst✝⁵ : HasCokernel (imageToKernel f g w)
inst✝⁴ : HasCokernel (imageToKernel f' g' w')
inst✝³ : HasCokernel (imageToKernel f₁✝ g₁✝ w₁)
inst✝² : HasCokernel (imageToKernel f₂✝ g₂✝ w₂)
inst✝¹ : HasCokernel (imageToKernel f₃✝ g₃✝ w₃)
V : Type u_2
inst✝ : Category.{u_3, u_2} V
A₁ B₁ C₁ A₂ B₂ C₂ A₃ B₃ C₃ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
f₃ : A₃ ⟶ B₃
g₃ : B₃ ⟶ C₃
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
p₁ : α₁.right = β₁.left
p₂ : α₂.right = β₂.left
⊢ (α₁ ≫ α₂).right = (β₁ ≫ β₂).left
[PROOFSTEP]
simp only [Arrow.comp_left, Arrow.comp_right, p₁, p₂]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p₁ : α₁.right = β₁.left
p₂ : α₂.right = β₂.left
⊢ map w₁ w₂ α₁ β₁ p₁ ≫ map w₂ w₃ α₂ β₂ p₂ = map w₁ w₃ (α₁ ≫ α₂) (β₁ ≫ β₂) (_ : (α₁ ≫ α₂).right = (β₁ ≫ β₂).left)
[PROOFSTEP]
ext
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p₁ : α₁.right = β₁.left
p₂ : α₂.right = β₂.left
⊢ π f₁ g₁ w₁ ≫ map w₁ w₂ α₁ β₁ p₁ ≫ map w₂ w₃ α₂ β₂ p₂ =
    π f₁ g₁ w₁ ≫ map w₁ w₃ (α₁ ≫ α₂) (β₁ ≫ β₂) (_ : (α₁ ≫ α₂).right = (β₁ ≫ β₂).left)
[PROOFSTEP]
simp only [kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, Category.assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.inv.right = β.inv.left
[PROOFSTEP]
rw [← cancel_mono α.hom.right, ← Comma.comp_right, α.inv_hom_id, Comma.id_right, p, ← Comma.comp_left, β.inv_hom_id,
  Comma.id_left]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ 𝟙 (Arrow.mk f₂).right = 𝟙 (Arrow.mk g₂).left
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ map w₁ w₂ α.hom β.hom p ≫ map w₂ w₁ α.inv β.inv (_ : α.inv.right = β.inv.left) = 𝟙 (homology f₁ g₁ w₁)
[PROOFSTEP]
rw [homology.map_comp, ← homology.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ map w₁ w₁ (α.hom ≫ α.inv) (β.hom ≫ β.inv) (_ : (α.hom ≫ α.inv).right = (β.hom ≫ β.inv).left) =
    map w₁ w₁ (𝟙 (Arrow.mk f₁)) (𝟙 (Arrow.mk g₁)) (_ : (𝟙 (Arrow.mk f₁)).right = (𝟙 (Arrow.mk f₁)).right)
[PROOFSTEP]
congr
[GOAL]
case e_α
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.hom ≫ α.inv = 𝟙 (Arrow.mk f₁)
[PROOFSTEP]
simp only [Iso.hom_inv_id]
[GOAL]
case e_β
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ β.hom ≫ β.inv = 𝟙 (Arrow.mk g₁)
[PROOFSTEP]
simp only [Iso.hom_inv_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ map w₂ w₁ α.inv β.inv (_ : α.inv.right = β.inv.left) ≫ map w₁ w₂ α.hom β.hom p = 𝟙 (homology f₂ g₂ w₂)
[PROOFSTEP]
rw [homology.map_comp, ← homology.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ map w₂ w₂ (α.inv ≫ α.hom) (β.inv ≫ β.hom) (_ : (α.inv ≫ α.hom).right = (β.inv ≫ β.hom).left) =
    map w₂ w₂ (𝟙 (Arrow.mk f₂)) (𝟙 (Arrow.mk g₂)) (_ : (𝟙 (Arrow.mk f₂)).right = (𝟙 (Arrow.mk f₂)).right)
[PROOFSTEP]
congr
[GOAL]
case e_α
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.inv ≫ α.hom = 𝟙 (Arrow.mk f₂)
[PROOFSTEP]
simp only [Iso.inv_hom_id]
[GOAL]
case e_β
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ β.inv ≫ β.hom = 𝟙 (Arrow.mk g₂)
[PROOFSTEP]
simp only [Iso.inv_hom_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ (𝟭 V).map (𝟙 (Arrow.mk f).left) ≫ (Arrow.mk f').hom = (Arrow.mk f).hom ≫ (𝟭 V).map (𝟙 (Arrow.mk f).right)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ (𝟭 V).map (𝟙 (Arrow.mk g).left) ≫ (Arrow.mk g').hom = (Arrow.mk g).hom ≫ (𝟭 V).map (𝟙 (Arrow.mk g).right)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ (𝟭 V).map (𝟙 (Arrow.mk f').left) ≫ (Arrow.mk f).hom = (Arrow.mk f').hom ≫ (𝟭 V).map (𝟙 (Arrow.mk f').right)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ (𝟭 V).map (𝟙 (Arrow.mk g').left) ≫ (Arrow.mk g).hom = (Arrow.mk g').hom ≫ (𝟭 V).map (𝟙 (Arrow.mk g').right)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g').left) (𝟙 (Arrow.mk g').right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right)).right) =
    𝟙 (homology f g w)
[PROOFSTEP]
obtain rfl := pf
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
g' : B ⟶ C
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pg : g = g'
w' : f ≫ g' = 0
⊢ map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g').left) (𝟙 (Arrow.mk g').right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f g w)
[PROOFSTEP]
obtain rfl := pg
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f g w)
[PROOFSTEP]
rw [homology.map_comp, ← homology.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ map w w
      (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
        CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
      (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
        CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
      (_ :
        (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
              CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
          (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
              CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right)).left) =
    map w w (𝟙 (Arrow.mk f)) (𝟙 (Arrow.mk g)) (_ : (𝟙 (Arrow.mk f)).right = (𝟙 (Arrow.mk f)).right)
[PROOFSTEP]
congr
[GOAL]
case e_α
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
      CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) =
    𝟙 (Arrow.mk f)
[PROOFSTEP]
aesop_cat
[GOAL]
case e_β
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
      CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) =
    𝟙 (Arrow.mk g)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g').left) (𝟙 (Arrow.mk g').right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right)).right) ≫
      map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f' g' w')
[PROOFSTEP]
obtain rfl := pf
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
g' : B ⟶ C
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pg : g = g'
w' : f ≫ g' = 0
⊢ map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g').left) (𝟙 (Arrow.mk g').right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f g' w')
[PROOFSTEP]
obtain rfl := pg
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f g w')
[PROOFSTEP]
rw [homology.map_comp, ← homology.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ map w' w'
      (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
        CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
      (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
        CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
      (_ :
        (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
              CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
          (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
              CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right)).left) =
    map w' w' (𝟙 (Arrow.mk f)) (𝟙 (Arrow.mk g)) (_ : (𝟙 (Arrow.mk f)).right = (𝟙 (Arrow.mk f)).right)
[PROOFSTEP]
congr
[GOAL]
case e_α
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
      CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) =
    𝟙 (Arrow.mk f)
[PROOFSTEP]
aesop_cat
[GOAL]
case e_β
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
      CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) =
    𝟙 (Arrow.mk g)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ image.ι f ≫ g = 0
[PROOFSTEP]
ext
[GOAL]
case w
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ factorThruImage f ≫ image.ι f ≫ g = factorThruImage f ≫ 0
[PROOFSTEP]
simpa using w
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageSubobjectIso f).hom ≫ imageToKernel' f g w = imageToKernel f g w ≫ (kernelSubobjectIso g).hom
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ ((imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 =
    (imageToKernel f g w ≫ (kernelSubobjectIso g).hom) ≫ equalizer.ι g 0
[PROOFSTEP]
simp [imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageToKernel' f g w ≫ (kernelSubobjectIso g).inv) ≫ Subobject.arrow (kernelSubobject g) =
    ((imageSubobjectIso f).inv ≫ imageToKernel f g w) ≫ Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp [imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ imageToKernel f g w ≫ (kernelSubobjectIso g).hom = (imageSubobjectIso f).hom ≫ imageToKernel' f g w
[PROOFSTEP]
simp only [imageSubobjectIso_imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w
[PROOFSTEP]
simp only [imageToKernel'_kernelSubobjectIso]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ 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) ≫
      cokernel.map (imageToKernel' f g w) (imageToKernel f g w) (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
        (_ : imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w) =
    𝟙 (homology f g w)
[PROOFSTEP]
apply coequalizer.hom_ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ coequalizer.π (imageToKernel f g w) 0 ≫
      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) ≫
        cokernel.map (imageToKernel' f g w) (imageToKernel f g w) (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
          (_ : imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w) =
    coequalizer.π (imageToKernel f g w) 0 ≫ 𝟙 (homology f g w)
[PROOFSTEP]
simp only [Iso.hom_inv_id_assoc, cokernel.π_desc, cokernel.π_desc_assoc, Category.assoc, coequalizer_as_cokernel]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ cokernel.π (imageToKernel f g w) = cokernel.π (imageToKernel f g w) ≫ 𝟙 (homology f g w)
[PROOFSTEP]
exact (Category.comp_id _).symm
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ cokernel.map (imageToKernel' f g w) (imageToKernel f g w) (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
        (_ : imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ 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) =
    𝟙 (cokernel (imageToKernel' f g w))
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ coequalizer.π (imageToKernel' f g w) 0 ≫
      cokernel.map (imageToKernel' f g w) (imageToKernel f g w) (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
          (_ : imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ 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) =
    coequalizer.π (imageToKernel' f g w) 0 ≫ 𝟙 (cokernel (imageToKernel' f g w))
[PROOFSTEP]
simp only [Iso.inv_hom_id_assoc, cokernel.π_desc, Category.comp_id, cokernel.π_desc_assoc, Category.assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
⊢ homology f g w ≅ cokernel (kernel.lift g f w)
[PROOFSTEP]
refine' homologyIsoCokernelImageToKernel' f g w ≪≫ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
⊢ cokernel (imageToKernel' f g w) ≅ cokernel (kernel.lift g f w)
[PROOFSTEP]
have p : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w :=
  by
  ext
  simp [imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
⊢ factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
⊢ (factorThruImage f ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 = kernel.lift g f w ≫ equalizer.ι g 0
[PROOFSTEP]
simp [imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
p : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w
⊢ cokernel (imageToKernel' f g w) ≅ cokernel (kernel.lift g f w)
[PROOFSTEP]
exact (cokernelEpiComp _ _).symm ≪≫ cokernelIsoOfEq p
