-- Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd
Goal:
C : Type u_1
I : Type u_2
inst : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst_1 : HasProduct.{u_2, v_1, u_1} X
inst_2 : HasProduct.{u_2, v_1, u_1} Y
inst_3 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ X (↑i : I)
inst_4 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ X (↑i : I)
inst_5 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // P x }) ↦ Y (↑i : I)
inst_6 : HasProduct.{u_2, v_1, u_1} (C := C) fun (i : { x : I // ¬P x }) ↦ Y (↑i : I)
inst_7 : (i : I) → Decidable (P i)
dsimp :
  Eq (α :=
    piObj.{u_2, v_1, u_1} X ⟶
      prod.{v_1, u_1} (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ Y (↑i : I))
        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ Y (↑i : I)))
    (CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} Y) (map f)
      (Iso.hom
        (Functor.mapIso
          (Cone.forget
            (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ Y (↑i : I))
              (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ Y (↑i : I))))
          (IsLimit.uniqueUpToIso (binaryFanOfPropIsLimit Y P)
            (IsLimit.ofIsoLimit (r :=
              limit.cone
                (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ Y (↑i : I))
                  (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ Y (↑i : I))))
              (limit.isLimit
                (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ Y (↑i : I))
                  (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ Y (↑i : I))))
              (Cone.ext
                (Iso.refl
                  (Cone.pt.{0, v_1, 0, u_1} (F :=
                    pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ Y (↑i : I))
                      (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ Y (↑i : I)))
                    (limit.cone
                      (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ Y (↑i : I))
                        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ Y (↑i : I))))))
                ⋯))))))
    (CategoryStruct.comp (Y :=
      Cone.pt.{0, v_1, 0, u_1} (F :=
        pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
          (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
        (BinaryFan.mk (P :=
          prod.{v_1, u_1} (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
            (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
          prod.fst prod.snd))
      (Iso.hom
        (Functor.mapIso
          (Cone.forget
            (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
              (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))))
          (IsLimit.uniqueUpToIso (binaryFanOfPropIsLimit X P)
            (IsLimit.ofIsoLimit (r :=
              limit.cone
                (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                  (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))))
              (limit.isLimit
                (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                  (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))))
              (Cone.ext
                (Iso.refl
                  (Cone.pt.{0, v_1, 0, u_1} (F :=
                    pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                      (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
                    (limit.cone
                      (pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
                        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I))))))
                ⋯)))))
      (prod.map (map fun (i : { x : I // P x }) ↦ f (↑i : I)) (map fun (i : { x : I // ¬P x }) ↦ f (↑i : I))))
⊢ Eq (α :=
    piObj.{u_2, v_1, u_1} X ⟶
      prod.{v_1, u_1} (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ Y (↑i : I))
        (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ Y (↑i : I)))
    (CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} Y) (map f)
      (Iso.hom
        (IsLimit.conePointUniqueUpToIso (binaryFanOfPropIsLimit Y P)
          (prodIsProd (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ Y (↑i : I))
            (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ Y (↑i : I))))))
    (CategoryStruct.comp (Y :=
      Cone.pt.{0, v_1, 0, u_1} (F :=
        pair (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
          (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
        (BinaryFan.mk (P :=
          prod.{v_1, u_1} (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
            (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))
          prod.fst prod.snd))
      (Iso.hom
        (IsLimit.conePointUniqueUpToIso (binaryFanOfPropIsLimit X P)
          (prodIsProd (piObj.{u_2, v_1, u_1} fun (i : { x : I // P x }) ↦ X (↑i : I))
            (piObj.{u_2, v_1, u_1} fun (i : { x : I // ¬P x }) ↦ X (↑i : I)))))
      (prod.map (map fun (i : { x : I // P x }) ↦ f (↑i : I)) (map fun (i : { x : I // ¬P x }) ↦ f (↑i : I))))

Tactic:
dsimp only [IsLimit.conePointUniqueUpToIso, binaryFanOfProp, prodIsProd]

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.Pi.binaryFanOfProp, CategoryTheory.Limits.prodIsProd