awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) inr (desc f g) =
    inr ≫ HAdd.hAdd (α := biprod.{v, u} X Y ⟶ T) (fst ≫ f) (snd ≫ g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
T U : C
f : T ⟶ X
g : T ⟶ Y
h : X ⟶ U
i : Y ⟶ U
⊢ CategoryStruct.comp (Y := biprod.{v, u} X Y) (lift f g) (desc h i) = f ≫ h + g ≫ i

Tactic:
simp [biprod.lift_eq, biprod.desc_eq]

Premises used: CategoryTheory.Limits.biprod.lift_eq, CategoryTheory.Limits.biprod.desc_eq
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) fst =
    (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) snd =
    (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ snd
h₂ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inr (map f g)) fst =
    (inr ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst
h₃ :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inr (map f g)) snd =
    (inr ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ snd
⊢ map f g = HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) fst =
    (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inl (map f g)) snd =
    (inl ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inr (map f g)) fst =
    (inr ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) (CategoryStruct.comp (Y := biprod.{v, u} W X) inr (map f g)) snd =
    (inr ≫ HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (fst ≫ f ≫ inl) (snd ≫ g ≫ inr)) ≫ snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
Z : C
f : Z ⟶ biprod.{v, u} X Y
⊢ f = HAdd.hAdd (α := Z ⟶ biprod.{v, u} X Y) ((f ≫ fst) ≫ inl) ((f ≫ snd) ≫ inr)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
Z : C
f g : Z ⟶ biprod.{v, u} X Y
⊢ f = g ↔ f ≫ fst = g ≫ fst ∧ f ≫ snd = g ≫ snd

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
Z : C
f : biprod.{v, u} X Y ⟶ Z
⊢ f = HAdd.hAdd (α := biprod.{v, u} X Y ⟶ Z) (fst ≫ inl ≫ f) (snd ≫ inr ≫ f)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
inst_2 : HasBinaryBiproduct.{v, u} X Y
Z : C
f g : biprod.{v, u} X Y ⟶ Z
⊢ f = g ↔ inl ≫ f = inl ≫ g ∧ inr ≫ f = inr ≫ g

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (𝟙 Y - (𝟙 Y - retraction f ≫ f)) ≫ Cofork.π c = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
c' : CokernelCofork (𝟙 Y - (𝟙 Y - retraction f ≫ f)) := CokernelCofork.ofπ (Cofork.π c) ⋯
⊢ 𝟙 Y - (𝟙 Y - retraction f ≫ f) = retraction f ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
c' : CokernelCofork (𝟙 Y - (𝟙 Y - retraction f ≫ f)) := CokernelCofork.ofπ (Cofork.π c) ⋯
i' : IsColimit c' := isCokernelEpiComp i (retraction f) ⋯
i'' : IsColimit (coforkOfCokernelCofork c') := isColimitCoforkOfCokernelCofork i'
⊢ (𝟙 Y - retraction f ≫ f) ≫ (𝟙 Y - retraction f ≫ f) = 𝟙 Y - retraction f ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ f ≫ retraction f = 𝟙 X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ f ≫ Cofork.π c = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
dsimp :
  Eq (α := c.pt ⟶ X)
    (SplitEpi.section_ (f := Cofork.π (coforkOfCokernelCofork (CokernelCofork.ofπ (Cofork.π c) ⋯)))
          (splitEpiOfIdempotentOfIsColimitCofork C ⋯
              (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯)) :
            SplitEpi (Y :=
              Cocone.pt (F := parallelPair (𝟙 Y) (𝟙 Y - retraction f ≫ f))
                (coforkOfCokernelCofork (CokernelCofork.ofπ (Cofork.π c) ⋯)))
              (Cofork.π (coforkOfCokernelCofork (CokernelCofork.ofπ (Cofork.π c) ⋯)))) ≫
        retraction f :
      c.pt ⟶ X)
    (0 : c.pt ⟶ X)
⊢ Eq (α := c.pt ⟶ X)
    ((let c' : CokernelCofork (𝟙 Y - (𝟙 Y - retraction f ≫ f)) := CokernelCofork.ofπ (Cofork.π c) ⋯;
      let i' : IsColimit c' := isCokernelEpiComp i (retraction f) ⋯;
      let i'' := isColimitCoforkOfCokernelCofork i';
      (splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_) ≫
      retraction f)
    0

Tactic:
dsimp only
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
rw :
  Eq (α := c.pt ⟶ X)
    (i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯))) ⋯) ≫ retraction f) 0
⊢ Eq (α := c.pt ⟶ X)
    (SplitEpi.section_ (f := Cofork.π (coforkOfCokernelCofork (CokernelCofork.ofπ (Cofork.π c) ⋯)))
          (splitEpiOfIdempotentOfIsColimitCofork C ⋯
              (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯)) :
            SplitEpi (Y :=
              Cocone.pt (F := parallelPair (𝟙 Y) (𝟙 Y - retraction f ≫ f))
                (coforkOfCokernelCofork (CokernelCofork.ofπ (Cofork.π c) ⋯)))
              (Cofork.π (coforkOfCokernelCofork (CokernelCofork.ofπ (Cofork.π c) ⋯)))) ≫
        retraction f :
      c.pt ⟶ X)
    (0 : c.pt ⟶ X)

Tactic:
rw [splitEpiOfIdempotentOfIsColimitCofork_section_,
      isColimitCoforkOfCokernelCofork_desc, isCokernelEpiComp_desc]

Premises used: CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc, CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_, CategoryTheory.Limits.isCokernelEpiComp_desc
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
dsimp :
  Eq (α := c.pt ⟶ X) (i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ⋯) ≫ retraction f) 0
⊢ Eq (α := c.pt ⟶ X)
    (i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯))) ⋯) ≫ retraction f) 0

Tactic:
dsimp only [cokernelCoforkOfCofork_ofπ]

Premises used: CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := ⋯
apply :
  Eq (α := Y ⟶ X)
    (Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ⋯) ≫ retraction f) 0
⊢ Eq (α := c.pt ⟶ X) (i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ⋯) ≫ retraction f) 0

Tactic:
apply zero_of_epi_comp c.π

Premises used: CategoryTheory.Limits.zero_of_epi_comp, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := ⋯
simp : 𝟙 Y ≫ retraction f - retraction f = 0
⊢ Eq (α := Y ⟶ X)
    (Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (CokernelCofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯)) ⋯) ≫ retraction f) 0

Tactic:
simp only [sub_comp, comp_sub, Category.comp_id, Category.assoc, IsSplitMono.id, sub_self,
      Cofork.IsColimit.π_desc_assoc, CokernelCofork.π_ofπ, IsSplitMono.id_assoc]

Premises used: CategoryTheory.Category.assoc, sub_self, CategoryTheory.IsSplitMono.id_assoc, CategoryTheory.Limits.Cofork.IsColimit.π_desc_assoc, CategoryTheory.Category.comp_id, CategoryTheory.IsSplitMono.id, CategoryTheory.Limits.CokernelCofork.π_ofπ, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := ⋯
a : 𝟙 Y ≫ retraction f = retraction f
⊢ 𝟙 Y ≫ retraction f - retraction f = 0

Tactic:
apply sub_eq_zero_of_eq

Premises used: sub_eq_zero_of_eq
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := ⋯
⊢ 𝟙 Y ≫ retraction f = retraction f

Tactic:
apply Category.id_comp

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (let c' : CokernelCofork (𝟙 Y - (𝟙 Y - retraction f ≫ f)) := CokernelCofork.ofπ (Cofork.π c) ⋯;
      let i' : IsColimit c' := isCokernelEpiComp i (retraction f) ⋯;
      let i'' := isColimitCoforkOfCokernelCofork i';
      (splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_) ≫
      Cofork.π c =
    𝟙 c.pt

Tactic:
apply SplitEpi.id

Premises used: CategoryTheory.SplitEpi.id
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
simp :
  HAdd.hAdd (β := (binaryBiconeOfIsSplitMonoOfCokernel i).pt ⟶ (binaryBiconeOfIsSplitMonoOfCokernel i).pt)
      (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
      (Cofork.π c ≫
          IsColimit.desc (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯))
            (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) :
        (binaryBiconeOfIsSplitMonoOfCokernel i).pt ⟶ (binaryBiconeOfIsSplitMonoOfCokernel i).pt) =
    𝟙 (binaryBiconeOfIsSplitMonoOfCokernel i).pt
⊢ (binaryBiconeOfIsSplitMonoOfCokernel i).fst ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      (binaryBiconeOfIsSplitMonoOfCokernel i).snd ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inr =
    𝟙 (binaryBiconeOfIsSplitMonoOfCokernel i).pt

Tactic:
simp only [binaryBiconeOfIsSplitMonoOfCokernel_fst,
        binaryBiconeOfIsSplitMonoOfCokernel_inr,
        binaryBiconeOfIsSplitMonoOfCokernel_snd,
        splitEpiOfIdempotentOfIsColimitCofork_section_]

Premises used: CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inr, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd, CategoryTheory.Limits.splitEpiOfIdempotentOfIsColimitCofork_section_, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_fst
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
dsimp :
  HAdd.hAdd (β := Y ⟶ Y) (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
      (Cofork.π c ≫
          IsColimit.desc (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯))
            (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) :
        Y ⟶ Y) =
    𝟙 Y
⊢ HAdd.hAdd (β := (binaryBiconeOfIsSplitMonoOfCokernel i).pt ⟶ (binaryBiconeOfIsSplitMonoOfCokernel i).pt)
      (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
      (Cofork.π c ≫
          IsColimit.desc (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯))
            (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) :
        (binaryBiconeOfIsSplitMonoOfCokernel i).pt ⟶ (binaryBiconeOfIsSplitMonoOfCokernel i).pt) =
    𝟙 (binaryBiconeOfIsSplitMonoOfCokernel i).pt

Tactic:
dsimp only [binaryBiconeOfIsSplitMonoOfCokernel_pt]

Premises used: CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
rw :
  HAdd.hAdd (β := Y ⟶ Y) (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
      (Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯))) ⋯) :
        Y ⟶ Y) =
    𝟙 Y
⊢ HAdd.hAdd (β := Y ⟶ Y) (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
      (Cofork.π c ≫
          IsColimit.desc (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯))
            (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) :
        Y ⟶ Y) =
    𝟙 Y

Tactic:
rw [isColimitCoforkOfCokernelCofork_desc, isCokernelEpiComp_desc]

Premises used: CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork_desc, CategoryTheory.Limits.isCokernelEpiComp_desc
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
f : X ⟶ Y
inst_3 : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ HAdd.hAdd (β := Y ⟶ Y) (retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl)
      (Cofork.π c ≫ i.desc (Cofork.ofπ (Cofork.π (cokernelCoforkOfCofork (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯))) ⋯) :
        Y ⟶ Y) =
    𝟙 Y

Tactic:
simp only [binaryBiconeOfIsSplitMonoOfCokernel_inl, Cofork.IsColimit.π_desc,
        cokernelCoforkOfCofork_π, Cofork.π_ofπ, add_sub_cancel]

Premises used: CategoryTheory.Preadditive.cokernelCoforkOfCofork_π, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inl, add_sub_cancel, CategoryTheory.Limits.Cofork.IsColimit.π_desc, CategoryTheory.Limits.Cofork.π_ofπ
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g ≫ BinaryFan.fst b.toCone = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g ≫ BinaryFan.snd b.toCone = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
⊢ (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0

Tactic:
simpa using sub_eq_zero.2 h₁

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
⊢ (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0

Tactic:
have h₁' : ((m : T ⟶ b.pt) - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0 := by
        simpa using sub_eq_zero.2 h₁
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
⊢ (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0

Tactic:
simpa using sub_eq_zero.2 h₂

Premises used: Iff.mpr, sub_eq_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
⊢ (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0

Tactic:
have h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0 := by simpa using sub_eq_zero.2 h₂
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
obtain :
  ∀ (q : T ⟶ X) (hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)),
    m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g

Tactic:
obtain ⟨q : T ⟶ X, hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)⟩ :=
        KernelFork.IsLimit.lift' hb _ h₂'

Premises used: CategoryTheory.Limits.BinaryBicone.inl, CategoryTheory.Limits.KernelFork.IsLimit.lift', CategoryTheory.Limits.BinaryBicone.inr, HAdd.hAdd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
rw : m - (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g = 0
rw₁ : q ≫ b.inl = 0
rw₂ : (q ≫ 𝟙 X) ≫ b.inl = 0
rw₃ : (q ≫ b.inl ≫ b.fst) ≫ b.inl = 0
rw₄ : ((q ≫ b.inl) ≫ b.fst) ≫ b.inl = 0
rw₅ : ((m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst) ≫ b.inl = 0
rw₆ : Eq (α := T ⟶ b.toCone.pt) (0 ≫ b.inl) 0
rw₇ rw₈ : Eq.{v + 1} (α := T ⟶ b.toCone.pt) 0 0
⊢ m = (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g

Tactic:
rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryBicone.inl_fst, sub_eq_zero, CategoryTheory.Category.comp_id, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g ≫ BinaryFan.fst b.toCone = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
⊢ (fun {T : C} (f : T ⟶ X) (g : T ⟶ Y) ↦ f ≫ b.inl + g ≫ b.inr) f g ≫ BinaryFan.snd b.toCone = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X_1 Y_1 : C
inst_2 : HasBinaryBiproduct.{v, u} X_1 Y_1
X Y : C
b : BinaryBicone.{v, u} X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
⊢ (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0

Tactic:
simpa using sub_eq_zero.2 h₁

Premises used: Iff.mpr, sub_eq_zero