-- 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))
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
have 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)
Tactic: ⟨a, b⟩