no goals
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map h ≫ G.map f = 0
simp only [← G.map_comp, w, Functor.map_zero]
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ (G.map (kernel.lift f h w) ≫ kernelComparison f G) ≫ equalizer.ι (G.map f) 0 =
    kernel.lift (G.map f) (G.map h) (_ : G.map h ≫ G.map f = 0) ≫ equalizer.ι (G.map f) 0
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map (kernel.lift f h w) ≫ kernelComparison f G = kernel.lift (G.map f) (G.map h) (_ : G.map h ≫ G.map f = 0)
apply equalizer.hom_ext
no goals
case h
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : Functor.PreservesZeroMorphisms G
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ (G.map (kernel.lift f h w) ≫ kernelComparison f G) ≫ equalizer.ι (G.map f) 0 =
    kernel.lift (G.map f) (G.map h) (_ : G.map h ≫ G.map f = 0) ≫ equalizer.ι (G.map f) 0
simp [← G.map_comp]