no goals
ι : Type ?u.17286
V : Type u
inst✝⁴ : Category 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
simpa using w
case h
ι : Type ?u.17286
V : Type u
inst✝⁴ : Category 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)
ι : Type ?u.17286
V : Type u
inst✝⁴ : Category 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)
ext
no goals
case h
ι : Type ?u.17286
V : Type u
inst✝⁴ : Category 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)
simp