-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β_1 : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : α → C
c : Cofan.{w₂, v, u} X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan (C := C) fun (x : (a : α) × β a) ↦
    match (motive := (a : α) × β a → C) x with
    | ⟨a, b⟩ => Y a b
refine_2 :
  ∀ (a : α) (b : β a),
    Eq.{v + 1} (α :=
      (match (motive := (a : α) × β a → C) Sigma.mk (β := fun (a : α) ↦ β a) a b with
        | ⟨a, b⟩ => Y a b) ⟶
        t.pt)
      (CategoryStruct.comp (Y :=
          Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
            Discrete.functor fun (x : (a : α) × β a) ↦
              match (motive := (a : α) × β a → C) x with
              | ⟨a, b⟩ => Y a b)
            (mk c.pt fun (x : (a : α) × β a) ↦
              match (motive :=
                (x : (a : α) × β a) →
                  (fun (x : (a : α) × β a) ↦
                        (match (motive := (a : α) × β a → C) x with
                          | ⟨a, b⟩ => Y a b :
                          C))
                      x ⟶
                    c.pt)
                x with
              | ⟨a, b⟩ => π a b ≫ c.inj a))
          (inj (f := fun (x : (a : α) × β a) ↦
            match (motive := (a : α) × β a → C) x with
            | ⟨a, b⟩ => Y a b)
            (mk c.pt fun (x : (a : α) × β a) ↦
              match (motive :=
                (x : (a : α) × β a) →
                  (fun (x : (a : α) × β a) ↦
                        (match (motive := (a : α) × β a → C) x with
                          | ⟨a, b⟩ => Y a b :
                          C))
                      x ⟶
                    c.pt)
                x with
              | ⟨a, b⟩ => π a b ≫ c.inj a)
            (Sigma.mk (β := fun (a : α) ↦ β a) a b))
          (hc.desc
            (mk t.1 fun (a : α) ↦
              (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b)))) :
        (match (motive := (a : α) × β a → C) Sigma.mk (β := fun (a : α) ↦ β a) a b with
          | ⟨a, b⟩ => Y a b) ⟶
          t.pt)
      (t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b) :
        (match (motive := (a : α) × β a → C) Sigma.mk (β := fun (a : α) ↦ β a) a b with
          | ⟨a, b⟩ => Y a b) ⟶
          t.pt)
⊢ ∀ (j : (a : α) × β a),
    CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete ((a : α) × β a)) (F :=
          Discrete.functor fun (x : (a : α) × β a) ↦
            match (motive := (a : α) × β a → C) x with
            | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a))
        (inj (f := fun (x : (a : α) × β a) ↦
          match (motive := (a : α) × β a → C) x with
          | ⟨a, b⟩ => Y a b)
          (mk c.pt fun (x : (a : α) × β a) ↦
            match (motive :=
              (x : (a : α) × β a) →
                (fun (x : (a : α) × β a) ↦
                      (match (motive := (a : α) × β a → C) x with
                        | ⟨a, b⟩ => Y a b :
                        C))
                    x ⟶
                  c.pt)
              x with
            | ⟨a, b⟩ => π a b ≫ c.inj a)
          j)
        (hc.desc
          (mk t.1 fun (a : α) ↦ (hs a).desc (mk t.pt fun (b : β a) ↦ t.inj (Sigma.mk (β := fun (a : α) ↦ β a) a b)))) =
      t.inj j

Tactic:
⟨a, b⟩