-- 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 ⟶ 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)))))))
have 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))))
Tactic: rw [← Category.assoc, Iso.eq_comp_inv]