-- 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)
rw :
  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))))
⊢ Eq (α := piObj.{u_2, v_1, u_1} X ⟶ piObj.{u_2, v_1, u_1} Y) (map f)
    (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)))))
      (CategoryStruct.comp (Y :=
        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)))
        (prod.map (map fun (i : { x : I // P x }) ↦ f (↑i : I)) (map fun (i : { x : I // ¬P x }) ↦ f (↑i : I)))
        (Iso.inv
          (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)))))))

Tactic:
rw [← Category.assoc, Iso.eq_comp_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv