awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi f
R : C
e : Y ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.snd f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc 0 e
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc 0 e)
this_2 : f ≫ d = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc 0 e)
e₂ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc 0 e) =
    CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g) ≫ d)
⊢ e = 0
have e₃ : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g) ≫ d) =
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g) ≫ 0)
Tactic: calc
      e = biprod.inr ≫ biprod.desc (0 : X ⟶ R) e := by rw [biprod.inr_desc]
      _ = biprod.inr ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
      _ = biprod.inr ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
      _ = (biprod.inr ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
      _ = 0 := HasZeroMorphisms.comp_zero _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi f
R : C
e : Y ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.snd f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc 0 e
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc 0 e)
this_2 : f ≫ d = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc 0 e)
e₂ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc 0 e) =
    CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g) ≫ d)
e₃ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g) ≫ d) =
    CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g) ≫ 0)
⊢ e = 0
have e₄ : Eq (α := Y ⟶ R) (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g) ≫ 0))
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g)) ≫ 0)
Tactic: calc
      e = biprod.inr ≫ biprod.desc (0 : X ⟶ R) e := by rw [biprod.inr_desc]
      _ = biprod.inr ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
      _ = biprod.inr ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
      _ = (biprod.inr ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
      _ = 0 := HasZeroMorphisms.comp_zero _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
⊢ e = 0
have hu : Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
  (0 : pullback f g ⟶ R)
Tactic: have hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0 := by simpa [u]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
⊢ e = 0
have have : ∀
  (this :
    IsColimit (F :=
      parallelPair (X :=
        Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
          (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
        (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
      (CokernelCofork.ofπ (biprod.desc f (-g)) sorry)),
  e = 0
Tactic: have :=
      epiIsCokernelOfKernel _
        (PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
⊢ e = 0
have obtain : ∀
  (d :
    Cocone.pt (F :=
        parallelPair (X :=
          Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
            (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
          (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
        (CokernelCofork.ofπ (biprod.desc f (-g)) sorry) ⟶
      R)
  (hd : Cofork.π (CokernelCofork.ofπ (biprod.desc f (-g)) sorry) ≫ d = u), e = 0
Tactic: obtain ⟨d, hd⟩ := CokernelCofork.IsColimit.desc' this u hu
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
⊢ (-g) ≫ d = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g)) ≫ d
have rw : (-g) ≫ d = (-g) ≫ d
Tactic: rw [biprod.inr_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g)) ≫ d = biprod.inr ≫ u
have rw : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g) ≫ d) = biprod.inr ≫ u
Tactic: rw [Category.assoc, hd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
rw : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g) ≫ d) = biprod.inr ≫ u
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g)) ≫ d = biprod.inr ≫ u
have rw₁ : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc e 0) = biprod.inr ≫ u
Tactic: rw [Category.assoc, hd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
⊢ e = 0
have this₁ : (-g) ≫ d = 0
Tactic: have : (-g) ≫ d = 0 := calc
      (-g) ≫ d = (biprod.inr ≫ biprod.desc f (-g)) ≫ d := by rw [biprod.inr_desc]
      _ = biprod.inr ≫ u := by rw [Category.assoc, hd]
      _ = 0 := biprod.inr_desc _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
this : (-g) ≫ d = 0
⊢ e = 0
have this₁ : d = 0
Tactic: have : d = 0 := (cancel_epi (-g)).1 (by simpa)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
this_2 : (-g) ≫ d = 0
this : d = 0
⊢ e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0)
have rw : e = e
Tactic: rw [biprod.inl_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
this_2 : (-g) ≫ d = 0
this : d = 0
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0) =
    CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d)
have rw : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d) =
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d)
Tactic: rw [← hd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
this_2 : (-g) ≫ d = 0
this : d = 0
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d) =
    CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ 0)
have rw : Eq (α := X ⟶ R) (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ 0))
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ 0))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
this_2 : (-g) ≫ d = 0
this : d = 0
⊢ Eq (α := X ⟶ R) (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ 0))
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g)) ≫ 0)
have rw : Eq (α := X ⟶ R) (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g)) ≫ 0)
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g)) ≫ 0)
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
this_2 : (-g) ≫ d = 0
this : d = 0
⊢ e = 0
have e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0)
Tactic: calc
      e = biprod.inl ≫ biprod.desc e (0 : Y ⟶ R) := by rw [biprod.inl_desc]
      _ = biprod.inl ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
      _ = biprod.inl ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
      _ = (biprod.inl ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
      _ = 0 := HasZeroMorphisms.comp_zero _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
this_2 : (-g) ≫ d = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0)
⊢ e = 0
have e₂ : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0) =
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d)
Tactic: calc
      e = biprod.inl ≫ biprod.desc e (0 : Y ⟶ R) := by rw [biprod.inl_desc]
      _ = biprod.inl ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
      _ = biprod.inl ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
      _ = (biprod.inl ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
      _ = 0 := HasZeroMorphisms.comp_zero _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
this_2 : (-g) ≫ d = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0)
e₂ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0) =
    CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d)
⊢ e = 0
have e₃ : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d) =
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ 0)
Tactic: calc
      e = biprod.inl ≫ biprod.desc e (0 : Y ⟶ R) := by rw [biprod.inl_desc]
      _ = biprod.inl ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
      _ = biprod.inl ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
      _ = (biprod.inl ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
      _ = 0 := HasZeroMorphisms.comp_zero _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
R : C
e : X ⟶ R
h : Eq (α := pullback f g ⟶ R) (pullback.fst f g ≫ e) 0
u : biprod.{v, u} X Y ⟶ R := biprod.desc e 0
hu :
  Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)
this_1 :
  IsColimit (F :=
    parallelPair (X :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0)
        (PullbackToBiproductIsKernel.pullbackToBiproductFork f g))
      (Fork.ι (PullbackToBiproductIsKernel.pullbackToBiproductFork f g)) 0)
    (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : Eq (α := biprod.{v, u} X Y ⟶ R) (biprod.desc f (-g) ≫ d) (biprod.desc e 0)
this_2 : (-g) ≫ d = 0
this : d = 0
e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0)
e₂ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0) =
    CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d)
e₃ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d) =
    CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ 0)
⊢ e = 0
have e₄ : Eq (α := X ⟶ R) (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ 0))
  (CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g)) ≫ 0)
Tactic: calc
      e = biprod.inl ≫ biprod.desc e (0 : Y ⟶ R) := by rw [biprod.inl_desc]
      _ = biprod.inl ≫ biprod.desc f (-g) ≫ d := by rw [← hd]
      _ = biprod.inl ≫ biprod.desc f (-g) ≫ 0 := by rw [this]
      _ = (biprod.inl ≫ biprod.desc f (-g)) ≫ 0 := by rw [← Category.assoc]
      _ = 0 := HasZeroMorphisms.comp_zero _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi f
s : PullbackCone f g
hs : IsLimit s
⊢ Epi s.snd
have this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.right)
Tactic: haveI : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.right) :=
    Abelian.epi_pullback_of_epi_f f g
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
s : PullbackCone f g
hs : IsLimit s
⊢ Epi s.fst
have this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.left)
Tactic: haveI : Epi (NatTrans.app (limit.cone (cospan f g)).π WalkingCospan.left) :=
    Abelian.epi_pullback_of_epi_g f g