-- 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)
x :
  BinaryFan.{v_1, u_1} (C := C) (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))
x_1 : x.pt ⟶ piObj.{u_2, v_1, u_1} X
h₁ : (x_1 ≫ map' (Subtype.val (p := fun (x : I) ↦ P x)) fun (x : { x : I // P x }) ↦ 𝟙 (X (↑x : I))) = x.fst
h₂ : (x_1 ≫ map' (Subtype.val (p := fun (x : I) ↦ ¬P x)) fun (x : { x : I // ¬P x }) ↦ 𝟙 (X (↑x : I))) = x.snd
b : I
pos :
  ∀ (h : P b),
    x_1 ≫ π X b =
      CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} X)
        ((fun
              (s :
                BinaryFan.{v_1, u_1} (C := C) (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))) ↦
            (lift fun (b : I) ↦
                if h : P b then
                  CategoryStruct.comp (Y :=
                    Functor.obj.{0, v_1, 0, u_1}
                      (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)))
                      { as := WalkingPair.left : Discrete WalkingPair })
                    (s.π.app { as := WalkingPair.left })
                    (π (fun (i : { x : I // P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ P x) b h))
                else
                  CategoryStruct.comp (Y :=
                    Functor.obj.{0, v_1, 0, u_1}
                      (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)))
                      { as := WalkingPair.right : Discrete WalkingPair })
                    (s.π.app { as := WalkingPair.right })
                    (π (fun (i : { x : I // ¬P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ ¬P x) b h)) :
              s.pt ⟶ piObj.{u_2, v_1, u_1} X))
          x)
        (π X b)
⊢ x_1 ≫ π X b =
    CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} X)
      ((fun
            (s :
              BinaryFan.{v_1, u_1} (C := C) (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))) ↦
          (lift fun (b : I) ↦
              if h : P b then
                CategoryStruct.comp (Y :=
                  Functor.obj.{0, v_1, 0, u_1}
                    (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)))
                    { as := WalkingPair.left : Discrete WalkingPair })
                  (s.π.app { as := WalkingPair.left })
                  (π (fun (i : { x : I // P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ P x) b h))
              else
                CategoryStruct.comp (Y :=
                  Functor.obj.{0, v_1, 0, u_1}
                    (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)))
                    { as := WalkingPair.right : Discrete WalkingPair })
                  (s.π.app { as := WalkingPair.right })
                  (π (fun (i : { x : I // ¬P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ ¬P x) b h)) :
            s.pt ⟶ piObj.{u_2, v_1, u_1} X))
        x)
      (π X b)
have neg : ∀ (h : ¬P b),
  x_1 ≫ π X b =
    CategoryStruct.comp (Y := piObj.{u_2, v_1, u_1} X)
      ((fun
            (s :
              BinaryFan.{v_1, u_1} (C := C) (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))) ↦
          (lift fun (b : I) ↦
              if h : P b then
                CategoryStruct.comp (Y :=
                  Functor.obj.{0, v_1, 0, u_1}
                    (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)))
                    { as := WalkingPair.left : Discrete WalkingPair })
                  (s.π.app { as := WalkingPair.left })
                  (π (fun (i : { x : I // P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ P x) b h))
              else
                CategoryStruct.comp (Y :=
                  Functor.obj.{0, v_1, 0, u_1}
                    (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)))
                    { as := WalkingPair.right : Discrete WalkingPair })
                  (s.π.app { as := WalkingPair.right })
                  (π (fun (i : { x : I // ¬P x }) ↦ X (↑i : I)) (Subtype.mk (p := fun (x : I) ↦ ¬P x) b h)) :
            s.pt ⟶ piObj.{u_2, v_1, u_1} X))
        x)
      (π X b)
Tactic: by_cases h : P b