-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.PiProd (goal)
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)
⊢ 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))))
have 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))))))
              sorry))))))
  (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))))))
              sorry)))))
    (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]