Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J✝ : Type w
C✝ : Type uC
inst✝⁶ : Category.{uC', uC} C✝
inst✝⁵ : HasZeroMorphisms C✝
D : Type uD
inst✝⁴ : Category.{uD', uD} D
inst✝³ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBiproductsOfShape J C
X✝ Y✝ : Discrete J ⥤ C
η : X✝ ⟶ Y✝
x✝¹ : Discrete J
i : J
x✝ : Discrete J
j : J
h : i = j
⊢ (colimit.ι X✝ { as := i } ≫
        colim.map η ≫
          ((Sigma.isoColimit Y✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ Y✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ Y✝.obj { as := j }) ≪≫ Pi.isoLimit Y✝).hom) ≫
      limit.π Y✝ { as := j } =
    (colimit.ι X✝ { as := i } ≫
        ((Sigma.isoColimit X✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ X✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ X✝.obj { as := j }) ≪≫ Pi.isoLimit X✝).hom ≫
          lim.map η) ≫
      limit.π Y✝ { as := j }

pp: case neg
J✝ : Type w
C✝ : Type uC
inst✝⁶ : Category.{uC', uC} C✝
inst✝⁵ : HasZeroMorphisms C✝
D : Type uD
inst✝⁴ : Category.{uD', uD} D
inst✝³ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBiproductsOfShape J C
X✝ Y✝ : Discrete J ⥤ C
η : X✝ ⟶ Y✝
x✝¹ : Discrete J
i : J
x✝ : Discrete J
j : J
h : ¬i = j
⊢ (colimit.ι X✝ { as := i } ≫
        colim.map η ≫
          ((Sigma.isoColimit Y✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ Y✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ Y✝.obj { as := j }) ≪≫ Pi.isoLimit Y✝).hom) ≫
      limit.π Y✝ { as := j } =
    (colimit.ι X✝ { as := i } ≫
        ((Sigma.isoColimit X✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ X✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ X✝.obj { as := j }) ≪≫ Pi.isoLimit X✝).hom ≫
          lim.map η) ≫
      limit.π Y✝ { as := j }

Tactic:
<;>

Goal state after:
case pos
J✝ : Type w
C✝ : Type uC
inst✝⁶ : Category.{uC', uC} C✝
inst✝⁵ : HasZeroMorphisms C✝
D : Type uD
inst✝⁴ : Category.{uD', uD} D
inst✝³ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBiproductsOfShape J C
X✝ Y✝ : Discrete J ⥤ C
η : X✝ ⟶ Y✝
x✝¹ : Discrete J
i : J
x✝ : Discrete J
j : J
h : i = j
⊢ (colimit.ι X✝ { as := i } ≫
        colim.map η ≫
          ((Sigma.isoColimit Y✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ Y✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ Y✝.obj { as := j }) ≪≫ Pi.isoLimit Y✝).hom) ≫
      limit.π Y✝ { as := j } =
    (colimit.ι X✝ { as := i } ≫
        ((Sigma.isoColimit X✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ X✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ X✝.obj { as := j }) ≪≫ Pi.isoLimit X✝).hom ≫
          lim.map η) ≫
      limit.π Y✝ { as := j }

case neg
J✝ : Type w
C✝ : Type uC
inst✝⁶ : Category.{uC', uC} C✝
inst✝⁵ : HasZeroMorphisms C✝
D : Type uD
inst✝⁴ : Category.{uD', uD} D
inst✝³ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBiproductsOfShape J C
X✝ Y✝ : Discrete J ⥤ C
η : X✝ ⟶ Y✝
x✝¹ : Discrete J
i : J
x✝ : Discrete J
j : J
h : ¬i = j
⊢ (colimit.ι X✝ { as := i } ≫
        colim.map η ≫
          ((Sigma.isoColimit Y✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ Y✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ Y✝.obj { as := j }) ≪≫ Pi.isoLimit Y✝).hom) ≫
      limit.π Y✝ { as := j } =
    (colimit.ι X✝ { as := i } ≫
        ((Sigma.isoColimit X✝).symm ≪≫
              (biproduct.isoCoproduct fun j ↦ X✝.obj { as := j }).symm ≪≫
                (biproduct.isoProduct fun j ↦ X✝.obj { as := j }) ≪≫ Pi.isoLimit X✝).hom ≫
          lim.map η) ≫
      limit.π Y✝ { as := j }