awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ f ≫ Arrow.Hom.right φ ≫ Cofork.π cc' = 0
have erw₂ : Eq.{v + 1} (α := X ⟶ cc'.pt) 0 0
Tactic: erw [← Arrow.w_assoc φ, condition, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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)) (colimit.ι (parallelPair f 0) zero) (cokernel.desc f g h) = 0
have 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
Tactic: rw [(colimit.w (parallelPair f 0) WalkingParallelPairHom.left).symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := cokernel f ⟶ W) (desc f 0 h) 0
have h₁ : CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0) (desc f 0 h) =
  CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0) 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (hypothesis)
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')
⊢ g = g'
have w₁ : 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
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (hypothesis)
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')
⊢ g = g'
have w₁ : k ≫ g = k ≫ g'
Tactic: simp only [cokernel.π_desc_assoc] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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')
have simp : Eq (α := X ⟶ cokernel f') ((f ≫ q) ≫ π f') ((p ≫ f') ≫ π f')
Tactic: simp only [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (hypothesis)
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') 0
have this : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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'
⊢ Eq (α := cokernel f ⟶ Z') (CategoryStruct.comp (Y := cokernel f') (map f f' p q h₁) (desc f' g' w')) (desc f g w ≫ r)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
have refine : (f' ≫ q.inv) ≫ q.hom = (p.inv ≫ f) ≫ q.hom
Tactic: refine (cancel_mono q.hom).1 ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := cokernel.{v, u} (X := X) (Y := Y) 0 ⟶ Y) (Iso.hom cokernelZeroIsoTarget) (cokernel.desc 0 (𝟙 Y) ⋯)
have 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) sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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 f 0 ≅ parallelPair g 0
have simp : parallelPair g 0 ≅ parallelPair g 0
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ cokernelIsoOfEq h = Iso.refl (cokernel f)
have w : CategoryStruct.comp (Y := coequalizer f 0) (coequalizer.π f 0) (Iso.hom (cokernelIsoOfEq h)) =
  coequalizer.π f 0 ≫ Iso.hom (Iso.refl (cokernel f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := Y ⟶ cokernel g) (CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (Iso.hom (cokernelIsoOfEq h)))
    (cokernel.π g)
have refl : ∀ [inst_4 : HasCokernel f],
  Eq (α := Y ⟶ cokernel f) (CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (Iso.hom (cokernelIsoOfEq sorry)))
    (cokernel.π f)
Tactic: cases h
Cleared hypotheses: g, inst_3, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := Y ⟶ cokernel f) (CategoryStruct.comp (Y := cokernel g) (cokernel.π g) (Iso.inv (cokernelIsoOfEq h)))
    (cokernel.π f)
have refl : ∀ [inst_4 : HasCokernel f],
  Eq (α := Y ⟶ cokernel f) (CategoryStruct.comp (Y := cokernel f) (cokernel.π f) (Iso.inv (cokernelIsoOfEq sorry)))
    (cokernel.π f)
Tactic: cases h
Cleared hypotheses: g, inst_3, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := cokernel f ⟶ Z) (CategoryStruct.comp (Y := cokernel g) (Iso.hom (cokernelIsoOfEq h)) (cokernel.desc g e he))
    (cokernel.desc f e ⋯)
have refl : ∀ [inst_4 : HasCokernel f] (he : f ≫ e = 0),
  Eq (α := cokernel f ⟶ Z) (CategoryStruct.comp (Y := cokernel f) (Iso.hom (cokernelIsoOfEq sorry)) (cokernel.desc f e he))
    (cokernel.desc f e sorry)
Tactic: cases h
Cleared hypotheses: g, inst_3, h, he
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := cokernel g ⟶ Z) (CategoryStruct.comp (Y := cokernel f) (Iso.inv (cokernelIsoOfEq h)) (cokernel.desc f e he))
    (cokernel.desc g e ⋯)
have refl : ∀ [inst_4 : HasCokernel f],
  Eq (α := cokernel f ⟶ Z) (CategoryStruct.comp (Y := cokernel f) (Iso.inv (cokernelIsoOfEq sorry)) (cokernel.desc f e he))
    (cokernel.desc f e sorry)
Tactic: cases h
Cleared hypotheses: g, inst_3, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := cokernel f ≅ cokernel h) (Iso.trans (Y := cokernel g) (cokernelIsoOfEq w₁) (cokernelIsoOfEq w₂))
    (cokernelIsoOfEq ⋯)
have refl : ∀ [inst_5 : HasCokernel f] (w₂ : f = h),
  Eq (α := cokernel f ≅ cokernel h) (Iso.trans (Y := cokernel f) (cokernelIsoOfEq sorry) (cokernelIsoOfEq w₂))
    (cokernelIsoOfEq sorry)
Tactic: cases w₁
Cleared hypotheses: g, inst_3, w₁, w₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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)
⊢ f ≫ g ≫ Cofork.π s = 0
have rw : (f ≫ g) ≫ Cofork.π s = 0
Tactic: rw [← Category.assoc, CokernelCofork.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ f ≫ g ≫ Cofork.π s = 0
have rw₁ : Eq.{v + 1} (α := X ⟶ s.pt) 0 0
Tactic: rw [← Category.assoc, CokernelCofork.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ m = (fun (s : CokernelCofork (f ≫ g)) ↦ (cokernel.desc f (g ≫ Cofork.π s) ⋯ : cokernel f ⟶ s.pt)) s
have simp_rw : m = cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) sorry) ≫ m) sorry
Tactic: simp_rw [← w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ m = cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (Z := cokernel f) (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯
have 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) sorry) ≫ m) sorry)
Tactic: apply coequalizer.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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 ≫ g)) (f ≫ g ≫ cokernel.π (f ≫ g)) 0
have rw : Eq (α := X ⟶ cokernel (f ≫ g)) ((f ≫ g) ≫ cokernel.π (f ≫ g)) 0
Tactic: rw [← Category.assoc, cokernel.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := X ⟶ cokernel (f ≫ g)) (f ≫ g ≫ cokernel.π (f ≫ g)) 0
have rw₁ : Eq.{v + 1} (α := X ⟶ cokernel (f ≫ g)) 0 0
Tactic: rw [← Category.assoc, cokernel.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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 (α := Y ⟶ cokernel (f ≫ g)) (g ≫ cokernel.π (f ≫ g)) 0
have rw : Eq (α := X ⟶ cokernel (f ≫ g)) ((f ≫ g) ≫ cokernel.π (f ≫ g)) (f ≫ 0)
Tactic: rw [← cancel_epi f, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := kernel f ⟶ F.I) (kernel.ι f ≫ F.e) 0
have rw : Eq (α := kernel f ⟶ Y) ((kernel.ι f ≫ F.e) ≫ F.m) (0 ≫ F.m)
Tactic: rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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)
⊢ Eq (α := kernel f ⟶ F.I) (kernel.ι f ≫ F.e) 0
have rw₁ : Eq (α := kernel f ⟶ Y) ((kernel.ι f ≫ F.e) ≫ F.m) 0
Tactic: rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := kernel f ⟶ F.I) (kernel.ι f ≫ F.e) 0
have rw₂ : Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ F.e ≫ F.m) 0
Tactic: rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := kernel f ⟶ F.I) (kernel.ι f ≫ F.e) 0
have rw₃ : Eq (α := kernel f ⟶ Y) (kernel.ι f ≫ f) 0
Tactic: rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
⊢ Eq (α := kernel f ⟶ F.I) (kernel.ι f ≫ F.e) 0
have rw₄ : Eq.{v + 1} (α := kernel f ⟶ Y) 0 0
Tactic: rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (hypothesis)
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 (α := image f ⟶ cokernel f) (image.ι f ≫ cokernel.π f) 0
have w : Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0
Tactic: have w := cokernel.condition f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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) (f ≫ cokernel.π f) 0
have lhs : f ≫ cokernel.π f
Tactic: lhs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
| f ≫ cokernel.π f
have a : f
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
| f ≫ cokernel.π f
have a₁ : cokernel.π f
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
| f
have a : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)
Tactic: rw [← image.fac f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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) (f ≫ cokernel.π f) 0
have a : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)
Tactic: lhs
          congr
          rw [← image.fac f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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)
| Eq (α := X ⟶ cokernel f) (f ≫ cokernel.π f) 0
have a₁ : cokernel.π f
Tactic: lhs
          congr
          rw [← image.fac f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (hypothesis)
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 (α := image f ⟶ cokernel f) (image.ι f ≫ cokernel.π f) 0
have w₁ : 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]
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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 (X := image f) (image.ι f)) (f ≫ cokernel.π (image.ι f)) 0
have lhs : f ≫ cokernel.π (image.ι f)
Tactic: lhs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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)
| f ≫ cokernel.π (image.ι f)
have a : f
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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
| f ≫ cokernel.π (image.ι f)
have a₁ : cokernel.π (image.ι f)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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)
| f
have a : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)
Tactic: rw [← image.fac f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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 (X := image f) (image.ι f)) (f ≫ cokernel.π (image.ι f)) 0
have a : CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f)
Tactic: lhs
          congr
          rw [← image.fac f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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)
| Eq (α := X ⟶ cokernel (X := image f) (image.ι f)) (f ≫ cokernel.π (image.ι f)) 0
have a₁ : cokernel.π (image.ι f)
Tactic: lhs
          congr
          rw [← image.fac f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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 (X := image f) (image.ι f)) (f ≫ cokernel.π (image.ι f)) 0
have conv : Eq (α := X ⟶ cokernel (X := image f) (image.ι f))
  (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) ≫ cokernel.π (image.ι f)) 0
Tactic: conv =>
          lhs
          congr
          rw [← image.fac f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Kernels (goal)
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 (X := image f) (image.ι f))
    (CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f) ≫ cokernel.π (image.ι f)) 0
have rw : 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]