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_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 : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
⊢ CategoryStruct.comp (Y := Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))
      ((fun (x : Fork f 0) ↦ (0 : x.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))) s)
      (Fork.ι (KernelFork.ofι (Z := 0) 0 ⋯)) =
    s.ι
have rw : Eq.{v + 1} (α := s.pt ⟶ X)
  (CategoryStruct.comp (Y := Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 sorry))
    ((fun (x : Fork f 0) ↦ (0 : x.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 sorry))) s)
    (Fork.ι (KernelFork.ofι (Z := 0) 0 sorry)))
  0
Tactic: rw [hf _ _ (KernelFork.condition s), zero_comp]
-- 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 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
rw :
  Eq.{v + 1} (α := s.pt ⟶ X)
    (CategoryStruct.comp (Y := Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))
      ((fun (x : Fork f 0) ↦ (0 : x.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))) s)
      (Fork.ι (KernelFork.ofι (Z := 0) 0 ⋯)))
    0
⊢ CategoryStruct.comp (Y := Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))
      ((fun (x : Fork f 0) ↦ (0 : x.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))) s)
      (Fork.ι (KernelFork.ofι (Z := 0) 0 ⋯)) =
    s.ι
have rw₁ : Eq.{v + 1} (α := s.pt ⟶ X) 0 0
Tactic: rw [hf _ _ (KernelFork.condition s), zero_comp]
-- 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 : HasZeroObject.{v, u} C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Z ⟶ X), g ≫ f = 0 → g = 0
s : Fork f 0
m : s.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯)
h : m ≫ Fork.ι (KernelFork.ofι (Z := 0) 0 ⋯) = s.ι
⊢ m = (fun (x : Fork f 0) ↦ (0 : x.pt ⟶ Cone.pt.{0, v, 0, u} (F := parallelPair f 0) (KernelFork.ofι (Z := 0) 0 ⋯))) s
have dsimp : m = 0
Tactic: dsimp
-- 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
Z : C
l : X ⟶ Z
i : Z ≅ Y
h_1 : l ≫ i.hom = f
s_1 : KernelFork f
hs : IsLimit s_1
s : Fork l 0
m : s.pt ⟶ Cone.pt (F := parallelPair l 0) (KernelFork.ofι (Fork.ι s_1) ⋯)
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι s_1) ⋯) = s.ι
⊢ m = (fun (s : Fork l 0) ↦ (hs.lift (KernelFork.ofι s.ι ⋯) : (KernelFork.ofι s.ι ⋯).pt ⟶ s_1.pt)) s
have apply : m ≫ Fork.ι s_1 =
  (fun (s : Fork l 0) ↦ (hs.lift (KernelFork.ofι s.ι sorry) : (KernelFork.ofι s.ι sorry).pt ⟶ s_1.pt)) s ≫ Fork.ι s_1
Tactic: apply Fork.IsLimit.hom_ext hs
-- 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
j : WalkingParallelPair
⊢ s.π.app j = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) j
have zero : s.π.app zero = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l sorry)) zero
Tactic: cases j
Cleared hypotheses: j
-- 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
j : WalkingParallelPair
zero :
  s.π.app WalkingParallelPair.zero = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) WalkingParallelPair.zero
⊢ s.π.app j = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) j
have one : s.π.app one = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l sorry)) one
Tactic: cases j
Cleared hypotheses: j
-- 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.symm.hom ≫ NatTrans.app (Cone.π (KernelFork.ofι l ⋯)) one
have one : s.π.app one = i.inv ≫ l ≫ f
Tactic: dsimp
-- 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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.inv ≫ l ≫ f
have one : s.π.app one = i.inv ≫ (i.hom ≫ Fork.ι s) ≫ f
Tactic: rw [← 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
s : CokernelCofork f
⊢ f ≫ Cofork.π s = 0
have rw : Eq (α := X ⟶ s.pt) (0 ≫ Cofork.π s) 0
Tactic: rw [Cofork.condition, zero_comp]
-- 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
s : CokernelCofork f
rw : Eq (α := X ⟶ s.pt) (0 ≫ Cofork.π s) 0
⊢ f ≫ Cofork.π s = 0
have rw₁ : Eq.{v + 1} (α := X ⟶ s.pt) 0 0
Tactic: rw [Cofork.condition, zero_comp]
-- 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
Z : C
π : Y ⟶ Z
w : f ≫ π = 0
⊢ f ≫ π = 0 ≫ π
have rw : Eq (α := X ⟶ Z) 0 (0 ≫ π)
Tactic: rw [w, zero_comp]
-- 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
Z : C
π : Y ⟶ Z
w : f ≫ π = 0
rw : Eq (α := X ⟶ Z) 0 (0 ≫ π)
⊢ f ≫ π = 0 ≫ π
have rw₁ : Eq.{v + 1} (α := X ⟶ Z) 0 0
Tactic: rw [w, zero_comp]
-- 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
s : Cofork f 0
j : WalkingParallelPair
⊢ s.ι.app j ≫ Iso.hom (Iso.refl s.pt) = (Cofork.ofπ s.π ⋯).ι.app j
have zero : s.ι.app zero ≫ Iso.hom (Iso.refl s.pt) = (Cofork.ofπ s.π sorry).ι.app zero
Tactic: cases j
Cleared hypotheses: j
-- 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
s : Cofork f 0
j : WalkingParallelPair
zero : s.ι.app WalkingParallelPair.zero ≫ Iso.hom (Iso.refl s.pt) = (Cofork.ofπ s.π ⋯).ι.app WalkingParallelPair.zero
⊢ s.ι.app j ≫ Iso.hom (Iso.refl s.pt) = (Cofork.ofπ s.π ⋯).ι.app j
have one : s.ι.app one ≫ Iso.hom (Iso.refl s.pt) = (Cofork.ofπ s.π sorry).ι.app one
Tactic: cases j
Cleared hypotheses: j
-- 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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
rw : f ≫ π = 0
⊢ f ≫ π' = 0
have rw₁ : Eq.{v + 1} (α := X ⟶ P) 0 0
Tactic: rw [← h, 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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
j : WalkingParallelPair
⊢ (CokernelCofork.ofπ π w).ι.app j ≫ Iso.hom (Iso.refl (CokernelCofork.ofπ π w).pt) =
    NatTrans.app (Cocone.ι (CokernelCofork.ofπ π' ⋯)) j
have zero : (CokernelCofork.ofπ π w).ι.app zero ≫ Iso.hom (Iso.refl (CokernelCofork.ofπ π w).pt) =
  NatTrans.app (Cocone.ι (CokernelCofork.ofπ π' sorry)) zero
Tactic: cases j
Cleared hypotheses: j
-- 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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
j : WalkingParallelPair
zero :
  (CokernelCofork.ofπ π w).ι.app WalkingParallelPair.zero ≫ Iso.hom (Iso.refl (CokernelCofork.ofπ π w).pt) =
    NatTrans.app (Cocone.ι (CokernelCofork.ofπ π' ⋯)) WalkingParallelPair.zero
⊢ (CokernelCofork.ofπ π w).ι.app j ≫ Iso.hom (Iso.refl (CokernelCofork.ofπ π w).pt) =
    NatTrans.app (Cocone.ι (CokernelCofork.ofπ π' ⋯)) j
have one : (CokernelCofork.ofπ π w).ι.app one ≫ Iso.hom (Iso.refl (CokernelCofork.ofπ π w).pt) =
  NatTrans.app (Cocone.ι (CokernelCofork.ofπ π' sorry)) one
Tactic: cases j
Cleared hypotheses: j
-- 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
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
j : WalkingParallelPair
⊢ t.ι.app j ≫ desc s = s.ι.app j
have zero : t.ι.app zero ≫ desc s = s.ι.app zero
Tactic: cases j
Cleared hypotheses: j
-- 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
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
j : WalkingParallelPair
zero : t.ι.app WalkingParallelPair.zero ≫ desc s = s.ι.app WalkingParallelPair.zero
⊢ t.ι.app j ≫ desc s = s.ι.app j
have one : t.ι.app one ≫ desc s = s.ι.app one
Tactic: cases j
Cleared hypotheses: j
-- 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 Q : C
f : X ⟶ Y
p : Y ⟶ Q
w : f ≫ p = 0
h : {A : C} → (k : Y ⟶ A) → f ≫ k = 0 → { l : Q ⟶ A // p ≫ l = k }
hp : Epi p
A : C
k : Y ⟶ A
hk : f ≫ k = 0
m : Q ⟶ A
hm : p ≫ m = k
⊢ m = (fun {x : C} (k : Y ⟶ x) (hk : f ≫ k = 0) ↦ (↑(h k hk) : Q ⟶ x)) k hk
have rw : p ≫ m = p ≫ (fun {x : C} (k : Y ⟶ x) (hk : f ≫ k = 0) ↦ (↑(h k hk) : Q ⟶ x)) k hk
Tactic: rw [← cancel_epi p, (h k hk).2, hm]
-- 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 Q : C
f : X ⟶ Y
p : Y ⟶ Q
w : f ≫ p = 0
h : {A : C} → (k : Y ⟶ A) → f ≫ k = 0 → { l : Q ⟶ A // p ≫ l = k }
hp : Epi p
A : C
k : Y ⟶ A
hk : f ≫ k = 0
m : Q ⟶ A
hm : p ≫ m = k
rw : p ≫ m = p ≫ (fun {x : C} (k : Y ⟶ x) (hk : f ≫ k = 0) ↦ (↑(h k hk) : Q ⟶ x)) k hk
rw₁ : p ≫ m = k
⊢ m = (fun {x : C} (k : Y ⟶ x) (hk : f ≫ k = 0) ↦ (↑(h k hk) : Q ⟶ x)) k hk
have rw₂ : k = k
Tactic: rw [← cancel_epi p, (h k hk).2, hm]
-- 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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
⊢ h ≫ Cofork.π c = 0
have rw : (g ≫ f) ≫ Cofork.π c = 0
Tactic: rw [hh]
-- 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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
⊢ f ≫ s.π = 0 ≫ s.π
have a : g ≫ f ≫ s.π = g ≫ 0 ≫ s.π
Tactic: apply hg.left_cancellation
-- 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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
⊢ g ≫ f ≫ s.π = g ≫ 0 ≫ s.π
have a : 0 ≫ s.π = g ≫ 0 ≫ s.π
Tactic: rw [← Category.assoc, ← hh, s.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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (Cofork.π c) ⋯) ≫ m = s.π
⊢ m = (↑l : c.pt ⟶ s'.pt)
have apply : Cofork.π c ≫ m = Cofork.π c ≫ (↑l : c.pt ⟶ s'.pt)
Tactic: apply Cofork.IsColimit.hom_ext i
-- 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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (Cofork.π c) ⋯) ≫ m = s.π
⊢ Cofork.π c ≫ m = Cofork.π c ≫ (↑l : c.pt ⟶ s'.pt)
have hm₁ : Cofork.π c ≫ m = s.π
Tactic: rw [Cofork.π_ofπ] at hm
Cleared hypotheses: hm
-- 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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l : c.pt ⟶ s'.pt // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π c ≫ m = s.π
⊢ Cofork.π c ≫ m = Cofork.π c ≫ (↑l : c.pt ⟶ s'.pt)
have rw : s.π = Cofork.π c ≫ (↑l : c.pt ⟶ s'.pt)
Tactic: rw [hm]
-- 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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ f ≫ Cofork.π s = 0 ≫ Cofork.π s
have rw : h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s
Tactic: rw [← cancel_epi g, ← Category.assoc, ← hh]
-- 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
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.π
⊢ m = (fun (s : Cofork f 0) ↦ (i.desc (CokernelCofork.ofπ s.π ⋯) : c.pt ⟶ (CokernelCofork.ofπ s.π ⋯).pt)) s
have apply : Cofork.π c ≫ m =
  Cofork.π c ≫ (fun (s : Cofork f 0) ↦ (i.desc (CokernelCofork.ofπ s.π sorry) : c.pt ⟶ (CokernelCofork.ofπ s.π sorry).pt)) s
Tactic: apply Cofork.IsColimit.hom_ext i
-- 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
hf : f = 0
⊢ f ≫ 𝟙 Y = 0
have rw : Eq.{v + 1} (α := X ⟶ Y) (0 ≫ 𝟙 Y) 0
Tactic: rw [hf, zero_comp]
-- 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
hf : f = 0
rw : Eq.{v + 1} (α := X ⟶ Y) (0 ≫ 𝟙 Y) 0
⊢ f ≫ 𝟙 Y = 0
have rw₁ : Eq.{v + 1} (α := X ⟶ Y) 0 0
Tactic: rw [hf, zero_comp]
-- 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
c : CokernelCofork f
hf : Epi f
h : IsZero.{v, u} c.pt
s : CokernelCofork f
⊢ Cofork.π c ≫ (fun (x : CokernelCofork f) ↦ (0 : c.pt ⟶ x.pt)) s = Cofork.π s
have rw : 0 = Cofork.π s
Tactic: rw [comp_zero, ← cancel_epi f, comp_zero, s.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
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
⊢ Cofork.π c ≫ (fun (x : CokernelCofork f) ↦ (0 : c.pt ⟶ x.pt)) s = Cofork.π s
have rw₁ : f ≫ 0 = f ≫ Cofork.π s
Tactic: rw [comp_zero, ← cancel_epi f, comp_zero, s.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
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
⊢ Cofork.π c ≫ (fun (x : CokernelCofork f) ↦ (0 : c.pt ⟶ x.pt)) s = Cofork.π s
have rw₂ : 0 = f ≫ Cofork.π s
Tactic: rw [comp_zero, ← cancel_epi f, comp_zero, s.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
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
⊢ Cofork.π c ≫ (fun (x : CokernelCofork f) ↦ (0 : c.pt ⟶ x.pt)) s = Cofork.π s
have rw₃ : Eq.{v + 1} (α := X ⟶ s.pt) 0 0
Tactic: rw [comp_zero, ← cancel_epi f, comp_zero, s.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
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
⊢ f ≫ e.inv ≫ s = 0
have rw : f' ≫ e.hom ≫ e.inv ≫ s = 0
Tactic: rw [iff, e.hom_inv_id_assoc, hs]
-- 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
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
⊢ f ≫ e.inv ≫ s = 0
have rw₂ : Eq.{v + 1} (α := X' ⟶ Z') 0 0
Tactic: rw [iff, e.hom_inv_id_assoc, hs]
-- 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
c : CokernelCofork f
hc : IsColimit c
inst_2 : Epi f
⊢ IsZero.{v, u} c.pt
have this : Epi (Cofork.π c)
Tactic: have := Cofork.IsColimit.epi hc
-- 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
c : CokernelCofork f
hc : IsColimit c
inst_2 : Epi f
this : Epi (Cofork.π c)
⊢ IsZero.{v, u} c.pt
have rw : Eq.{v + 1} (α := c.pt ⟶ c.pt) (𝟙 c.pt) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi c.π, ← cancel_epi f,
    c.condition_assoc, comp_zero, comp_zero, zero_comp]
-- 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
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
⊢ IsZero.{v, u} c.pt
have rw₁ : Cofork.π c ≫ 𝟙 c.pt = Cofork.π c ≫ 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi c.π, ← cancel_epi f,
    c.condition_assoc, comp_zero, comp_zero, zero_comp]
-- 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
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
⊢ IsZero.{v, u} c.pt
have rw₂ : f ≫ Cofork.π c ≫ 𝟙 c.pt = f ≫ Cofork.π c ≫ 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi c.π, ← cancel_epi f,
    c.condition_assoc, comp_zero, comp_zero, zero_comp]
-- 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
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
⊢ IsZero.{v, u} c.pt
have rw₃ : 0 ≫ 𝟙 c.pt = f ≫ Cofork.π c ≫ 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi c.π, ← cancel_epi f,
    c.condition_assoc, comp_zero, comp_zero, zero_comp]
-- 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
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
⊢ IsZero.{v, u} c.pt
have rw₄ : 0 ≫ 𝟙 c.pt = f ≫ 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi c.π, ← cancel_epi f,
    c.condition_assoc, comp_zero, comp_zero, zero_comp]
-- 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
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
⊢ IsZero.{v, u} c.pt
have rw₅ : Eq.{v + 1} (α := X ⟶ c.pt) (0 ≫ 𝟙 c.pt) 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi c.π, ← cancel_epi f,
    c.condition_assoc, comp_zero, comp_zero, zero_comp]
-- 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
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
⊢ IsZero.{v, u} c.pt
have rw₆ : Eq.{v + 1} (α := X ⟶ c.pt) 0 0
Tactic: rw [IsZero.iff_id_eq_zero, ← cancel_epi c.π, ← cancel_epi f,
    c.condition_assoc, comp_zero, comp_zero, zero_comp]
-- 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'
⊢ f ≫ Arrow.Hom.right φ ≫ Cofork.π cc' = 0
have erw : Arrow.Hom.left φ ≫ (Arrow.mk f').hom ≫ Cofork.π cc' = 0
Tactic: erw [← Arrow.w_assoc φ, condition, comp_zero]
-- 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
⊢ f ≫ Arrow.Hom.right φ ≫ Cofork.π cc' = 0
have erw₁ : Eq (α := X ⟶ cc'.pt) (Arrow.Hom.left φ ≫ 0) 0
Tactic: erw [← Arrow.w_assoc φ, condition, comp_zero]