awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
inst_4 : HasFiniteBiproducts.{uC', uC} C
inst_5 : Finite J
rcases : ∀ (n : ℕ) (e : J ≃ Fin n), HasBiproductsOfShape.{w, uC', uC} J C
⊢ HasBiproductsOfShape.{w, uC', uC} J C

Tactic:
rcases Finite.exists_equiv_fin J with ⟨n, ⟨e⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
inst_4 : HasFiniteBiproducts.{uC', uC} C
inst_5 : Finite J
n : ℕ
e : J ≃ Fin n
⊢ HasBiproductsOfShape.{0, uC', uC} (Fin n) C

Tactic:
haveI : HasBiproductsOfShape (Fin n) C := HasFiniteBiproducts.out n
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
inst_4 : HasFiniteBiproducts.{uC', uC} C
inst_5 : Finite J
n : ℕ
e : J ≃ Fin n
this : HasBiproductsOfShape.{0, uC', uC} (Fin n) C
⊢ HasBiproductsOfShape.{w, uC', uC} J C

Tactic:
hasBiproductsOfShape_of_equiv C e

Premises used: CategoryTheory.Limits.hasBiproductsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J → C
inst_4 : HasFiniteBiproducts.{uC', uC} C
inst_5 : Finite J
n : ℕ
e : J ≃ Fin n
this : HasBiproductsOfShape.{0, uC', uC} (Fin n) C
⊢ HasBiproductsOfShape.{w, uC', uC} J C

Tactic:
exact hasBiproductsOfShape_of_equiv C e

Premises used: CategoryTheory.Limits.hasBiproductsOfShape_of_equiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : J
⊢ Eq.{v + 1} (α := Bicone.pt.{w, v, u} (bicone f) ⟶ f b) (Bicone.π (bicone f) b) (π f b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
b : J
⊢ Eq.{v + 1} (α := f b ⟶ Bicone.pt.{w, v, u} (bicone f)) (Bicone.ι (bicone f) b) (ι f b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : DecidableEq J
f : J → C
inst_3 : HasBiproduct.{w, v, u} f
j j' : J
⊢ Eq.{v + 1} (α := f j ⟶ f j')
    (CategoryStruct.comp (Y := Bicone.pt.{w, v, u} (bicone f)) (Bicone.ι (bicone f) j) (Bicone.π (bicone f) j'))
    (if h : j = j' then eqToHom ⋯ else 0)

Tactic:
(biproduct.bicone f).ι_π j j'

Premises used: CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : DecidableEq J
f : J → C
inst_3 : HasBiproduct.{w, v, u} f
j j' : J
⊢ Eq.{v + 1} (α := f j ⟶ f j') (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j'))
    (if h : j = j' then eqToHom ⋯ else 0)

Tactic:
convert! (biproduct.bicone f).ι_π j j'

Premises used: CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
j : J
⊢ Eq.{v + 1} (α := f j ⟶ f j) (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j)) (𝟙 (f j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
j j' : J
h : j ≠ j'
⊢ Eq.{v + 1} (α := f j ⟶ f j') (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (π f j')) 0

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
inst_6 : HasBiproduct.{w, v, u} f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
j j' : J
w : j = j'
refl : Eq.{v + 1} (α := f j ⟶ biproduct.{w, v, u} f) (eqToHom ⋯ ≫ ι f j) (ι f j)
⊢ Eq.{v + 1} (α := f j ⟶ biproduct.{w, v, u} f) (eqToHom ⋯ ≫ ι f j') (ι f j)

Tactic:
cases w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
j : J
⊢ Eq.{v + 1} (α := f j ⟶ biproduct.{w, v, u} f) (eqToHom ⋯ ≫ ι f j) (ι f j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
j j' : J
w : j = j'
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f j') (π f j ≫ eqToHom ⋯) (π f j')

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
P : C
p : (b : J) → P ⟶ f b
j : J
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift p) (π f j) = p j

Tactic:
(biproduct.isLimit f).fac _ ⟨j⟩

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.biproduct.isLimit, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
P : C
p : (b : J) → f b ⟶ P
j : J
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc p) = p j

Tactic:
(biproduct.isColimit f).fac _ ⟨j⟩

Premises used: CategoryTheory.Limits.biproduct.isColimit, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
Z : C
g h : Z ⟶ biproduct.{w, v, u} f
w : ∀ (j : J), g ≫ π f j = h ≫ π f j
⊢ g = h

Tactic:
(biproduct.isLimit f).hom_ext fun j => w j.as

Premises used: CategoryTheory.Discrete.as, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.biproduct.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
Z : C
g h : biproduct.{w, v, u} f ⟶ Z
w : ∀ (j : J), ι f j ≫ g = ι f j ≫ h
⊢ g = h

Tactic:
(biproduct.isColimit f).hom_ext fun j => w j.as

Premises used: CategoryTheory.Limits.biproduct.isColimit, CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
j : Discrete J
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ obj.{w, v, w, u} (Discrete.functor f) j)
    (Iso.hom (isoProduct f) ≫ limit.π (Discrete.functor f) j)
    (CategoryStruct.comp (Y := limit.{w, w, v, u} (Discrete.functor f)) (Pi.lift (π f))
      (limit.π (Discrete.functor f) j))

Tactic:
simp [biproduct.isoProduct]

Premises used: CategoryTheory.Limits.biproduct.isoProduct
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
j : J
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.inv (isoProduct f)) (π f j) : piObj.{w, v, u} f ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift (Pi.π f)) (π f j) : piObj.{w, v, u} f ⟶ f j)

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
j : Discrete J
⊢ Eq.{v + 1} (α := obj.{w, v, w, u} (Discrete.functor f) j ⟶ biproduct.{w, v, u} f)
    (colimit.ι (Discrete.functor f) j ≫ Iso.inv (isoCoproduct f))
    (CategoryStruct.comp (Y := colimit.{w, w, v, u} (Discrete.functor f)) (colimit.ι (Discrete.functor f) j)
      (Sigma.desc (ι f)))

Tactic:
simp [biproduct.isoCoproduct]

Premises used: CategoryTheory.Limits.biproduct.isoCoproduct
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
j : J
⊢ Eq.{v + 1} (α := f j ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (Iso.hom (isoCoproduct f)) : f j ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc (Sigma.ι f)) : f j ⟶ sigmaObj.{w, v, u} f)

Tactic:
simp [← Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
inst_6 : HasBiproductsOfShape.{w, v, u} J C
X Y : Functor.{w, v, w, u} (Discrete J) C
η : X ⟶ Y
x : Discrete J
i : J
x_1 : Discrete J
j : J
h : i = j
⊢ Eq (α := X.obj { as := i : Discrete J } ⟶ Y.obj { as := j })
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := colimit X) (colimit.ι X { as := i })
        (Functor.map colim η ≫
          Iso.hom
            ((fun (F : Functor.{w, v, w, u} (Discrete J) C) ↦
                (Iso.trans (Y := sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                    (Iso.symm (Sigma.isoColimit F) : colimit F ≅ sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                    (Iso.trans (Y := biproduct.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                        (Iso.symm (biproduct.isoCoproduct fun (j : J) ↦ F.obj { as := j }))
                        ((biproduct.isoProduct fun (j : J) ↦ F.obj { as := j : Discrete J }) ≪≫ Pi.isoLimit F) :
                      (sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j }) ≅ obj lim F) :
                  obj colim F ≅ obj lim F))
              Y)))
      (limit.π Y { as := j }))
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := colimit X) (colimit.ι X { as := i })
          (Iso.hom
              ((fun (F : Functor.{w, v, w, u} (Discrete J) C) ↦
                  (Iso.trans (Y := sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                      (Iso.symm (Sigma.isoColimit F) : colimit F ≅ sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                      (Iso.trans (Y := biproduct.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                          (Iso.symm (biproduct.isoCoproduct fun (j : J) ↦ F.obj { as := j }))
                          ((biproduct.isoProduct fun (j : J) ↦ F.obj { as := j : Discrete J }) ≪≫ Pi.isoLimit F) :
                        (sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j }) ≅ obj lim F) :
                    obj colim F ≅ obj lim F))
                X) ≫
            Functor.map lim η) :
        X.obj { as := i : Discrete J } ⟶ obj lim Y)
      (limit.π Y { as := j }))

Tactic:
simp_all [Sigma.isoColimit, Pi.isoLimit, biproduct.ι_π, biproduct.ι_π_assoc]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.Limits.Sigma.isoColimit, CategoryTheory.Limits.Pi.isoLimit, CategoryTheory.Limits.biproduct.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
inst_6 : HasBiproductsOfShape.{w, v, u} J C
X Y : Functor.{w, v, w, u} (Discrete J) C
η : X ⟶ Y
x : Discrete J
i : J
x_1 : Discrete J
j : J
h : ¬i = j
⊢ Eq (α := X.obj { as := i : Discrete J } ⟶ Y.obj { as := j })
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := colimit X) (colimit.ι X { as := i })
        (Functor.map colim η ≫
          Iso.hom
            ((fun (F : Functor.{w, v, w, u} (Discrete J) C) ↦
                (Iso.trans (Y := sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                    (Iso.symm (Sigma.isoColimit F) : colimit F ≅ sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                    (Iso.trans (Y := biproduct.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                        (Iso.symm (biproduct.isoCoproduct fun (j : J) ↦ F.obj { as := j }))
                        ((biproduct.isoProduct fun (j : J) ↦ F.obj { as := j : Discrete J }) ≪≫ Pi.isoLimit F) :
                      (sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j }) ≅ obj lim F) :
                  obj colim F ≅ obj lim F))
              Y)))
      (limit.π Y { as := j }))
    (CategoryStruct.comp (Y := limit Y)
      (CategoryStruct.comp (Y := colimit X) (colimit.ι X { as := i })
          (Iso.hom
              ((fun (F : Functor.{w, v, w, u} (Discrete J) C) ↦
                  (Iso.trans (Y := sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                      (Iso.symm (Sigma.isoColimit F) : colimit F ≅ sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                      (Iso.trans (Y := biproduct.{w, v, u} fun (j : J) ↦ F.obj { as := j })
                          (Iso.symm (biproduct.isoCoproduct fun (j : J) ↦ F.obj { as := j }))
                          ((biproduct.isoProduct fun (j : J) ↦ F.obj { as := j : Discrete J }) ≪≫ Pi.isoLimit F) :
                        (sigmaObj.{w, v, u} fun (j : J) ↦ F.obj { as := j }) ≅ obj lim F) :
                    obj colim F ≅ obj lim F))
                X) ≫
            Functor.map lim η) :
        X.obj { as := i : Discrete J } ⟶ obj lim Y)
      (limit.π Y { as := j }))

Tactic:
simp_all [Sigma.isoColimit, Pi.isoLimit, biproduct.ι_π, biproduct.ι_π_assoc]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.Limits.Sigma.isoColimit, CategoryTheory.Limits.Pi.isoLimit, CategoryTheory.Limits.biproduct.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (b : J) → f b ⟶ g b
w :
  ∀ (j j_1 : J),
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map p) (π g j)) =
      CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map' p) (π g j))
⊢ Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p) (map' p)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (b : J) → f b ⟶ g b
j j_1 : J
w :
  Eq (α := f j_1 ⟶ g j)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (NatTrans.app (Cocone.ι (Bicone.toCocone (bicone f))) { as := j_1 } :
        obj.{w, v, w, u} (Discrete.functor f) { as := j_1 : Discrete J } ⟶
          obj.{w, v, w, u} (obj (const (Discrete J)) (Cocone.pt.{w, v, w, u} (Bicone.toCocone (bicone f))))
            { as := j_1 : Discrete J })
      (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) { as := j } ≫ p j))
    (p j_1 ≫
      CategoryStruct.comp (Y := Cocone.pt.{w, v, w, u} (Bicone.toCocone (bicone g)))
        (NatTrans.app (Cocone.ι (Bicone.toCocone (bicone g))) { as := j_1 } :
          obj.{w, v, w, u} (Discrete.functor g) { as := j_1 : Discrete J } ⟶
            obj.{w, v, w, u} (obj (const (Discrete J)) (Cocone.pt.{w, v, w, u} (Bicone.toCocone (bicone g))))
              { as := j_1 : Discrete J })
        (NatTrans.app (Cone.π (Bicone.toCone (bicone g))) { as := j }))
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map p) (π g j)) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map' p) (π g j))

Tactic:
simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map_assoc, Limits.IsLimit.map_π,
    ← Bicone.toCone_π_app_mk, ← Bicone.toCocone_ι_app_mk]

Premises used: CategoryTheory.Limits.Bicone.toCocone_ι_app_mk, CategoryTheory.Limits.IsLimit.map_π, CategoryTheory.Limits.Bicone.toCone_π_app_mk, CategoryTheory.Limits.IsColimit.ι_map_assoc, CategoryTheory.Discrete.natTrans_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (b : J) → f b ⟶ g b
j j_1 : J
w :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1) (π f j ≫ p j) =
    p j_1 ≫ CategoryStruct.comp (Y := Bicone.pt.{w, v, u} (bicone g)) (ι g j_1) (π g j)
⊢ Eq (α := f j_1 ⟶ g j)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (NatTrans.app (Cocone.ι (Bicone.toCocone (bicone f))) { as := j_1 } :
        obj.{w, v, w, u} (Discrete.functor f) { as := j_1 : Discrete J } ⟶
          obj.{w, v, w, u} (obj (const (Discrete J)) (Cocone.pt.{w, v, w, u} (Bicone.toCocone (bicone f))))
            { as := j_1 : Discrete J })
      (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) { as := j } ≫ p j))
    (p j_1 ≫
      CategoryStruct.comp (Y := Cocone.pt.{w, v, w, u} (Bicone.toCocone (bicone g)))
        (NatTrans.app (Cocone.ι (Bicone.toCocone (bicone g))) { as := j_1 } :
          obj.{w, v, w, u} (Discrete.functor g) { as := j_1 : Discrete J } ⟶
            obj.{w, v, w, u} (obj (const (Discrete J)) (Cocone.pt.{w, v, w, u} (Bicone.toCocone (bicone g))))
              { as := j_1 : Discrete J })
        (NatTrans.app (Cone.π (Bicone.toCone (bicone g))) { as := j }))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (b : J) → f b ⟶ g b
j j_1 : J
w : Eq.{v + 1} ((if h : j_1 = j then eqToHom ⋯ else 0) ≫ p j) (p j_1 ≫ if h : j_1 = j then eqToHom ⋯ else 0)
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1) (π f j ≫ p j) =
    p j_1 ≫ CategoryStruct.comp (Y := Bicone.pt.{w, v, u} (bicone g)) (ι g j_1) (π g j)

Tactic:
rw [biproduct.ι_π_assoc, biproduct.ι_π]

Premises used: CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.Limits.biproduct.ι_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (b : J) → f b ⟶ g b
j j_1 : J
pos : ∀ (h : j_1 = j), eqToHom ⋯ ≫ p j = p j_1 ≫ eqToHom ⋯
neg : ∀ (h : ¬j_1 = j), Eq.{v + 1} (0 ≫ p j) (p j_1 ≫ 0)
⊢ Eq.{v + 1} ((if h : j_1 = j then eqToHom ⋯ else 0) ≫ p j) (p j_1 ≫ if h : j_1 = j then eqToHom ⋯ else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (b : J) → f b ⟶ g b
j j_1 : J
h : j_1 = j
pos : eqToHom ⋯ ≫ p j_1 = p j_1 ≫ eqToHom ⋯
⊢ eqToHom ⋯ ≫ p j = p j_1 ≫ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (b : J) → f b ⟶ g b
j : J
⊢ eqToHom ⋯ ≫ p j = p j ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (b : J) → f b ⟶ g b
j j_1 : J
h : ¬j_1 = j
⊢ Eq.{v + 1} (0 ≫ p j) (p j_1 ≫ 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (b : J) → f b ⟶ g b
w w₁ :
  ∀ (j j_1 : J),
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map p) (π g j)) =
      CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map' p) (π g j))
w₂ :
  ∀ (j j_1 : J),
    Eq (α := f j_1 ⟶ g j)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (NatTrans.app (Cocone.ι (Bicone.toCocone (bicone f))) { as := j_1 } :
          obj.{w, v, w, u} (Discrete.functor f) { as := j_1 : Discrete J } ⟶
            obj.{w, v, w, u} (obj (const (Discrete J)) (Cocone.pt.{w, v, w, u} (Bicone.toCocone (bicone f))))
              { as := j_1 : Discrete J })
        (NatTrans.app (Cone.π (Bicone.toCone (bicone f))) { as := j } ≫ p j))
      (p j_1 ≫
        CategoryStruct.comp (Y := Cocone.pt.{w, v, w, u} (Bicone.toCocone (bicone g)))
          (NatTrans.app (Cocone.ι (Bicone.toCocone (bicone g))) { as := j_1 } :
            obj.{w, v, w, u} (Discrete.functor g) { as := j_1 : Discrete J } ⟶
              obj.{w, v, w, u} (obj (const (Discrete J)) (Cocone.pt.{w, v, w, u} (Bicone.toCocone (bicone g))))
                { as := j_1 : Discrete J })
          (NatTrans.app (Cone.π (Bicone.toCone (bicone g))) { as := j }))
w₃ :
  ∀ (j j_1 : J),
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1) (π f j ≫ p j) =
      p j_1 ≫ CategoryStruct.comp (Y := Bicone.pt.{w, v, u} (bicone g)) (ι g j_1) (π g j)
w₄ :
  ∀ (j j_1 : J),
    Eq.{v + 1} ((if h : j_1 = j then eqToHom ⋯ else 0) ≫ p j) (p j_1 ≫ if h : j_1 = j then eqToHom ⋯ else 0)
pos : ∀ (j j_1 : J) (h : j_1 = j), eqToHom ⋯ ≫ p j = p j_1 ≫ eqToHom ⋯
neg neg₁ : ∀ (j j_1 : J) (h : ¬j_1 = j), Eq.{v + 1} (0 ≫ p j) (p j_1 ≫ 0)
⊢ Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p) (map' p)

Tactic:
classical
  ext
  dsimp
  simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map_assoc, Limits.IsLimit.map_π,
    ← Bicone.toCone_π_app_mk, ← Bicone.toCocone_ι_app_mk]
  dsimp
  rw [biproduct.ι_π_assoc, biproduct.ι_π]
  split_ifs with h
  · subst h; simp
  · simp

Premises used: CategoryTheory.Limits.Bicone.toCocone_ι_app_mk, CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.Limits.IsLimit.map_π, CategoryTheory.Limits.Bicone.toCone_π_app_mk, CategoryTheory.Limits.IsColimit.ι_map_assoc, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Discrete.natTrans_app