awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ preadditiveHasZeroMorphisms = inst_3

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)

Tactic:
have h₁ := @biprod.add_eq_lift_id_desc _ _ a _ _ f g
      (by convert! (inferInstance : HasBinaryBiproduct X X); subsingleton)
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ HasBinaryBiproduct.{v, u} X X

Tactic:
(inferInstance : HasBinaryBiproduct X X)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
h : preadditiveHasZeroMorphisms = inst_3
⊢ HasBinaryBiproduct.{v, u} X X

Tactic:
convert! (inferInstance : HasBinaryBiproduct X X)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ preadditiveHasZeroMorphisms = inst_3

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)

Tactic:
have h₂ := @biprod.add_eq_lift_id_desc _ _ b _ _ f g
      (by convert! (inferInstance : HasBinaryBiproduct X X); subsingleton)
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
h₂ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ f + g = f + g

Tactic:
h₁.trans (Eq.trans ?_ h₂.symm)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
h₂ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
homGroup :
  CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ f + g = f + g

Tactic:
refine h₁.trans (Eq.trans ?_ h₂.symm)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
h₂ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
homGroup : Eq (α := HasZeroMorphisms.{v, u} C) preadditiveHasZeroMorphisms preadditiveHasZeroMorphisms
homGroup₁ homGroup₂ :
  biprod.{v, u} X X = biprod.{v, u} X X →
    Eq (α := HasZeroMorphisms.{v, u} C) preadditiveHasZeroMorphisms preadditiveHasZeroMorphisms
⊢ CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)

Tactic:
congr! 2
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
h₂ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ Eq (α := HasZeroMorphisms.{v, u} C) preadditiveHasZeroMorphisms preadditiveHasZeroMorphisms

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
h₂ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
e_4 : biprod.{v, u} X X = biprod.{v, u} X X
⊢ Eq (α := HasZeroMorphisms.{v, u} C) preadditiveHasZeroMorphisms preadditiveHasZeroMorphisms

Tactic:
subsingleton
-- 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
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
      (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) =
    HAdd.hAdd (α := X₁ ⟶ biprod.{v, u} Y₁ Y₂) (f₁₁ ≫ biprod.inl) (f₁₂ ≫ biprod.inr)

Tactic:
simp [Biprod.ofComponents]

Premises used: CategoryTheory.Biprod.ofComponents
-- 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
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
      (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) =
    HAdd.hAdd (α := X₂ ⟶ biprod.{v, u} Y₁ Y₂) (f₂₁ ≫ biprod.inl) (f₂₂ ≫ biprod.inr)

Tactic:
simp [Biprod.ofComponents]

Premises used: CategoryTheory.Biprod.ofComponents
-- 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
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ Y₁) (biprod.fst ≫ f₁₁) (biprod.snd ≫ f₂₁)

Tactic:
simp [Biprod.ofComponents]

Premises used: CategoryTheory.Biprod.ofComponents
-- 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
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
    HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ Y₂) (biprod.fst ≫ f₁₂) (biprod.snd ≫ f₂₂)

Tactic:
simp [Biprod.ofComponents]

Premises used: CategoryTheory.Biprod.ofComponents
-- 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
X₁ X₂ Y₁ Y₂ : C
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    (biprod.inl ≫ f) ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
    (biprod.inl ≫ f) ≫ biprod.snd
h₂ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₂ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    (biprod.inr ≫ f) ≫ biprod.fst
h₃ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₂ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
    (biprod.inr ≫ f) ≫ biprod.snd
⊢ ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f

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
X₁ X₂ Y₁ Y₂ : C
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    (biprod.inl ≫ f) ≫ biprod.fst

Tactic:
simp only [Category.comp_id, biprod.inr_fst, biprod.inr_snd, biprod.inl_snd, add_zero, zero_add,
      Biprod.inl_ofComponents, Biprod.inr_ofComponents, Category.assoc,
      comp_zero, biprod.inl_fst, Preadditive.add_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Biprod.inr_ofComponents, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inl_snd, zero_add, CategoryTheory.Preadditive.add_comp, add_zero, CategoryTheory.Biprod.inl_ofComponents, CategoryTheory.Limits.biprod.inr_snd
-- 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
X₁ X₂ Y₁ Y₂ : C
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
    (biprod.inl ≫ f) ≫ biprod.snd

Tactic:
simp only [Category.comp_id, biprod.inr_fst, biprod.inr_snd, biprod.inl_snd, add_zero, zero_add,
      Biprod.inl_ofComponents, Biprod.inr_ofComponents, Category.assoc,
      comp_zero, biprod.inl_fst, Preadditive.add_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Biprod.inr_ofComponents, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inl_snd, zero_add, CategoryTheory.Preadditive.add_comp, add_zero, CategoryTheory.Biprod.inl_ofComponents, CategoryTheory.Limits.biprod.inr_snd
-- 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
X₁ X₂ Y₁ Y₂ : C
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₂ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    (biprod.inr ≫ f) ≫ biprod.fst

Tactic:
simp only [Category.comp_id, biprod.inr_fst, biprod.inr_snd, biprod.inl_snd, add_zero, zero_add,
      Biprod.inl_ofComponents, Biprod.inr_ofComponents, Category.assoc,
      comp_zero, biprod.inl_fst, Preadditive.add_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Biprod.inr_ofComponents, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inl_snd, zero_add, CategoryTheory.Preadditive.add_comp, add_zero, CategoryTheory.Biprod.inl_ofComponents, CategoryTheory.Limits.biprod.inr_snd
-- 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
X₁ X₂ Y₁ Y₂ : C
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₂ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
    (biprod.inr ≫ f) ≫ biprod.snd

Tactic:
simp only [Category.comp_id, biprod.inr_fst, biprod.inr_snd, biprod.inl_snd, add_zero, zero_add,
      Biprod.inl_ofComponents, Biprod.inr_ofComponents, Category.assoc,
      comp_zero, biprod.inl_fst, Preadditive.add_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Biprod.inr_ofComponents, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.biprod.inl_snd, zero_add, CategoryTheory.Preadditive.add_comp, add_zero, CategoryTheory.Biprod.inl_ofComponents, CategoryTheory.Limits.biprod.inr_snd
-- 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
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
dsimp :
  (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) (biprod.fst ≫ f₁₁ ≫ biprod.inl)
            (biprod.fst ≫ f₁₂ ≫ biprod.inr) +
          biprod.snd ≫ f₂₁ ≫ biprod.inl +
        biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
      (HAdd.hAdd (α := biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ g₁₁ ≫ biprod.inl)
            (biprod.fst ≫ g₁₂ ≫ biprod.inr) +
          biprod.snd ≫ g₂₁ ≫ biprod.inl +
        biprod.snd ≫ g₂₂ ≫ biprod.inr) =
    HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl)
          (biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr) +
        biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
      biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr
⊢ Eq (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂)
    (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
        (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
        (ofComponents g₁₁ g₁₂ g₂₁ g₂₂ : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) :
      biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂)
    (ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) :
      biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂)

Tactic:
dsimp [Biprod.ofComponents]

Premises used: CategoryTheory.Biprod.ofComponents
-- 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
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.inl ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) (biprod.fst ≫ f₁₁ ≫ biprod.inl)
                (biprod.fst ≫ f₁₂ ≫ biprod.inr) +
              biprod.snd ≫ f₂₁ ≫ biprod.inl +
            biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
          (HAdd.hAdd (α := biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ g₁₁ ≫ biprod.inl)
                (biprod.fst ≫ g₁₂ ≫ biprod.inr) +
              biprod.snd ≫ g₂₁ ≫ biprod.inl +
            biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inl ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl)
              (biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr) +
            biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
          biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
      biprod.fst

Tactic:
simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inl_snd_assoc, CategoryTheory.Limits.biprod.inr_snd_assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Limits.biprod.inl_snd, zero_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Limits.biprod.inr_fst_assoc, CategoryTheory.Preadditive.comp_add, CategoryTheory.Limits.zero_comp, add_zero, CategoryTheory.Limits.biprod.inr_snd, CategoryTheory.Limits.biprod.inl_fst_assoc
-- 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
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.inl ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) (biprod.fst ≫ f₁₁ ≫ biprod.inl)
                (biprod.fst ≫ f₁₂ ≫ biprod.inr) +
              biprod.snd ≫ f₂₁ ≫ biprod.inl +
            biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
          (HAdd.hAdd (α := biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ g₁₁ ≫ biprod.inl)
                (biprod.fst ≫ g₁₂ ≫ biprod.inr) +
              biprod.snd ≫ g₂₁ ≫ biprod.inl +
            biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inl ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl)
              (biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr) +
            biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
          biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
      biprod.snd

Tactic:
simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inl_snd_assoc, CategoryTheory.Limits.biprod.inr_snd_assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Limits.biprod.inl_snd, zero_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Limits.biprod.inr_fst_assoc, CategoryTheory.Preadditive.comp_add, CategoryTheory.Limits.zero_comp, add_zero, CategoryTheory.Limits.biprod.inr_snd, CategoryTheory.Limits.biprod.inl_fst_assoc
-- 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
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.inr ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) (biprod.fst ≫ f₁₁ ≫ biprod.inl)
                (biprod.fst ≫ f₁₂ ≫ biprod.inr) +
              biprod.snd ≫ f₂₁ ≫ biprod.inl +
            biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
          (HAdd.hAdd (α := biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ g₁₁ ≫ biprod.inl)
                (biprod.fst ≫ g₁₂ ≫ biprod.inr) +
              biprod.snd ≫ g₂₁ ≫ biprod.inl +
            biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inr ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl)
              (biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr) +
            biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
          biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
      biprod.fst

Tactic:
simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inl_snd_assoc, CategoryTheory.Limits.biprod.inr_snd_assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Limits.biprod.inl_snd, zero_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Limits.biprod.inr_fst_assoc, CategoryTheory.Preadditive.comp_add, CategoryTheory.Limits.zero_comp, add_zero, CategoryTheory.Limits.biprod.inr_snd, CategoryTheory.Limits.biprod.inl_fst_assoc