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

Tactic:
simp [cokernelIsoOfEq]

Premises used: CategoryTheory.Limits.cokernelIsoOfEq
-- 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 g : X ⟶ Y
inst_2 : HasCokernel f
inst_3 : HasCokernel g
h : f = g
refl :
  ∀ [inst_4 : HasCokernel f],
    Eq (α := Y ⟶ cokernel f) (CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (Iso.hom (cokernelIsoOfEq ⋯)))
      (cokernel.π f)
⊢ Eq (α := Y ⟶ cokernel g) (CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (Iso.hom (cokernelIsoOfEq h)))
    (cokernel.π g)

Tactic:
cases 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 inst_3 : HasCokernel f
⊢ Eq (α := Y ⟶ cokernel f) (CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (Iso.hom (cokernelIsoOfEq ⋯)))
    (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 g : X ⟶ Y
inst_2 : HasCokernel f
inst_3 : HasCokernel g
h : f = g
refl :
  ∀ [inst_4 : HasCokernel f],
    Eq (α := Y ⟶ cokernel f) (CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (Iso.inv (cokernelIsoOfEq ⋯)))
      (cokernel.π f)
⊢ Eq (α := Y ⟶ cokernel f) (CategoryStruct.comp (Y := cokernel g) (cokernel.π g) (Iso.inv (cokernelIsoOfEq h)))
    (cokernel.π f)

Tactic:
cases 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 inst_3 : HasCokernel f
⊢ Eq (α := Y ⟶ cokernel f) (CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (Iso.inv (cokernelIsoOfEq ⋯)))
    (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_1 : X ⟶ Y
inst_2 : HasCokernel f_1
Z : C
f g : X ⟶ Y
inst_3 : HasCokernel f
inst_4 : HasCokernel g
h : f = g
e : Y ⟶ Z
he : g ≫ e = 0
⊢ f ≫ e = 0

Tactic:
simp [h, he]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : HasCokernel f
inst_3 : HasCokernel g
h : f = g
e : Y ⟶ Z
he : g ≫ e = 0
refl :
  ∀ [inst_4 : HasCokernel f] (he : f ≫ e = 0),
    Eq (α := cokernel f ⟶ Z)
      (CategoryStruct.comp (Y := cokernel f) (Iso.hom (cokernelIsoOfEq ⋯)) (cokernel.desc f e he)) (cokernel.desc f e ⋯)
⊢ Eq (α := cokernel f ⟶ Z) (CategoryStruct.comp (Y := cokernel g) (Iso.hom (cokernelIsoOfEq h)) (cokernel.desc g e he))
    (cokernel.desc f e ⋯)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_2 : HasCokernel f
e : Y ⟶ Z
inst_3 : HasCokernel f
he : f ≫ e = 0
⊢ Eq (α := cokernel f ⟶ Z) (CategoryStruct.comp (Y := cokernel f) (Iso.hom (cokernelIsoOfEq ⋯)) (cokernel.desc f e he))
    (cokernel.desc f e ⋯)

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_1 : X ⟶ Y
inst_2 : HasCokernel f_1
Z : C
f g : X ⟶ Y
inst_3 : HasCokernel f
inst_4 : HasCokernel g
h : f = g
e : Y ⟶ Z
he : f ≫ e = 0
⊢ g ≫ e = 0

Tactic:
simp [← h, he]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst_2 : HasCokernel f
inst_3 : HasCokernel g
h : f = g
e : Y ⟶ Z
he : f ≫ e = 0
refl :
  ∀ [inst_4 : HasCokernel f],
    Eq (α := cokernel f ⟶ Z)
      (CategoryStruct.comp (Y := cokernel f) (Iso.inv (cokernelIsoOfEq ⋯)) (cokernel.desc f e he)) (cokernel.desc f e ⋯)
⊢ Eq (α := cokernel g ⟶ Z) (CategoryStruct.comp (Y := cokernel f) (Iso.inv (cokernelIsoOfEq h)) (cokernel.desc f e he))
    (cokernel.desc g e ⋯)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_2 : HasCokernel f
e : Y ⟶ Z
he : f ≫ e = 0
inst_3 : HasCokernel f
⊢ Eq (α := cokernel f ⟶ Z) (CategoryStruct.comp (Y := cokernel f) (Iso.inv (cokernelIsoOfEq ⋯)) (cokernel.desc f e he))
    (cokernel.desc f e ⋯)

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 g h : X ⟶ Y
inst_2 : HasCokernel f
inst_3 : HasCokernel g
inst_4 : HasCokernel h
w₁ : f = g
w₂ : g = h
refl :
  ∀ [inst_5 : HasCokernel f] (w₂ : f = h),
    Eq (α := cokernel f ≅ cokernel h) (Iso.trans (Y := cokernel f) (cokernelIsoOfEq ⋯) (cokernelIsoOfEq w₂))
      (cokernelIsoOfEq ⋯)
⊢ Eq (α := cokernel f ≅ cokernel h) (Iso.trans (Y := cokernel g) (cokernelIsoOfEq w₁) (cokernelIsoOfEq w₂))
    (cokernelIsoOfEq ⋯)

Tactic:
cases 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 h : X ⟶ Y
inst_2 : HasCokernel f
inst_3 : HasCokernel h
inst_4 : HasCokernel f
w₂ : f = h
⊢ Eq (α := cokernel f ≅ cokernel h) (Iso.trans (Y := cokernel f) (cokernelIsoOfEq ⋯) (cokernelIsoOfEq w₂))
    (cokernelIsoOfEq ⋯)

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 : f ≠ 0
⊢ ¬Mono (Y := cokernel f) (cokernel.π f)

Tactic:
fun _ =>
  w (eq_zero_of_mono_cokernel f)

Premises used: CategoryTheory.Limits.eq_zero_of_mono_cokernel, Not
-- 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 : f ≠ 0
⊢ IsIso (Y := cokernel f) (cokernel.π f) → False

Tactic:
fun _ =>
  cokernel_not_mono_of_nonzero w inferInstance

Premises used: CategoryTheory.Limits.cokernel_not_mono_of_nonzero, inferInstance
-- 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 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : HasCokernel f
inst_4 : IsIso g
⊢ Eq (α := X ⟶ cokernel f) ((f ≫ g) ≫ inv g ≫ cokernel.π f) 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 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : HasCokernel f
inst_4 : IsIso g
s : CokernelCofork (f ≫ g)
rw : (f ≫ g) ≫ Cofork.π s = 0
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ s.pt) 0 0
⊢ f ≫ g ≫ Cofork.π s = 0

Tactic:
rw [← Category.assoc, CokernelCofork.condition]

Premises used: CategoryTheory.Category.assoc, 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 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : HasCokernel f
inst_4 : IsIso g
⊢ ∀ (s : CokernelCofork (f ≫ g)),
    CategoryStruct.comp (Y :=
        Cocone.pt (F := parallelPair (f ≫ g) 0) (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯))
        (Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯))
        ((fun (s : CokernelCofork (f ≫ g)) ↦ (cokernel.desc f (g ≫ Cofork.π s) ⋯ : cokernel f ⟶ s.pt)) s) =
      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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : HasCokernel f
inst_4 : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel f ⟶ s.pt
w : Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
simp_rw : m = cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯
⊢ m = (fun (s : CokernelCofork (f ≫ g)) ↦ (cokernel.desc f (g ≫ Cofork.π s) ⋯ : cokernel f ⟶ s.pt)) s

Tactic:
simp_rw [← w]
-- 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 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : HasCokernel f
inst_4 : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel f ⟶ s.pt
w : Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
h :
  coequalizer.π f 0 ≫ m =
    CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0)
      (cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯)
⊢ m = cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯

Tactic:
apply coequalizer.hom_ext

Premises used: CategoryTheory.Limits.coequalizer.hom_ext
-- 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 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : HasCokernel f
inst_4 : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel f ⟶ s.pt
w : Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ coequalizer.π f 0 ≫ m =
    CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0)
      (cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯)

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 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : HasCokernel f
inst_4 : IsIso g
rw : Eq (α := X ⟶ cokernel (f ≫ g)) ((f ≫ g) ≫ cokernel.π (f ≫ g)) 0
rw₁ rw₂ : Eq.{v + 1} (α := X ⟶ cokernel (f ≫ g)) 0 0
⊢ Eq (α := X ⟶ cokernel (f ≫ g)) (f ≫ g ≫ cokernel.π (f ≫ g)) 0

Tactic:
rw [← Category.assoc, cokernel.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.cokernel.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 : HasCokernel f_1
X Y : C
f : X ⟶ Y
inst_3 : HasCokernel f
W : C
g : W ⟶ X
inst_4 : Epi g
⊢ HasCokernel (g ≫ f)

Tactic:
⟨⟨{   cocone := _
        isColimit := isCokernelEpiComp (colimit.isColimit _) g rfl }⟩⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.isCokernelEpiComp._proof_1, CategoryTheory.Limits.isCokernelEpiComp, CategoryTheory.Limits.colimit.cocone, OfNat.ofNat, CategoryTheory.Limits.parallelPair, rfl, CategoryTheory.Limits.CokernelCofork.ofπ, 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : Epi f
inst_4 : HasCokernel g
⊢ Eq (α := X ⟶ cokernel g) ((f ≫ g) ≫ cokernel.π g) 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 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : Epi f
inst_4 : HasCokernel g
rw : Eq (α := X ⟶ cokernel (f ≫ g)) ((f ≫ g) ≫ cokernel.π (f ≫ g)) (f ≫ 0)
⊢ Eq (α := Y ⟶ cokernel (f ≫ g)) (g ≫ cokernel.π (f ≫ g)) 0

Tactic:
rw [← cancel_epi f, ← Category.assoc]

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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasCokernel f_1
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_3 : Epi f
inst_4 : HasCokernel g
⊢ Eq (α := X ⟶ cokernel (f ≫ g)) ((f ≫ g) ≫ cokernel.π (f ≫ g)) (f ≫ 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 : HasCokernel f_1
X Y : C
f g : X ⟶ Y
inst_3 : HasCokernel f
inst_4 : HasCokernel g
h : f = g
⊢ Eq (α := X ⟶ cokernel g) (f ≫ π 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_1 Y_1 : C
f_1 : X_1 ⟶ Y_1
inst_2 : HasCokernel f_1
X Y : C
f g : X ⟶ Y
inst_3 : HasCokernel f
inst_4 : HasCokernel g
h : f = g
⊢ Eq (α := X ⟶ cokernel f) (g ≫ π f) 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
inst_2 : Epi f
inst_3 : HasCokernel f
⊢ IsZero.{v, u} (cokernel f)

Tactic:
CokernelCofork.IsColimit.isZero_of_epi (c := CokernelCofork.ofπ _ (cokernel.condition f))
    (cokernelIsCokernel f)

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.cokernelIsCokernel, CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_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
⊢ Eq (α := Y ⟶ Cocone.pt (F := parallelPair f 0) (zeroCokernelCofork f)) (Cofork.π (zeroCokernelCofork f)) 0

Tactic:
rfl

Premises used: 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
inst_2 : HasZeroObject.{v, u} C
inst_3 : Epi f
x : Cofork f 0
⊢ CategoryStruct.comp (Y := Cocone.pt (F := parallelPair f 0) (zeroCokernelCofork f)) (Cofork.π (zeroCokernelCofork f))
      ((fun (x : Cofork f 0) ↦ (0 : Cocone.pt (F := parallelPair f 0) (zeroCokernelCofork f) ⟶ x.pt)) x) =
    x.π

Tactic:
simp [zero_of_epi_comp f _]

Premises used: CategoryTheory.Limits.zero_of_epi_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
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasCokernel f
inst_4 : Epi f
⊢ Eq (α := Y ⟶ cokernel f) (π f) 0

Tactic:
zero_of_target_iso_zero _ (cokernel.ofEpi f)

Premises used: CategoryTheory.Limits.cokernel.ofEpi, CategoryTheory.Limits.zero_of_target_iso_zero
-- 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
F : MonoFactorisation f
rw : Eq (α := kernel f ⟶ Y) ((kernel.ι f ≫ F.e) ≫ F.m) (0 ≫ F.m)
rw₁ : Eq (α := kernel f ⟶ Y) ((kernel.ι f ≫ F.e) ≫ F.m) 0
rw₂ : Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ F.e ≫ F.m) 0
rw₃ : Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ f) 0
rw₄ rw₅ : Eq.{v + 1} (α := kernel f ⟶ Y) 0 0
⊢ Eq (α := kernel f ⟶ F.I) (kernel.ι f ≫ F.e) 0

Tactic:
rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Limits.kernel.condition, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.MonoFactorisation.m
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
⊢ Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0

Tactic:
have w := cokernel.condition f
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
w : Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0
lhs : f ≫ cokernel.π f
| Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0

Tactic:
lhs
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
w : Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0
a : f
a₁ : cokernel.π f
| f ≫ cokernel.π f

Tactic:
congr
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
w : Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0
a : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)
| f

Tactic:
rw [← image.fac f]

Premises used: CategoryTheory.Limits.image.fac
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
w : Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0
a : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)
a₁ : cokernel.π f
| Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0

Tactic:
lhs
          congr
          rw [← image.fac f]

Premises used: CategoryTheory.Limits.image.fac
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
w : Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0
⊢ Eq (α := X ⟶ cokernel f) (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) ≫ cokernel.π f) 0

Tactic:
conv at w =>
          lhs
          congr
          rw [← image.fac f]

Premises used: CategoryTheory.Limits.image.fac
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
w : Eq (α := X ⟶ cokernel f) (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) ≫ cokernel.π f) 0
⊢ Eq (α := image f ⟶ cokernel f) (image.ι f ≫ cokernel.π f) 0

Tactic:
rw [← HasZeroMorphisms.comp_zero (Limits.factorThruImage f), Category.assoc,
          cancel_epi] at w

Premises used: CategoryTheory.Limits.factorThruImage, CategoryTheory.Category.assoc, CategoryTheory.cancel_epi, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
w : Eq (α := image f ⟶ cokernel f) (image.ι f ≫ cokernel.π f) 0
⊢ Eq (α := image f ⟶ cokernel f) (image.ι f ≫ cokernel.π f) 0

Tactic:
w
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
w : Eq (α := image f ⟶ cokernel f) (image.ι f ≫ cokernel.π f) 0
⊢ Eq (α := image f ⟶ cokernel f) (image.ι f ≫ cokernel.π f) 0

Tactic:
exact w
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
lhs : f ≫ cokernel.π (image.ι f)
| Eq (α := X ⟶ cokernel (X := image f) (image.ι f)) (f ≫ cokernel.π (image.ι f)) 0

Tactic:
lhs
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
a : f
a₁ : cokernel.π (image.ι f)
| f ≫ cokernel.π (image.ι f)

Tactic:
congr
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
a : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)
| f

Tactic:
rw [← image.fac f]

Premises used: CategoryTheory.Limits.image.fac
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
a : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)
a₁ : cokernel.π (image.ι f)
| Eq (α := X ⟶ cokernel (X := image f) (image.ι f)) (f ≫ cokernel.π (image.ι f)) 0

Tactic:
lhs
          congr
          rw [← image.fac f]

Premises used: CategoryTheory.Limits.image.fac
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
conv :
  Eq (α := X ⟶ cokernel (X := image f) (image.ι f))
    (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) ≫ cokernel.π (image.ι f)) 0
⊢ Eq (α := X ⟶ cokernel (X := image f) (image.ι f)) (f ≫ cokernel.π (image.ι f)) 0

Tactic:
conv =>
          lhs
          congr
          rw [← image.fac f]

Premises used: CategoryTheory.Limits.image.fac
-- 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
inst_2 : HasImage f
inst_3 : HasCokernel (X := image f) (image.ι f)
inst_4 : HasCokernel f
inst_5 : Epi (Y := image f) (factorThruImage f)
rw :
  Eq (α := X ⟶ cokernel (X := image f) (image.ι f))
    (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f ≫ cokernel.π (image.ι f))) 0
rw₁ : Eq (α := X ⟶ cokernel (X := image f) (image.ι f)) (CategoryStruct.comp (Y := image f) (factorThruImage f) 0) 0
rw₂ rw₃ : Eq.{v + 1} (α := X ⟶ cokernel (X := image f) (image.ι f)) 0 0
⊢ Eq (α := X ⟶ cokernel (X := image f) (image.ι f))
    (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) ≫ cokernel.π (image.ι f)) 0

Tactic:
rw [Category.assoc, cokernel.condition, HasZeroMorphisms.comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- 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 f : X ⟶ Y
inst_2 : HasKernel f
inst_3 : HasImage f
inst_4 : HasKernel (Y := image f) (factorThruImage f)
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) = f

Tactic:
simp