awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)

Tactic:
simpa [u]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ 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]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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)
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)) ⋯)),
    e = 0
⊢ e = 0

Tactic:
have :=
      epiIsCokernelOfKernel _
        (PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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)) ⋯)
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)) ⋯) ⟶
        R)
    (hd : Cofork.π (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯) ≫ d = u), e = 0
⊢ e = 0

Tactic:
obtain ⟨d, hd⟩ := CokernelCofork.IsColimit.desc' this u hu

Premises used: CategoryTheory.Limits.CokernelCofork.IsColimit.desc'
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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 rw₁ : f ≫ d = f ≫ d
⊢ f ≫ d = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g)) ≫ d

Tactic:
rw [biprod.inl_desc]

Premises used: CategoryTheory.Limits.biprod.inl_desc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw₁ rw₂ : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc 0 e) = biprod.inl ≫ u
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc f (-g)) ≫ d = biprod.inl ≫ u

Tactic:
rw [Category.assoc, hd]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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 = 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 _ _
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ f ≫ d = f ≫ 0

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ d = 0

Tactic:
have : d = 0 := (cancel_epi f).1 (by simpa)
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw rw₁ : e = e
⊢ e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc 0 e)

Tactic:
rw [biprod.inr_desc]

Premises used: CategoryTheory.Limits.biprod.inr_desc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw 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)
⊢ 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:
rw [← hd]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw 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))
⊢ 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:
rw [this]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw 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)
⊢ 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]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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) 0

Tactic:
HasZeroMorphisms.comp_zero _ _

Premises used: CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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₄ :
  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)
⊢ e = 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 _ _

Premises used: CategoryTheory.Limits.biprod.desc, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.biprod.inr, OfNat.ofNat, Neg.neg, CategoryTheory.Limits.HasZeroMorphisms.comp_zero
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ Eq (α := pullback f g ⟶ R) (PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u : pullback f g ⟶ R)
    (0 : pullback f g ⟶ R)

Tactic:
simpa [u]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ 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]
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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)
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)) ⋯)),
    e = 0
⊢ e = 0

Tactic:
have :=
      epiIsCokernelOfKernel _
        (PullbackToBiproductIsKernel.isLimitPullbackToBiproduct f g)
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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)) ⋯)
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)) ⋯) ⟶
        R)
    (hd : Cofork.π (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯) ≫ d = u), e = 0
⊢ e = 0

Tactic:
obtain ⟨d, hd⟩ := CokernelCofork.IsColimit.desc' this u hu

Premises used: CategoryTheory.Limits.CokernelCofork.IsColimit.desc'
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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 rw₁ : (-g) ≫ d = (-g) ≫ d
⊢ (-g) ≫ d = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g)) ≫ d

Tactic:
rw [biprod.inr_desc]

Premises used: CategoryTheory.Limits.biprod.inr_desc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
rw₁ rw₂ : CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc e 0) = biprod.inr ≫ u
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inr (biprod.desc f (-g)) ≫ d = biprod.inr ≫ u

Tactic:
rw [Category.assoc, hd]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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 = 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 _ _
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
⊢ (-g) ≫ d = (-g) ≫ 0

Tactic:
simpa