case refl
C : Type u
inst✝⁵ : Category C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝³ : HasKernel f✝
f h : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel h
inst✝ : HasKernel f
w₂ : f = h
⊢ kernelIsoOfEq (_ : f = f) ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq (_ : f = h)
C : Type u
inst✝⁵ : Category C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝³ : HasKernel f✝
f g h : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel g
inst✝ : HasKernel h
w₁ : f = g
w₂ : g = h
⊢ kernelIsoOfEq w₁ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq (_ : f = h)
cases w₁
case refl.refl
C : Type u
inst✝⁵ : Category C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝³ : HasKernel f✝
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasKernel f
⊢ kernelIsoOfEq (_ : f = f) ≪≫ kernelIsoOfEq (_ : f = f) = kernelIsoOfEq (_ : f = f)
case refl
C : Type u
inst✝⁵ : Category C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝³ : HasKernel f✝
f h : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel h
inst✝ : HasKernel f
w₂ : f = h
⊢ kernelIsoOfEq (_ : f = f) ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq (_ : f = h)
cases w₂
case refl.refl.w.h
C : Type u
inst✝⁵ : Category C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝³ : HasKernel f✝
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq (_ : f = f) ≪≫ kernelIsoOfEq (_ : f = f)).hom ≫ equalizer.ι f 0 =
    (kernelIsoOfEq (_ : f = f)).hom ≫ equalizer.ι f 0
case refl.refl
C : Type u
inst✝⁵ : Category C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝³ : HasKernel f✝
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasKernel f
⊢ kernelIsoOfEq (_ : f = f) ≪≫ kernelIsoOfEq (_ : f = f) = kernelIsoOfEq (_ : f = f)
ext
no goals
case refl.refl.w.h
C : Type u
inst✝⁵ : Category C
inst✝⁴ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝³ : HasKernel f✝
f : X ⟶ Y
inst✝² inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq (_ : f = f) ≪≫ kernelIsoOfEq (_ : f = f)).hom ≫ equalizer.ι f 0 =
    (kernelIsoOfEq (_ : f = f)).hom ≫ equalizer.ι f 0
simp [kernelIsoOfEq]