-- 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
pos :
  ∀ (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 }))
neg :
  ∀ (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 }))
pos₁ :
  ∀ (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 }))
neg₁ :
  ∀ (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 }))
pos₂ :
  ∀ (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 }))
neg₂ :
  ∀ (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 }))
pos₃ :
  ∀ (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 }))
neg₃ :
  ∀ (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 }))
⊢ 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:
classical
      by_cases h : i = j <;>
       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.ι_π