no goals
ι : Type ?u.10958
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
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ f ≫ g ≫ h = 0
simp [reassoc_of% w]
case h
ι : Type ?u.10958
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
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))
ι : Type ?u.10958
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
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))
ext
no goals
case h
ι : Type ?u.10958
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
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))
simp