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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0
rw : (f ≫ biprod.inl) ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
rw₁ : (f ≫ biprod.inl) ≫ s.π - (g ≫ biprod.inr) ≫ s.π = 0
rw₂ : HSub.hSub (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) (g ≫ biprod.inr) ≫ s.π = 0
rw₃ : HAdd.hAdd (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) (-g ≫ biprod.inr) ≫ s.π = 0
rw₄ : HAdd.hAdd (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) ((-g) ≫ biprod.inr) ≫ s.π = 0
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
have rw₅ : biprod.lift f (-g) ≫ s.π = 0
Tactic: rw [← Category.assoc, ← Category.assoc, ← sub_comp, sub_eq_add_neg, ← neg_comp, ←
            biprod.lift_eq, Cofork.condition s, zero_comp]
-- 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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0
rw : (f ≫ biprod.inl) ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
rw₁ : (f ≫ biprod.inl) ≫ s.π - (g ≫ biprod.inr) ≫ s.π = 0
rw₂ : HSub.hSub (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) (g ≫ biprod.inr) ≫ s.π = 0
rw₃ : HAdd.hAdd (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) (-g ≫ biprod.inr) ≫ s.π = 0
rw₄ : HAdd.hAdd (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) ((-g) ≫ biprod.inr) ≫ s.π = 0
rw₅ : biprod.lift f (-g) ≫ s.π = 0
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
have rw₆ : Eq (α := X ⟶ s.pt) (0 ≫ s.π) 0
Tactic: rw [← Category.assoc, ← Category.assoc, ← sub_comp, sub_eq_add_neg, ← neg_comp, ←
            biprod.lift_eq, Cofork.condition s, zero_comp]
-- 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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0
rw : (f ≫ biprod.inl) ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
rw₁ : (f ≫ biprod.inl) ≫ s.π - (g ≫ biprod.inr) ≫ s.π = 0
rw₂ : HSub.hSub (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) (g ≫ biprod.inr) ≫ s.π = 0
rw₃ : HAdd.hAdd (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) (-g ≫ biprod.inr) ≫ s.π = 0
rw₄ : HAdd.hAdd (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) ((-g) ≫ biprod.inr) ≫ s.π = 0
rw₅ : biprod.lift f (-g) ≫ s.π = 0
rw₆ : Eq (α := X ⟶ s.pt) (0 ≫ s.π) 0
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
have rw₇ : Eq.{v + 1} (α := X ⟶ s.pt) 0 0
Tactic: rw [← Category.assoc, ← Category.assoc, ← sub_comp, sub_eq_add_neg, ← neg_comp, ←
            biprod.lift_eq, Cofork.condition s, zero_comp]
-- 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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) (biproductToPushoutCofork f g))
      (Cofork.π (biproductToPushoutCofork f g))
      ((fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
          (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ : pushout f g ⟶ s.pt))
        s) =
    s.π
have h₀ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) (biproductToPushoutCofork f g))
      (Cofork.π (biproductToPushoutCofork f g))
      ((fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
          (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry : pushout f g ⟶ s.pt))
        s)) =
  biprod.inl ≫ s.π
Tactic: apply biprod.hom_ext'
-- 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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) (biproductToPushoutCofork f g))
        (Cofork.π (biproductToPushoutCofork f g))
        ((fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
            (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ : pushout f g ⟶ s.pt))
          s)) =
    biprod.inl ≫ s.π
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) (biproductToPushoutCofork f g))
      (Cofork.π (biproductToPushoutCofork f g))
      ((fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
          (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ : pushout f g ⟶ s.pt))
        s) =
    s.π
have h₁ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inr
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) (biproductToPushoutCofork f g))
      (Cofork.π (biproductToPushoutCofork f g))
      ((fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
          (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry : pushout f g ⟶ s.pt))
        s)) =
  biprod.inr ≫ s.π
Tactic: apply biprod.hom_ext'
-- 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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) (biproductToPushoutCofork f g) ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = s.π
⊢ m =
    (fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
        (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ : pushout f g ⟶ s.pt))
      s
have h₀ : pushout.inl f g ≫ m =
  CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
    ((fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
        (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry : pushout f g ⟶ s.pt))
      s)
Tactic: apply pushout.hom_ext
-- 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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0
m : Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) (biproductToPushoutCofork f g) ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = s.π
h₀ :
  pushout.inl f g ≫ m =
    CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
      ((fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
          (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ : pushout f g ⟶ s.pt))
        s)
⊢ m =
    (fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
        (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ : pushout f g ⟶ s.pt))
      s
have h₁ : pushout.inr f g ≫ m =
  CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
    ((fun (s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0) ↦
        (pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) sorry : pushout f g ⟶ s.pt))
      s)
Tactic: apply pushout.hom_ext
-- 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 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
⊢ 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 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)
⊢ 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 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 :
  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 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 :
  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)
⊢ f ≫ d = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g)) ≫ d
have rw : f ≫ d = f ≫ d
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 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 :
  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)
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g)) ≫ d = biprod.inl ≫ u
have rw : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d) = biprod.inl ≫ 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 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 :
  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)
rw : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g) ≫ d) = biprod.inl ≫ u
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g)) ≫ d = biprod.inl ≫ u
have rw₁ : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc 0 e) = biprod.inl ≫ 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 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 :
  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)
⊢ e = 0
have this₁ : f ≫ d = 0
Tactic: have : f ≫ d = 0 := calc
      f ≫ d = (biprod.inl ≫ biprod.desc f (-g)) ≫ d := by rw [biprod.inl_desc]
      _ = biprod.inl ≫ u := by rw [Category.assoc, hd]
      _ = 0 := biprod.inl_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 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 : f ≫ d = 0
⊢ e = 0
have this₁ : d = 0
Tactic: have : d = 0 := (cancel_epi f).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 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 = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc 0 e)
have rw : e = e
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 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
⊢ 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)
have rw : 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) ≫ 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 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
⊢ 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)
have rw : 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: 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 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
⊢ 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)
have rw : 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: 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 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 = 0
have e₁ : e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc 0 e)
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 = 0
have 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)
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 _ _