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 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
⊢ d = 0

Tactic:
have : d = 0 := (cancel_epi (-g)).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 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
rw rw₁ : e = e
⊢ e = CategoryStruct.comp (Y := biprod.{v, u} X Y) biprod.inl (biprod.desc e 0)

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 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
rw 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)
⊢ 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:
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 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
rw 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))
⊢ 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:
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 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
rw 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)
⊢ 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]

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_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) 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 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₄ :
  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)
⊢ 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 _ _

Premises used: CategoryTheory.Limits.biprod.desc, CategoryTheory.Limits.biprod.inl, CategoryTheory.CategoryStruct.comp, 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi f
s : PullbackCone f g
hs : IsLimit s
⊢ 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
-- 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi f
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.right)
⊢ Epi s.snd

Tactic:
apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.limit.isLimit, CategoryTheory.epi_of_epi_fac
-- 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
s : PullbackCone f g
hs : IsLimit s
⊢ 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
-- 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : Epi g
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.left)
⊢ Epi s.fst

Tactic:
apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.limit.isLimit, CategoryTheory.epi_of_epi_fac
-- 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
g₁ : Y ⟶ W
inst_3 : Epi g₁
g₂ : W ⟶ Z
inst_4 : Mono g₂
hg : g₁ ≫ g₂ = g
f' : X ⟶ W
hf : f' ≫ g₂ = f
t : PullbackCone f g
ht : IsLimit t
⊢ Epi t.fst

Tactic:
apply epi_fst_of_isLimit _ _ (PullbackCone.isLimitOfFactors f g g₂ f' g₁ hf hg t ht)

Premises used: CategoryTheory.Limits.PullbackCone.isLimitOfFactors, CategoryTheory.Abelian.epi_fst_of_isLimit
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
⊢ Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)

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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
⊢ Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)

Tactic:
have hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
have :
  ∀
    (this :
      IsLimit (F :=
        parallelPair (X := biprod.{v, u} Y Z) (Y :=
          Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
            (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
          (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
        (KernelFork.ofι (biprod.lift f (-g)) ⋯)),
    e = 0
⊢ e = 0

Tactic:
have :=
      monoIsKernelOfCokernel _
        (BiproductToPushoutIsCokernel.isColimitBiproductToPushout f g)
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
obtain :
  ∀
    (d :
      R ⟶
        Cone.pt (F :=
          parallelPair (X := biprod.{v, u} Y Z) (Y :=
            Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
              (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
            (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
          (KernelFork.ofι (biprod.lift f (-g)) ⋯))
    (hd : d ≫ Fork.ι (KernelFork.ofι (biprod.lift f (-g)) ⋯) = u), e = 0
⊢ e = 0

Tactic:
obtain ⟨d, hd⟩ := KernelFork.IsLimit.lift' this u hu

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.lift'
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
rw rw₁ : d ≫ f = d ≫ f
⊢ d ≫ f = d ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst

Tactic:
rw [biprod.lift_fst]

Premises used: CategoryTheory.Limits.biprod.lift_fst
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
rw : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.fst = u ≫ biprod.fst
rw₁ rw₂ : CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.fst = u ≫ biprod.fst
⊢ d ≫ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) biprod.fst = u ≫ biprod.fst

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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
⊢ d ≫ f = 0

Tactic:
have : d ≫ f = 0 := calc
      d ≫ f = d ≫ biprod.lift f (-g) ≫ biprod.fst := by rw [biprod.lift_fst]
      _ = u ≫ biprod.fst := by rw [← Category.assoc, hd]
      _ = 0 := biprod.lift_fst _ _
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this : d ≫ f = 0
⊢ d ≫ f = 0 ≫ f

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this : d ≫ f = 0
⊢ d = 0

Tactic:
have : d = 0 := (cancel_mono 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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
rw rw₁ : e = e
⊢ e = CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd

Tactic:
rw [biprod.lift_snd]

Premises used: CategoryTheory.Limits.biprod.lift_snd
-- Module: Mathlib.CategoryTheory.Abelian.Basic
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
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
rw rw₁ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift 0 e) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd

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 : HasPushouts.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_3 : Mono f
R : C
e : R ⟶ Z
h : Eq (α := R ⟶ pushout f g) (e ≫ pushout.inr f g) 0
u : R ⟶ biprod.{v, u} Y Z := biprod.lift 0 e
hu :
  Eq (α := R ⟶ pushout f g) (u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g : R ⟶ pushout f g)
    (0 : R ⟶ pushout f g)
this_1 :
  IsLimit (F :=
    parallelPair (X := biprod.{v, u} Y Z) (Y :=
      Cocone.pt (F := parallelPair (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0)
        (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g))
      (Cofork.π (BiproductToPushoutIsCokernel.biproductToPushoutCofork f g)) 0)
    (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : Eq (α := R ⟶ biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) (biprod.lift 0 e)
this_2 : d ≫ f = 0
this : d = 0
rw rw₁ :
  Eq (α := R ⟶ Z) (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd)
    (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd)
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (d ≫ biprod.lift f (-g)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) (0 ≫ biprod.lift f (-g)) biprod.snd

Tactic:
rw [this]