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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
rw : h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s
⊢ f ≫ Cofork.π s = 0 ≫ Cofork.π s

Tactic:
rw [← cancel_epi g, ← Category.assoc, ← hh]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π 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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ (isCokernelEpiComp i g hh).desc s = i.desc (Cofork.ofπ (Cofork.π s) ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Limits.parallelPair, rfl, 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
W : C
g : W ⟶ X
h : W ⟶ Y
c : CokernelCofork h
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h
s : Cofork f 0
⊢ h ≫ s.π = 0

Tactic:
simp [← hfg]
-- 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
W : C
g : W ⟶ X
h : W ⟶ Y
c : CokernelCofork h
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h
s : Cofork f 0
⊢ Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫
      (fun (s : Cofork f 0) ↦ (i.desc (CokernelCofork.ofπ s.π ⋯) : c.pt ⟶ (CokernelCofork.ofπ s.π ⋯).pt)) s =
    s.π

Tactic:
simp only [CokernelCofork.π_ofπ, Cofork.IsColimit.π_desc]

Premises used: CategoryTheory.Limits.Cofork.IsColimit.π_desc, CategoryTheory.Limits.CokernelCofork.π_ofπ
-- 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
W : C
g : W ⟶ X
h_1 : W ⟶ Y
c : CokernelCofork h_1
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h_1
s : Cofork f 0
m : (CokernelCofork.ofπ (Cofork.π c) hf).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ m = s.π
apply :
  Cofork.π c ≫ m =
    Cofork.π c ≫ (fun (s : Cofork f 0) ↦ (i.desc (CokernelCofork.ofπ s.π ⋯) : c.pt ⟶ (CokernelCofork.ofπ s.π ⋯).pt)) s
⊢ m = (fun (s : Cofork f 0) ↦ (i.desc (CokernelCofork.ofπ s.π ⋯) : c.pt ⟶ (CokernelCofork.ofπ s.π ⋯).pt)) s

Tactic:
apply Cofork.IsColimit.hom_ext i

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
W : C
g : W ⟶ X
h_1 : W ⟶ Y
c : CokernelCofork h_1
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h_1
s : Cofork f 0
m : (CokernelCofork.ofπ (Cofork.π c) hf).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ m = s.π
⊢ Cofork.π c ≫ m =
    Cofork.π c ≫ (fun (s : Cofork f 0) ↦ (i.desc (CokernelCofork.ofπ s.π ⋯) : c.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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
hf : f = 0
rw : Eq.{v + 1} (α := X ⟶ Y) (0 ≫ 𝟙 Y) 0
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ Y) 0 0
⊢ f ≫ 𝟙 Y = 0

Tactic:
rw [hf, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- 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
X Y : C
f : X ⟶ Y
hf : f = 0
Z' : C
x : Y ⟶ Z'
h : f ≫ x = 0
x_1 : Y ⟶ Z'
hb : 𝟙 Y ≫ x_1 = x
⊢ x_1 = (fun {Z' : C} (x : Y ⟶ Z') (x_2 : f ≫ x = 0) ↦ x) x h

Tactic:
simp only [← hb, Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- 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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hf : Epi f
h : IsZero.{v, u} c.pt
s : CokernelCofork f
rw : 0 = Cofork.π s
rw₁ : f ≫ 0 = f ≫ Cofork.π s
rw₂ : 0 = f ≫ Cofork.π s
rw₃ rw₄ : Eq.{v + 1} (α := X ⟶ s.pt) 0 0
⊢ Cofork.π c ≫ (fun (x : CokernelCofork f) ↦ (0 : c.pt ⟶ x.pt)) s = Cofork.π s

Tactic:
rw [comp_zero, ← cancel_epi f, comp_zero, s.condition]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.cancel_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
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
⊢ IsIso (Cofork.π c)

Tactic:
isIso_colimit_cocone_parallelPair_of_eq hf hc

Premises used: CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
⊢ f' ≫ e.hom ≫ Cofork.π c = 0

Tactic:
simp [← iff]
-- 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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
Z' : C
s : Y' ⟶ Z'
hs : f' ≫ s = 0
rw : f' ≫ e.hom ≫ e.inv ≫ s = 0
rw₁ : f' ≫ s = 0
rw₂ rw₃ : Eq.{v + 1} (α := X' ⟶ Z') 0 0
⊢ f ≫ e.inv ≫ s = 0

Tactic:
rw [iff, e.hom_inv_id_assoc, hs]

Premises used: CategoryTheory.Iso.hom_inv_id_assoc
-- 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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
Z' : C
s : Y' ⟶ Z'
hs : f' ≫ s = 0
⊢ (e.hom ≫ Cofork.π c) ≫
      (fun {Z' : C} (s : Y' ⟶ Z') (hs : f' ≫ s = 0) ↦ (hc.desc (ofπ (e.inv ≫ s) ⋯) : c.pt ⟶ (ofπ (e.inv ≫ s) ⋯).pt)) s
        hs =
    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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
Z' : C
s : Y' ⟶ Z'
hs : f' ≫ s = 0
m : c.pt ⟶ Z'
hm : (e.hom ≫ Cofork.π c) ≫ m = s
⊢ Cofork.π c ≫ m =
    Cofork.π c ≫
      (fun {Z' : C} (s : Y' ⟶ Z') (hs : f' ≫ s = 0) ↦ (hc.desc (ofπ (e.inv ≫ s) ⋯) : c.pt ⟶ (ofπ (e.inv ≫ s) ⋯).pt)) s
        hs

Tactic:
simpa [← cancel_epi e.hom] using hm

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- 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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' : C
f' : X' ⟶ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ φ = 0
⊢ f' ≫ Cofork.π c = 0

Tactic:
simp [← iff]
-- 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
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' : C
f' : X' ⟶ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ φ = 0
⊢ ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ Iso.hom (Iso.refl Y) ≫ φ = 0

Tactic:
simpa using iff
-- 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
c : CokernelCofork f
hc : IsColimit c
inst_2 : Epi f
⊢ Epi (Cofork.π c)

Tactic:
have := Cofork.IsColimit.epi hc
-- 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
c : CokernelCofork f
hc : IsColimit c
inst_2 : Epi f
this : Epi (Cofork.π c)
rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
rw₁ : Cofork.π c ≫ 𝟙 c.pt = Cofork.π c ≫ 0
rw₂ : f ≫ Cofork.π c ≫ 𝟙 c.pt = f ≫ Cofork.π c ≫ 0
rw₃ : 0 ≫ 𝟙 c.pt = f ≫ Cofork.π c ≫ 0
rw₄ : 0 ≫ 𝟙 c.pt = f ≫ 0
rw₅ : Eq.{v + 1} (α := X ⟶ c.pt) (0 ≫ 𝟙 c.pt) 0
rw₆ rw₇ : Eq.{v + 1} (α := X ⟶ c.pt) 0 0
⊢ IsZero.{v, u} c.pt

Tactic:
rw [IsZero.iff_id_eq_zero, ← cancel_epi c.π, ← cancel_epi f,
    c.condition_assoc, comp_zero, comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.CokernelCofork.condition_assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.cancel_epi, 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
X' Y' : C
f' : X' ⟶ Y'
cc : CokernelCofork f
hf : IsColimit cc
cc' : CokernelCofork f'
φ : Arrow.mk f ⟶ Arrow.mk f'
erw : Arrow.Hom.left φ ≫ (Arrow.mk f').hom ≫ Cofork.π cc' = 0
erw₁ : Eq (α := X ⟶ cc'.pt) (Arrow.Hom.left φ ≫ 0) 0
erw₂ erw₃ : Eq.{v + 1} (α := X ⟶ cc'.pt) 0 0
⊢ f ≫ Arrow.Hom.right φ ≫ Cofork.π cc' = 0

Tactic:
erw [← Arrow.w_assoc φ, condition, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.Arrow.w_assoc
-- 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'
cc : CokernelCofork f
hf : IsColimit cc
cc' : CokernelCofork f'
φ : Arrow.mk f ⟶ Arrow.mk f'
⊢ Cofork.π cc ≫ mapOfIsColimit hf cc' φ = Arrow.Hom.right φ ≫ Cofork.π cc'

Tactic:
hf.fac _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.CokernelCofork.mapOfIsColimit, CategoryTheory.Limits.parallelPair, 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
X' Y' : C
f' : X' ⟶ Y'
cc : CokernelCofork f
cc' : CokernelCofork f'
hf : IsColimit cc
hf' : IsColimit cc'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ Cofork.π cc ≫ mapOfIsColimit hf cc' φ.hom ≫ mapOfIsColimit hf' cc φ.inv = Cofork.π cc ≫ 𝟙 cc.pt

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'
cc : CokernelCofork f
cc' : CokernelCofork f'
hf : IsColimit cc
hf' : IsColimit cc'
φ : Arrow.mk f ≅ Arrow.mk f'
⊢ Cofork.π cc' ≫ mapOfIsColimit hf' cc φ.inv ≫ mapOfIsColimit hf cc' φ.hom = Cofork.π cc' ≫ 𝟙 cc'.pt

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
inst_2 : HasCokernel f
⊢ Eq (α := Y ⟶ coequalizer f 0) (coequalizer.π f 0) (cokernel.π f)

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq (α := X ⟶ cokernel f) (f ≫ π f) 0

Tactic:
CokernelCofork.condition _

Premises used: CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- 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
W : C
k : Y ⟶ W
h : f ≫ k = 0
⊢ CategoryStruct.comp (Y := cokernel f) (π f) (desc f k h) = k

Tactic:
(cokernelIsCokernel f).fac (CokernelCofork.ofπ k h) WalkingParallelPair.one

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.colimit, CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.Limits.CokernelCofork.ofπ, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0
inst_2 : HasCokernel f
rw :
  CategoryStruct.comp (Y := colimit (parallelPair f 0))
      ((parallelPair f 0).map WalkingParallelPairHom.left ≫ colimit.ι (parallelPair f 0) one) (cokernel.desc f g h) =
    0
⊢ CategoryStruct.comp (Y := colimit (parallelPair f 0)) (colimit.ι (parallelPair f 0) zero) (cokernel.desc f g h) = 0

Tactic:
rw [(colimit.w (parallelPair f 0) WalkingParallelPairHom.left).symm]

Premises used: CategoryTheory.Limits.colimit.w, OfNat.ofNat, Eq.symm, CategoryTheory.Limits.WalkingParallelPairHom.left, CategoryTheory.Limits.parallelPair
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : f ≫ g = 0
inst_2 : HasCokernel f
⊢ CategoryStruct.comp (Y := colimit (parallelPair f 0))
      ((parallelPair f 0).map WalkingParallelPairHom.left ≫ colimit.ι (parallelPair f 0) one) (cokernel.desc f g h) =
    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 Y : C
f : X ⟶ Y
inst_2 : HasCokernel f
W : C
h : Eq (α := X ⟶ W) (f ≫ 0) 0
h₁ :
  CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0) (desc f 0 h) =
    CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0) 0
⊢ Eq (α := cokernel f ⟶ W) (desc f 0 h) 0

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
inst_2 : HasCokernel f
W : C
h : Eq (α := X ⟶ W) (f ≫ 0) 0
⊢ CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0) (desc f 0 h) =
    CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π 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 Y : C
f : X ⟶ Y
inst_2 : HasCokernel f
W : C
k : Y ⟶ W
h : f ≫ k = 0
inst_3 : Epi k
Z : C
g g' : W ⟶ Z
w : Eq (α := cokernel f ⟶ Z) (desc f k h ≫ g) (desc f k h ≫ g')
⊢ CategoryStruct.comp (Y := cokernel f) (π f) (desc f k h ≫ g) =
    CategoryStruct.comp (Y := cokernel f) (π f) (desc f k h ≫ g')

Tactic:
replace w := cokernel.π f ≫= w
-- 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
W : C
k : Y ⟶ W
h : f ≫ k = 0
inst_3 : Epi k
Z : C
g g' : W ⟶ Z
w :
  CategoryStruct.comp (Y := cokernel f) (π f) (desc f k h ≫ g) =
    CategoryStruct.comp (Y := cokernel f) (π f) (desc f k h ≫ g')
⊢ k ≫ g = k ≫ g'

Tactic:
simp only [cokernel.π_desc_assoc] at w

Premises used: CategoryTheory.Limits.cokernel.π_desc_assoc
-- 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
W : C
k : Y ⟶ W
h : f ≫ k = 0
inst_3 : Epi k
Z : C
g g' : W ⟶ Z
w : k ≫ g = k ≫ g'
⊢ g = g'

Tactic:
(cancel_epi k).1 w

Premises used: Iff.mp, CategoryTheory.cancel_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 : HasCokernel f
W : C
k : Y ⟶ W
h : f ≫ k = 0
inst_3 : Epi k
Z : C
g g' : W ⟶ Z
w : k ≫ g = k ≫ g'
⊢ g = g'

Tactic:
exact (cancel_epi k).1 w

Premises used: Iff.mp, CategoryTheory.cancel_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 : HasCokernel f
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
simp : Eq (α := X ⟶ cokernel f') ((f ≫ q) ≫ π f') ((p ≫ f') ≫ π f')
⊢ Eq (α := X ⟶ cokernel f') (f ≫ q ≫ π f') (p ≫ f' ≫ π f')

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
⊢ Eq (α := X ⟶ cokernel f') ((f ≫ q) ≫ π f') ((p ≫ f') ≫ π f')

Tactic:
apply congrArg (· ≫ π f') w

Premises used: congrArg, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.cokernel.π
-- 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
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
⊢ Eq (α := X ⟶ cokernel f') (f ≫ q ≫ π f') (p ≫ f' ≫ π f')

Tactic:
have : f ≫ q ≫ π f' = p ≫ f' ≫ π f' := by
      simp only [← Category.assoc]
      apply congrArg (· ≫ π f') w
-- 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
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
this : Eq (α := X ⟶ cokernel f') (f ≫ q ≫ π f') (p ≫ f' ≫ π f')
⊢ Eq (α := X ⟶ cokernel f') (f ≫ q ≫ π f') 0

Tactic:
simp [this]
-- 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
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst_4 : Epi p
inst_5 : IsIso q
⊢ Eq (α := X' ⟶ cokernel f) (f' ≫ inv q ≫ cokernel.π f) 0

Tactic:
simp [← cancel_epi p, ← reassoc_of% w]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z X' Y' Z' : C
f : X ⟶ Y
inst_2 : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
h :
  CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0)
      (CategoryStruct.comp (Y := cokernel f') (map f f' p q h₁) (desc f' g' w')) =
    CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0) (desc f g w ≫ r)
⊢ Eq (α := cokernel f ⟶ Z') (CategoryStruct.comp (Y := cokernel f') (map f f' p q h₁) (desc f' g' w')) (desc f g w ≫ r)

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 Z X' Y' Z' : C
f : X ⟶ Y
inst_2 : HasCokernel f
g : Y ⟶ Z
w : f ≫ g = 0
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
g' : Y' ⟶ Z'
w' : f' ≫ g' = 0
p : X ⟶ X'
q : Y ⟶ Y'
r : Z ⟶ Z'
h₁ : f ≫ q = p ≫ f'
h₂ : g ≫ r = q ≫ g'
⊢ CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0)
      (CategoryStruct.comp (Y := cokernel f') (map f f' p q h₁) (desc f' g' w')) =
    CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0) (desc f g w ≫ r)

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
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
p : X ≅ X'
q : Y ≅ Y'
w : f ≫ q.hom = p.hom ≫ f'
⊢ f' ≫ q.inv = p.inv ≫ f

Tactic:
(cancel_mono q.hom).1 ?_

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Iso.hom
-- 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
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
p : X ≅ X'
q : Y ≅ Y'
w : f ≫ q.hom = p.hom ≫ f'
refine : (f' ≫ q.inv) ≫ q.hom = (p.inv ≫ f) ≫ q.hom
⊢ f' ≫ q.inv = p.inv ≫ f

Tactic:
refine (cancel_mono q.hom).1 ?_

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Iso.hom
-- 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
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasCokernel f'
p : X ≅ X'
q : Y ≅ Y'
w : f ≫ q.hom = p.hom ≫ f'
⊢ (f' ≫ q.inv) ≫ q.hom = (p.inv ≫ f) ≫ q.hom

Tactic:
simp [w]
-- 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
⊢ 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 : HasCokernel f
inst_3 : Mono (Y := cokernel f) (cokernel.π f)
⊢ Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) (0 ≫ cokernel.π f)

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
inst_2 : HasCokernel f
⊢ Eq.{v + 1} (α := X ⟶ Y) (0 ≫ 𝟙 Y) 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 Y : C
h :
  Eq.{v + 1} (α := Y ⟶ Y)
    (CategoryStruct.comp (Y := coequalizer.{v, u} (X := X) (Y := Y) 0 0) (coequalizer.π 0 0)
      (Iso.hom cokernelZeroIsoTarget))
    (CategoryStruct.comp (Y := coequalizer.{v, u} (X := X) (Y := Y) 0 0) (coequalizer.π 0 0) (cokernel.desc 0 (𝟙 Y) ⋯))
⊢ Eq.{v + 1} (α := cokernel.{v, u} (X := X) (Y := Y) 0 ⟶ Y) (Iso.hom cokernelZeroIsoTarget) (cokernel.desc 0 (𝟙 Y) ⋯)

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
⊢ Eq.{v + 1} (α := Y ⟶ Y)
    (CategoryStruct.comp (Y := coequalizer.{v, u} (X := X) (Y := Y) 0 0) (coequalizer.π 0 0)
      (Iso.hom cokernelZeroIsoTarget))
    (CategoryStruct.comp (Y := coequalizer.{v, u} (X := X) (Y := Y) 0 0) (coequalizer.π 0 0) (cokernel.desc 0 (𝟙 Y) ⋯))

Tactic:
simp [cokernelZeroIsoTarget]

Premises used: CategoryTheory.Limits.cokernelZeroIsoTarget
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := Y ⟶ cokernel.{v, u} (X := X) (Y := Y) 0) (Iso.inv cokernelZeroIsoTarget) (cokernel.π 0)

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- 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_1 : X ⟶ Y
inst_2 : HasCokernel f_1
f g : X ⟶ Y
inst_3 : HasCokernel f
inst_4 : HasCokernel g
h : f = g
simp : parallelPair g 0 ≅ parallelPair g 0
⊢ parallelPair f 0 ≅ parallelPair g 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_1 : X ⟶ Y
inst_2 : HasCokernel f_1
f g : X ⟶ Y
inst_3 : HasCokernel f
inst_4 : HasCokernel g
h : f = g
⊢ parallelPair g 0 ≅ parallelPair g 0

Tactic:
rfl
-- 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
h : f = f
w :
  CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0) (Iso.hom (cokernelIsoOfEq h)) =
    coequalizer.π f 0 ≫ Iso.hom (Iso.refl (cokernel f))
⊢ cokernelIsoOfEq h = Iso.refl (cokernel f)

Tactic:
ext