-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
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
⊢ 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)
have 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)))
Tactic: refine Cofan.IsColimit.mk _ ?_ ?_ ?_