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
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
e : parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F ≅ parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (F :=
  parallelPair (X := Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
    (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
  (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
change : F.map p ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ F.map p
⊢ Cofork.π (CokernelCofork.ofπ (F.map p) ⋯) ≫
      Iso.hom
        (Iso.refl
          (Cocone.pt (F :=
            parallelPair (X :=
              Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
              (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
            (CokernelCofork.ofπ (F.map p) ⋯))) =
    Cofork.π ((Cocone.precompose e.inv).obj (F.mapCocone (CokernelCofork.ofπ p ⋯)))

Tactic:
change F.map p ≫ 𝟙 _ = 𝟙 _ ≫ F.map p

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
D : Type u_1
inst_2 : Category.{v_1, u_1} D
inst_3 : HasZeroMorphisms.{v_1, u_1} D
X Y : D
p : X ⟶ Y
inst_4 : HasKernel p
F : Functor.{v_1, v, u_1, u} D C
inst_5 : F.PreservesZeroMorphisms
inst_6 : Epi (F.map p)
inst_7 : PreservesLimit (parallelPair p 0) F
e : parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F ≅ parallelPair (X := kernel (F.map p)) (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (F :=
  parallelPair (X := Cone.pt (F := parallelPair (F.map p) 0) (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯))
    (Fork.ι (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯)) 0)
  (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (P := kernel (F.map p)) (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
rw : F.map p = 𝟙 (F.obj X) ≫ F.map p
rw₁ rw₂ : F.map p = F.map p
⊢ F.map p ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ F.map p

Tactic:
rw [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasEqualizers.{v, u} C

Tactic:
Preadditive.hasEqualizers_of_hasKernels

Premises used: CategoryTheory.Preadditive.hasEqualizers_of_hasKernels
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasPullbacks.{v, u} C

Tactic:
hasPullbacks_of_hasBinaryProducts_of_hasEqualizers C

Premises used: CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasCoequalizers.{v, u} C

Tactic:
Preadditive.hasCoequalizers_of_hasCokernels

Premises used: CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasPushouts.{v, u} C

Tactic:
hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers C

Premises used: CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasFiniteLimits.{v, u} C

Tactic:
Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products

Premises used: CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products
-- Module: Mathlib.CategoryTheory.Abelian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ HasFiniteColimits.{v, u} C

Tactic:
Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts

Premises used: CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts
-- 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
rw : HAdd.hAdd (α := pullback f g ⟶ Z) (pullback.fst f g ≫ f) (pullback.snd f g ≫ (-g)) = 0
rw₁ : HAdd.hAdd (α := pullback f g ⟶ Z) (pullback.fst f g ≫ f) (-pullback.snd f g ≫ g) = 0
rw₂ : HAdd.hAdd (α := pullback f g ⟶ Z) (pullback.snd f g ≫ g) (-pullback.snd f g ≫ g) = 0
rw₃ rw₄ : Eq.{v + 1} (α := pullback f g ⟶ Z) 0 0
⊢ Eq (α := pullback f g ⟶ Z)
    (CategoryStruct.comp (Y := biprod.{v, u} X Y) (pullbackToBiproduct f g) (biprod.desc f (-g)) : pullback f g ⟶ Z)
    (0 : pullback f g ⟶ Z)

Tactic:
rw [biprod.lift_desc, comp_neg, pullback.condition, add_neg_cancel]

Premises used: add_neg_cancel, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Limits.pullback.condition, CategoryTheory.Limits.biprod.lift_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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
rw : s.ι ≫ biprod.fst ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0
rw₁ : s.ι ≫ biprod.fst ≫ f - s.ι ≫ biprod.snd ≫ g = 0
rw₂ : s.ι ≫ HSub.hSub (α := biprod.{v, u} X Y ⟶ Z) (biprod.fst ≫ f) (biprod.snd ≫ g) = 0
rw₃ : s.ι ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ Z) (biprod.fst ≫ f) (-biprod.snd ≫ g) = 0
rw₄ : s.ι ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ Z) (biprod.fst ≫ f) (biprod.snd ≫ (-g)) = 0
rw₅ : s.ι ≫ biprod.desc f (-g) = 0
rw₆ rw₇ : Eq.{v + 1} (α := s.pt ⟶ Z) 0 0
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0

Tactic:
rw [Category.assoc, Category.assoc, ← comp_sub, sub_eq_add_neg, ← comp_neg, ←
            biprod.desc_eq, KernelFork.condition s]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.comp_neg, sub_eq_add_neg, CategoryTheory.Limits.biprod.desc_eq, CategoryTheory.Limits.KernelFork.condition, CategoryTheory.Preadditive.comp_sub
-- 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
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
        ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
            (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
          s)
        (Fork.ι (pullbackToBiproductFork f g)))
      biprod.fst =
    s.ι ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} X Y)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
        ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
            (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
          s)
        (Fork.ι (pullbackToBiproductFork f g)))
      biprod.snd =
    s.ι ≫ biprod.snd
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
          (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
        s)
      (Fork.ι (pullbackToBiproductFork f g)) =
    s.ι

Tactic:
apply biprod.hom_ext

Premises used: CategoryTheory.Limits.biprod.hom_ext
-- 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
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
h₀ :
  CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
            (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
          s :
        s.pt ⟶ pullback f g)
      (CategoryStruct.comp (Y := biprod.{v, u} X Y) (pullbackToBiproduct f g) biprod.fst :
        Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g) ⟶ X) =
    s.ι ≫ biprod.fst
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
        ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
            (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
          s)
        (Fork.ι (pullbackToBiproductFork f g)))
      biprod.fst =
    s.ι ≫ biprod.fst

Tactic:
rw [Fork.ι_ofι, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Fork.ι_ofι
-- 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
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
h₁ :
  CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
            (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
          s :
        s.pt ⟶ pullback f g)
      (CategoryStruct.comp (Y := biprod.{v, u} X Y) (pullbackToBiproduct f g) biprod.snd :
        Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g) ⟶ Y) =
    s.ι ≫ biprod.snd
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
        ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
            (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
          s)
        (Fork.ι (pullbackToBiproductFork f g)))
      biprod.snd =
    s.ι ≫ biprod.snd

Tactic:
rw [Fork.ι_ofι, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Fork.ι_ofι
-- 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
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
h₀ :
  CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
          (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
        s)
      (pullback.fst f g) =
    s.ι ≫ biprod.fst
h₁ h₂ : s.ι ≫ biprod.fst = s.ι ≫ biprod.fst
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
            (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
          s :
        s.pt ⟶ pullback f g)
      (CategoryStruct.comp (Y := biprod.{v, u} X Y) (pullbackToBiproduct f g) biprod.fst :
        Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g) ⟶ X) =
    s.ι ≫ biprod.fst

Tactic:
rw [biprod.lift_fst, pullback.lift_fst]

Premises used: CategoryTheory.Limits.biprod.lift_fst, CategoryTheory.Limits.pullback.lift_fst
-- 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
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
h₁ :
  CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
          (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
        s)
      (pullback.snd f g) =
    s.ι ≫ biprod.snd
h₂ h₃ : s.ι ≫ biprod.snd = s.ι ≫ biprod.snd
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g))
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
            (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
          s :
        s.pt ⟶ pullback f g)
      (CategoryStruct.comp (Y := biprod.{v, u} X Y) (pullbackToBiproduct f g) biprod.snd :
        Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g) ⟶ Y) =
    s.ι ≫ biprod.snd

Tactic:
rw [biprod.lift_snd, pullback.lift_snd]

Premises used: CategoryTheory.Limits.biprod.lift_snd, CategoryTheory.Limits.pullback.lift_snd
-- 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
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g)
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
h₀ :
  m ≫ pullback.fst f g =
    CategoryStruct.comp (Y := pullback f g)
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
          (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
        s)
      (pullback.fst f g)
h₁ :
  m ≫ pullback.snd f g =
    CategoryStruct.comp (Y := pullback f g)
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
          (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
        s)
      (pullback.snd f g)
⊢ m =
    (fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
        (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
      s

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- 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
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g)
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
⊢ m ≫ pullback.fst f g =
    CategoryStruct.comp (Y := pullback f g)
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
          (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
        s)
      (pullback.fst f g)

Tactic:
simp [← h]
-- 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
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) (pullbackToBiproductFork f g)
h : m ≫ Fork.ι (pullbackToBiproductFork f g) = s.ι
⊢ m ≫ pullback.snd f g =
    CategoryStruct.comp (Y := pullback f g)
      ((fun (s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0) ↦
          (pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ : s.pt ⟶ pullback f g))
        s)
      (pullback.snd f g)

Tactic:
simp [← h]
-- 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
rw : HAdd.hAdd (α := X ⟶ pushout f g) (f ≫ pushout.inl f g) ((-g) ≫ pushout.inr f g) = 0
rw₁ : HAdd.hAdd (α := X ⟶ pushout f g) (f ≫ pushout.inl f g) (-g ≫ pushout.inr f g) = 0
rw₂ : HAdd.hAdd (α := X ⟶ pushout f g) (g ≫ pushout.inr f g) (-g ≫ pushout.inr f g) = 0
rw₃ rw₄ : Eq.{v + 1} (α := X ⟶ pushout f g) 0 0
⊢ Eq (α := X ⟶ pushout f g)
    (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) (biproductToPushout f g) : X ⟶ pushout f g)
    (0 : X ⟶ pushout f g)

Tactic:
rw [biprod.lift_desc, neg_comp, pushout.condition, add_neg_cancel]

Premises used: add_neg_cancel, CategoryTheory.Limits.pushout.condition, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Limits.biprod.lift_desc
-- 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
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
rw₇ rw₈ : Eq.{v + 1} (α := X ⟶ s.pt) 0 0
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0

Tactic:
rw [← Category.assoc, ← Category.assoc, ← sub_comp, sub_eq_add_neg, ← neg_comp, ←
            biprod.lift_eq, Cofork.condition s, zero_comp]

Premises used: CategoryTheory.Limits.biprod.lift_eq, CategoryTheory.Category.assoc, sub_eq_add_neg, CategoryTheory.Limits.Cofork.condition, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Limits.zero_comp, CategoryTheory.Preadditive.sub_comp
-- 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
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.π
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.π) ⋯ : pushout f g ⟶ s.pt))
          s)) =
    biprod.inr ≫ 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.π

Tactic:
apply biprod.hom_ext'

Premises used: CategoryTheory.Limits.biprod.hom_ext'
-- 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
s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0
⊢ 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.π

Tactic:
simp
-- 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
s : Cofork (Y := biprod.{v, u} Y Z) (biprod.lift f (-g)) 0
⊢ 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.π) ⋯ : pushout f g ⟶ s.pt))
          s)) =
    biprod.inr ≫ s.π

Tactic:
simp
-- 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
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)
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.π) ⋯ : 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

Tactic:
apply pushout.hom_ext

Premises used: CategoryTheory.Limits.pushout.hom_ext
-- 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
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.π
⊢ 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)

Tactic:
simp [← h]
-- 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
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.π
⊢ 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.π) ⋯ : pushout f g ⟶ s.pt))
        s)

Tactic:
simp [← h]