no goals
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ g = 0
⊢ e ≫ f = 0
simp [h, he]
case refl
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
Z : C
f : X ⟶ Y
inst✝¹ : HasKernel f
e : Z ⟶ X
inst✝ : HasKernel f
he : e ≫ f = 0
⊢ kernel.lift f e he ≫ (kernelIsoOfEq (_ : f = f)).inv = kernel.lift f e (_ : e ≫ f = 0)
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ g = 0
⊢ kernel.lift g e he ≫ (kernelIsoOfEq h).inv = kernel.lift f e (_ : e ≫ f = 0)
cases h
no goals
case refl
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
Z : C
f : X ⟶ Y
inst✝¹ : HasKernel f
e : Z ⟶ X
inst✝ : HasKernel f
he : e ≫ f = 0
⊢ kernel.lift f e he ≫ (kernelIsoOfEq (_ : f = f)).inv = kernel.lift f e (_ : e ≫ f = 0)
simp