-- 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))
refine_1 :
  (t :
      Cofan (C := C) fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b) →
    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) ⟶
      t.pt
refine_2 :
  ∀
    (t :
      Cofan (C := C) fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
    (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
refine_3 :
  ∀
    (t :
      Cofan (C := C) fun (x : (a : α) × β a) ↦
        match (motive := (a : α) × β a → C) x with
        | ⟨a, b⟩ => Y a b)
    (m :
      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) ⟶
        t.pt),
    (∀ (j : (a : α) × β 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 ≫
            m =
          t.inj j) →
      m =
        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)))
⊢ IsColimit (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)

Tactic:
refine Cofan.IsColimit.mk _ ?_ ?_ ?_

Premises used: CategoryTheory.Limits.Cofan.IsColimit.mk