-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
h :
  Eq.{u + 1} (α := C) (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      (Cocone.pt (J := Discrete (ι × ι')) (F :=
        Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
        (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
          (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))) →
    sigmaObj.{u_1, v, u} X =
        Cocone.pt.{u_1, v, u_1, u} (J := Discrete ι) (F := Discrete.functor X)
          (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i) →
      Eq (α :=
        {P : C} →
          (p : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ P) →
            (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) ⟶ P)
        (@Sigma.desc (ι × ι') C inst (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) ⋯)
        (@Cofan.IsColimit.desc (ι × ι') C inst (fun (b : ι × ι') ↦ pullback (f b.1) (g b.2))
          (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (f p.1) (g p.2))
            (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)))
          (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))
⊢ IsPullback (P := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) (X :=
    sigmaObj.{u_1, v, u} X) (Y := sigmaObj.{u_2, v, u} Y)
    (Sigma.desc fun (p : ι × ι') ↦ pullback.fst (f p.1) (g p.2) ≫ Sigma.ι X p.1)
    (Sigma.desc fun (p : ι × ι') ↦ pullback.snd (f p.1) (g p.2) ≫ Sigma.ι Y p.2) (Sigma.desc f) (Sigma.desc g)
have h₁ : Eq.{u + 1} (α := C) (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
    (Cocone.pt (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))) →
  sigmaObj.{u_2, v, u} Y =
      Cocone.pt.{u_2, v, u_2, u} (J := Discrete ι') (F := Discrete.functor Y)
        (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i) →
    Eq (α :=
      {P : C} →
        (p : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ P) →
          (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) ⟶ P)
      (@Sigma.desc (ι × ι') C inst (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) sorry)
      (@Cofan.IsColimit.desc (ι × ι') C inst (fun (b : ι × ι') ↦ pullback (f b.1) (g b.2))
        (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)))
        (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))
Tactic: convert!
    IsUniversalColimit.isPullback_prod_of_isColimit (d :=
      Cofan.mk _ (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2))) (hd :=
      coproductIsCoproduct (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2))) (a :=
      Cofan.mk _ <| fun i ↦ Sigma.ι _ i) (b := Cofan.mk _ <| fun i ↦ Sigma.ι _ i) ?_ ?_ f g
      (Sigma.desc f) (Sigma.desc g) (fun i j ↦ IsPullback.of_hasPullback (f i) (g j))