awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasKernel f
inst_3 : HasImage f
inst_4 : HasKernel (Y := image f) (factorThruImage f)
⊢ Eq (α := kernel (Y := image f) (factorThruImage f) ⟶ X)
    (CategoryStruct.comp (Y := kernel f) (Iso.hom (kernelFactorThruImage f)) (kernel.ι f))
    (kernel.ι (factorThruImage f))

Tactic:
simp [kernelFactorThruImage]

Premises used: CategoryTheory.Limits.kernelFactorThruImage
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasKernel f
inst_3 : HasImage f
inst_4 : HasKernel (Y := image f) (factorThruImage f)
⊢ Eq (α := kernel f ⟶ X)
    (CategoryStruct.comp (Y := kernel (Y := image f) (factorThruImage f)) (Iso.inv (kernelFactorThruImage f))
      (kernel.ι (factorThruImage f)))
    (kernel.ι f)

Tactic:
simp [kernelFactorThruImage]

Premises used: CategoryTheory.Limits.kernelFactorThruImage
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
⊢ IsIso.{v, u} (C := C) (X := Y) (Y := cokernel.{v, u} (X := X) (Y := Y) 0) (π 0)

Tactic:
coequalizer.π_of_self _

Premises used: CategoryTheory.Limits.coequalizer.π_of_self
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasCokernel f
inst_4 : HasKernel (Y := cokernel f) (cokernel.π f)
inst_5 : Epi f
⊢ IsIso (X := kernel (Y := cokernel f) (cokernel.π f)) (ι (cokernel.π f))

Tactic:
equalizer.ι_of_eq <| cokernel.π_of_epi f

Premises used: CategoryTheory.Limits.equalizer.ι_of_eq, CategoryTheory.Limits.cokernel.π_of_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasKernel f
inst_4 : HasCokernel (X := kernel f) (kernel.ι f)
inst_5 : Mono f
⊢ IsIso (Y := cokernel (X := kernel f) (kernel.ι f)) (π (kernel.ι f))

Tactic:
coequalizer.π_of_eq <| kernel.ι_of_mono f

Premises used: CategoryTheory.Limits.kernel.ι_of_mono, CategoryTheory.Limits.coequalizer.π_of_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
⊢ Eq (α := X ⟶ 0) (f ≫ 0) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
s : Cofork f 0
rw :
  Eq.{v + 1} (α := Y ⟶ s.pt)
    (CategoryStruct.comp (Y := Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      (Cofork.π (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      ((fun (x : Cofork f 0) ↦
          (0 : Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⟶ x.pt))
        s))
    0
rw₁ rw₂ : Eq.{v + 1} (α := Y ⟶ s.pt) 0 0
⊢ CategoryStruct.comp (Y := Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      (Cofork.π (CokernelCofork.ofπ (Z := 0) 0 ⋯))
      ((fun (x : Cofork f 0) ↦
          (0 : Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⟶ x.pt))
        s) =
    s.π

Tactic:
rw [hf _ _ (CokernelCofork.condition s), comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.CokernelCofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
s : Cofork f 0
m : Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Z := 0) 0 ⋯) ≫ m = s.π
⊢ m =
    (fun (x : Cofork f 0) ↦
        (0 : Cocone.pt.{0, v, 0, u} (F := parallelPair f 0) (CokernelCofork.ofπ (Z := 0) 0 ⋯) ⟶ x.pt))
      s

Tactic:
apply HasZeroObject.from_zero_ext

Premises used: CategoryTheory.Limits.HasZeroObject.from_zero_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ Y
i : X ≅ Z
h : i.hom ≫ l = f
s : CokernelCofork f
hs : IsColimit s
⊢ l ≫ Cofork.π s = 0

Tactic:
simp [i.eq_inv_comp.2 h]

Premises used: Iff.mpr, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ Y
i : X ≅ Z
h : i.hom ≫ l = f
s_1 : CokernelCofork f
hs : IsColimit s_1
s : Cofork l 0
⊢ f ≫ s.π = 0

Tactic:
simp [← h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ Y
i : X ≅ Z
h : i.hom ≫ l = f
s_1 : CokernelCofork f
hs : IsColimit s_1
s : Cofork l 0
⊢ CategoryStruct.comp (Y := Cocone.pt (F := parallelPair l 0) (CokernelCofork.ofπ (Cofork.π s_1) ⋯))
      (Cofork.π (CokernelCofork.ofπ (Cofork.π s_1) ⋯))
      ((fun (s : Cofork l 0) ↦ (hs.desc (CokernelCofork.ofπ s.π ⋯) : s_1.pt ⟶ (CokernelCofork.ofπ s.π ⋯).pt)) s) =
    s.π

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ Y
i : X ≅ Z
h_1 : i.hom ≫ l = f
s_1 : CokernelCofork f
hs : IsColimit s_1
s : Cofork l 0
m : Cocone.pt (F := parallelPair l 0) (CokernelCofork.ofπ (Cofork.π s_1) ⋯) ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π s_1) ⋯) ≫ m = s.π
apply :
  Cofork.π s_1 ≫ m =
    Cofork.π s_1 ≫
      (fun (s : Cofork l 0) ↦ (hs.desc (CokernelCofork.ofπ s.π ⋯) : s_1.pt ⟶ (CokernelCofork.ofπ s.π ⋯).pt)) s
⊢ m = (fun (s : Cofork l 0) ↦ (hs.desc (CokernelCofork.ofπ s.π ⋯) : s_1.pt ⟶ (CokernelCofork.ofπ s.π ⋯).pt)) s

Tactic:
apply Cofork.IsColimit.hom_ext hs

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ Y
i : X ≅ Z
h_1 : i.hom ≫ l = f
s_1 : CokernelCofork f
hs : IsColimit s_1
s : Cofork l 0
m : Cocone.pt (F := parallelPair l 0) (CokernelCofork.ofπ (Cofork.π s_1) ⋯) ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π s_1) ⋯) ≫ m = s.π
⊢ Cofork.π s_1 ≫ m =
    Cofork.π s_1 ≫
      (fun (s : Cofork l 0) ↦ (hs.desc (CokernelCofork.ofπ s.π ⋯) : s_1.pt ⟶ (CokernelCofork.ofπ s.π ⋯).pt)) s

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasCokernel f
Z : C
l : Z ⟶ Y
i : X ≅ Z
h : i.hom ≫ l = f
⊢ Eq (α := Z ⟶ cokernel f) (l ≫ π f) 0

Tactic:
simp [i.eq_inv_comp.2 h]

Premises used: Iff.mpr, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ f ≫ l = 0

Tactic:
simp [← h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
j : WalkingParallelPair
zero :
  s.ι.app WalkingParallelPair.zero ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) WalkingParallelPair.zero
one : s.ι.app WalkingParallelPair.one ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) WalkingParallelPair.one
⊢ s.ι.app j ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
zero : s.ι.app WalkingParallelPair.zero ≫ i.hom = f ≫ l
⊢ s.ι.app WalkingParallelPair.zero ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) WalkingParallelPair.zero

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
zero : s.ι.app WalkingParallelPair.zero ≫ i.hom = f ≫ Cofork.π s ≫ i.hom
⊢ s.ι.app WalkingParallelPair.zero ≫ i.hom = f ≫ l

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app zero ≫ i.hom = f ≫ Cofork.π s ≫ i.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app one ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) one

Tactic:
h

Premises used: CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app one ≫ i.hom = NatTrans.app (Cocone.ι (CokernelCofork.ofπ l ⋯)) one

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
s : CokernelCofork f
hs : IsColimit s
s' : CokernelCofork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : eY.hom ≫ Cofork.π s' = Cofork.π s ≫ e.hom
⊢ (parallelPair f 0).map WalkingParallelPairHom.right ≫ eY.hom =
    eX.hom ≫ (parallelPair f' 0).map WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
s : CokernelCofork f
hs : IsColimit s
s' : CokernelCofork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : eY.hom ≫ Cofork.π s' = Cofork.π s ≫ e.hom
α : parallelPair f 0 ≅ parallelPair f' 0 := parallelPairIsoMk eX eY ⋯ ⋯
⊢ ((Cocone.precompose α.symm.hom).obj s).ι.app zero ≫ e.hom = s'.ι.app zero

Tactic:
simp [α, ← H']
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
s : CokernelCofork f
hs : IsColimit s
s' : CokernelCofork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : eY.hom ≫ Cofork.π s' = Cofork.π s ≫ e.hom
α : parallelPair f 0 ≅ parallelPair f' 0 := parallelPairIsoMk eX eY ⋯ ⋯
⊢ ((Cocone.precompose α.symm.hom).obj s).ι.app one ≫ e.hom = s'.ι.app one

Tactic:
simp [α, ← H']
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : HasCokernel f
Z : C
l : Y ⟶ Z
i : cokernel f ≅ Z
h : π f ≫ i.hom = l
⊢ f ≫ l = 0

Tactic:
simp [← h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f) ≫ G.map f) 0

Tactic:
simp only [← G.map_comp, kernel.condition, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.kernel.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj X)
    (CategoryStruct.comp (Y := kernel (G.map f)) (kernelComparison f G) (kernel.ι (G.map f))) (G.map (kernel.ι f))

Tactic:
kernel.lift_ι _ _ _

Premises used: CategoryTheory.Limits.kernelComparison, CategoryTheory.Limits.kernel.lift_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map h ≫ G.map f = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
h₁ :
  CategoryStruct.comp (Y := equalizer (G.map f) 0)
      (CategoryStruct.comp (Y := G.obj (kernel f)) (G.map (kernel.lift f h w)) (kernelComparison f G))
      (equalizer.ι (G.map f) 0) =
    CategoryStruct.comp (Y := equalizer (G.map f) 0) (kernel.lift (G.map f) (G.map h) ⋯) (equalizer.ι (G.map f) 0)
⊢ Eq (α := G.obj Z ⟶ kernel (G.map f))
    (CategoryStruct.comp (Y := G.obj (kernel f)) (G.map (kernel.lift f h w)) (kernelComparison f G))
    (kernel.lift (G.map f) (G.map h) ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ CategoryStruct.comp (Y := equalizer (G.map f) 0)
      (CategoryStruct.comp (Y := G.obj (kernel f)) (G.map (kernel.lift f h w)) (kernelComparison f G))
      (equalizer.ι (G.map f) 0) =
    CategoryStruct.comp (Y := equalizer (G.map f) 0) (kernel.lift (G.map f) (G.map h) ⋯) (equalizer.ι (G.map f) 0)

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X' Y' : C
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : G.map (f ≫ q) = G.map p ≫ G.map g
rw₁ : G.map (p ≫ g) = G.map p ≫ G.map g
rw₂ rw₃ : G.map p ≫ G.map g = G.map p ≫ G.map g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
rw [← G.map_comp, hpq, G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X' Y' : C
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f ≫ f)) 0
rw₁ : Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map 0) 0
rw₂ rw₃ : Eq.{v₂ + 1} (α := G.obj (kernel f) ⟶ G.obj Y) 0 0
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj Y) (G.map (kernel.ι f) ≫ G.map f) 0

Tactic:
rw [← G.map_comp, kernel.condition, G.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.kernel.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X' Y' : C
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map (kernel.ι g ≫ g)) 0
rw₁ : Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map 0) 0
rw₂ rw₃ : Eq.{v₂ + 1} (α := G.obj (kernel g) ⟶ G.obj Y') 0 0
⊢ Eq (α := G.obj (kernel g) ⟶ G.obj Y') (G.map (kernel.ι g) ≫ G.map g) 0

Tactic:
rw [← G.map_comp, kernel.condition, G.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.kernel.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X' Y' : C
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
simp :
  Eq (α := G.obj (kernel f) ⟶ G.obj X') (G.map (kernel.ι f ≫ p))
    (G.map (CategoryStruct.comp (Y := kernel g) (kernel.map f g p q hpq) (kernel.ι g)))
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj X') (G.map (kernel.ι f) ≫ G.map p)
    (CategoryStruct.comp (Y := G.obj (kernel g)) (G.map (kernel.map f g p q hpq)) (G.map (kernel.ι g)))

Tactic:
simp only [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X' Y' : C
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj X') (G.map (kernel.ι f ≫ p))
    (G.map (CategoryStruct.comp (Y := kernel g) (kernel.map f g p q hpq) (kernel.ι g)))

Tactic:
G.congr_map (kernel.lift_ι _ _ _).symm

Premises used: CategoryTheory.Functor.congr_map, CategoryTheory.Limits.kernel.lift_ι, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X' Y' : C
inst_5 : HasKernel f
inst_6 : HasKernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasKernel g
inst_8 : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj (kernel f) ⟶ G.obj X') (G.map (kernel.ι f ≫ p))
    (G.map (CategoryStruct.comp (Y := kernel g) (kernel.map f g p q hpq) (kernel.ι g)))

Tactic:
exact G.congr_map (kernel.lift_ι _ _ _).symm

Premises used: CategoryTheory.Functor.congr_map, CategoryTheory.Limits.kernel.lift_ι, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
⊢ Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map f ≫ G.map (coequalizer.π f 0)) 0

Tactic:
simp only [← G.map_comp, cokernel.condition, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
⊢ Eq (α := G.obj Y ⟶ G.obj (cokernel f))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (cokernel.π (G.map f)) (cokernelComparison f G))
    (G.map (cokernel.π f))

Tactic:
cokernel.π_desc _ _ _

Premises used: CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Limits.cokernelComparison
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ G.map f ≫ G.map h = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
h₁ :
  CategoryStruct.comp (Y := coequalizer (G.map f) 0) (coequalizer.π (G.map f) 0)
      (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.desc f h w))) =
    CategoryStruct.comp (Y := coequalizer (G.map f) 0) (coequalizer.π (G.map f) 0) (cokernel.desc (G.map f) (G.map h) ⋯)
⊢ Eq (α := cokernel (G.map f) ⟶ G.obj Z)
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.desc f h w)))
    (cokernel.desc (G.map f) (G.map h) ⋯)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ CategoryStruct.comp (Y := coequalizer (G.map f) 0) (coequalizer.π (G.map f) 0)
      (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.desc f h w))) =
    CategoryStruct.comp (Y := coequalizer (G.map f) 0) (coequalizer.π (G.map f) 0) (cokernel.desc (G.map f) (G.map h) ⋯)

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X' Y' : C
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : G.map (f ≫ q) = G.map p ≫ G.map g
rw₁ : G.map (p ≫ g) = G.map p ≫ G.map g
rw₂ rw₃ : G.map p ≫ G.map g = G.map p ≫ G.map g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
rw [← G.map_comp, hpq, G.map_comp]

Premises used: CategoryTheory.Functor.map_comp