no goals
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ 𝟙 X ≫ 0 = 0
simp
case h
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ kernelZeroIsoSource.inv ≫ equalizer.ι 0 0 = kernel.lift 0 (𝟙 X) (_ : 𝟙 X ≫ 0 = 0) ≫ equalizer.ι 0 0
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ kernelZeroIsoSource.inv = kernel.lift 0 (𝟙 X) (_ : 𝟙 X ≫ 0 = 0)
apply equalizer.hom_ext
no goals
case h
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ kernelZeroIsoSource.inv ≫ equalizer.ι 0 0 = kernel.lift 0 (𝟙 X) (_ : 𝟙 X ≫ 0 = 0) ≫ equalizer.ι 0 0
simp [kernelZeroIsoSource]