-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.ColimitPresentation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.52389, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.52389, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P_2 : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
X : C
P : ColimitPresentation.{w, w, v, u} J X
Q : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (P.diag.obj j)
inst_5 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_6 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((Q j).diag.obj i)
c :
  Cocone
    {
      obj := fun (k : Total (I := I) Q) ↦
        Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
      map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
      Total (I := I) Q ⥤ C }
m :
  Cocone.pt (J := Total (I := I) Q) (F :=
      {
        obj := fun (k : Total (I := I) Q) ↦
          Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
        map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
        Total (I := I) Q ⥤ C })
      { pt := X,
        ι :=
          {
            app := fun (k : Total (I := I) Q) ↦
              NatTrans.app (ι (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
                P.ι.app (k.fst (β := fun (j : J) ↦ I j)),
            naturality := ⋯ :
            NatTrans
              {
                obj := fun (k : Total (I := I) Q) ↦
                  Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
                map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
                Total (I := I) Q ⥤ C }
              (Functor.obj (Functor.const (Total (I := I) Q)) X) } :
        Cocone
          {
            obj := fun (k : Total (I := I) Q) ↦
              Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
            map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
            Total (I := I) Q ⥤ C } } ⟶
    c.pt
hm :
  ∀ (j : Total (I := I) Q),
    NatTrans.app
          (Cocone.ι
            { pt := X,
              ι :=
                {
                  app := fun (k : Total (I := I) Q) ↦
                    NatTrans.app (ι (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
                      P.ι.app (k.fst (β := fun (j : J) ↦ I j)),
                  naturality := ⋯ } })
          j ≫
        m =
      c.ι.app j
⊢ m =
    P.isColimit.desc
      { pt := c.pt,
        ι :=
          {
            app := fun (j : J) ↦
              (Q j).isColimit.desc
                { pt := c.pt,
                  ι := { app := fun (i : I j) ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i), naturality := ⋯ } },
            naturality := ⋯ } }
have refine : ∀ (j : J),
  { pt := X, ι := P.ι : Cocone P.diag }.ι.app j ≫ m =
    { pt := X, ι := P.ι : Cocone P.diag }.ι.app j ≫
      P.isColimit.desc
        { pt := c.pt,
          ι :=
            {
              app := fun (j : J) ↦
                (Q j).isColimit.desc
                  { pt := c.pt,
                    ι := { app := fun (i : I j) ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i), naturality := sorry } },
              naturality := sorry } }
Tactic: refine P.isColimit.hom_ext fun j ↦ ?_