awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasPullbacks.{v, u} C
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
⊢ 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)
have rw₃ : Eq.{v + 1} (α := pullback f g ⟶ Z) 0 0
Tactic: rw [biprod.lift_desc, comp_neg, pullback.condition, add_neg_cancel]
-- 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0
have rw : 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]
-- 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
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
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0
have rw₁ : 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]
-- 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
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
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0
have rw₂ : s.ι ≫ HSub.hSub (α := biprod.{v, u} X Y ⟶ Z) (biprod.fst ≫ f) (biprod.snd ≫ g) = 0
Tactic: rw [Category.assoc, Category.assoc, ← comp_sub, sub_eq_add_neg, ← comp_neg, ←
            biprod.desc_eq, KernelFork.condition s]
-- 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
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
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0
have rw₃ : s.ι ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ Z) (biprod.fst ≫ f) (-biprod.snd ≫ g) = 0
Tactic: rw [Category.assoc, Category.assoc, ← comp_sub, sub_eq_add_neg, ← comp_neg, ←
            biprod.desc_eq, KernelFork.condition s]
-- 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
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
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0
have rw₄ : s.ι ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ Z) (biprod.fst ≫ f) (biprod.snd ≫ (-g)) = 0
Tactic: rw [Category.assoc, Category.assoc, ← comp_sub, sub_eq_add_neg, ← comp_neg, ←
            biprod.desc_eq, KernelFork.condition s]
-- 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
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
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0
have rw₅ : s.ι ≫ biprod.desc f (-g) = 0
Tactic: rw [Category.assoc, Category.assoc, ← comp_sub, sub_eq_add_neg, ← comp_neg, ←
            biprod.desc_eq, KernelFork.condition s]
-- 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
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
⊢ (s.ι ≫ biprod.fst) ≫ f - (s.ι ≫ biprod.snd) ≫ g = 0
have rw₆ : Eq.{v + 1} (α := s.pt ⟶ Z) 0 0
Tactic: rw [Category.assoc, Category.assoc, ← comp_sub, sub_eq_add_neg, ← comp_neg, ←
            biprod.desc_eq, KernelFork.condition s]
-- 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
⊢ 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.ι
have 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) sorry : s.pt ⟶ pullback f g))
        s)
      (Fork.ι (pullbackToBiproductFork f g)))
    biprod.fst =
  s.ι ≫ biprod.fst
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 : 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
⊢ 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.ι
have 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) sorry : s.pt ⟶ pullback f g))
        s)
      (Fork.ι (pullbackToBiproductFork f g)))
    biprod.snd =
  s.ι ≫ biprod.snd
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 : 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
⊢ 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
have 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) sorry : 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 [Fork.ι_ofι, 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
⊢ 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
have 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) sorry : 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 [Fork.ι_ofι, 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
⊢ 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
have 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) sorry : s.pt ⟶ pullback f g))
      s)
    (pullback.fst f g) =
  s.ι ≫ biprod.fst
Tactic: rw [biprod.lift_fst, pullback.lift_fst]
-- 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
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
⊢ 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
have h₁ : s.ι ≫ biprod.fst = s.ι ≫ biprod.fst
Tactic: rw [biprod.lift_fst, pullback.lift_fst]
-- 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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (X := biprod.{v, u} X Y) (biprod.desc f (-g)) 0
⊢ 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
have 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) sorry : s.pt ⟶ pullback f g))
      s)
    (pullback.snd f g) =
  s.ι ≫ biprod.snd
Tactic: rw [biprod.lift_snd, pullback.lift_snd]
-- 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
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
⊢ 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
have h₂ : s.ι ≫ biprod.snd = s.ι ≫ biprod.snd
Tactic: rw [biprod.lift_snd, pullback.lift_snd]
-- 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
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 =
    (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
have 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) sorry : s.pt ⟶ pullback f g))
      s)
    (pullback.fst f g)
Tactic: apply pullback.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 : 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)
⊢ 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
have 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) sorry : s.pt ⟶ pullback f g))
      s)
    (pullback.snd f g)
Tactic: apply pullback.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
⊢ 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)
have rw : HAdd.hAdd (α := X ⟶ pushout f g) (f ≫ pushout.inl f g) ((-g) ≫ pushout.inr f g) = 0
Tactic: rw [biprod.lift_desc, neg_comp, pushout.condition, add_neg_cancel]
-- 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
rw : HAdd.hAdd (α := X ⟶ pushout f g) (f ≫ pushout.inl f g) ((-g) ≫ pushout.inr f g) = 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)
have rw₁ : HAdd.hAdd (α := X ⟶ pushout f g) (f ≫ pushout.inl f g) (-g ≫ pushout.inr f g) = 0
Tactic: rw [biprod.lift_desc, neg_comp, pushout.condition, add_neg_cancel]
-- 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
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
⊢ 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)
have rw₂ : HAdd.hAdd (α := X ⟶ pushout f g) (g ≫ pushout.inr f g) (-g ≫ pushout.inr f g) = 0
Tactic: rw [biprod.lift_desc, neg_comp, pushout.condition, add_neg_cancel]
-- 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
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
⊢ 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)
have rw₃ : Eq.{v + 1} (α := X ⟶ pushout f g) 0 0
Tactic: rw [biprod.lift_desc, neg_comp, pushout.condition, add_neg_cancel]
-- 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
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
have rw : (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]
-- 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
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
have rw₁ : (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]
-- 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
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
have rw₂ : HSub.hSub (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) (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]
-- 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
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
have rw₃ : HAdd.hAdd (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) (-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]
-- 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
⊢ f ≫ biprod.inl ≫ s.π - g ≫ biprod.inr ≫ s.π = 0
have rw₄ : HAdd.hAdd (α := X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.inl) ((-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]