-- 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 }
j j' : J
u : j ⟶ j'
⊢ Eq (α := P.diag.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')
    (P.diag.map u ≫
        (Q j').isColimit.desc
          { pt := c.pt,
            ι := { app := fun (i : I j') ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j' i), naturality := ⋯ } } :
      P.diag.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')
    (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) 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 := ⋯ } } :
          { pt := P.diag.obj j, ι := (Q j).ι : Cocone (Q j).diag }.pt ⟶
            Cocone.pt.{w, v, w, u} (J := I j) (F := (Q j).diag)
              { pt := c.pt,
                ι := { app := fun (i : I j) ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i), naturality := ⋯ } })
        (Functor.map (Functor.obj (Functor.const J) c.pt) u) :
      P.diag.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')
have refine : ∀ (i : I j),
  Eq (α := (Q j).diag.obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')
    ({ pt := P.diag.obj j, ι := (Q j).ι : Cocone (Q j).diag }.ι.app i ≫
        P.diag.map u ≫
          (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 } } :
      (Q j).diag.obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')
    ({ pt := P.diag.obj j, ι := (Q j).ι : Cocone (Q j).diag }.ι.app i ≫
        CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) 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 } } :
            { pt := P.diag.obj j, ι := (Q j).ι : Cocone (Q j).diag }.pt ⟶
              Cocone.pt.{w, v, w, u} (J := I j) (F := (Q j).diag)
                { pt := c.pt,
                  ι := { app := fun (i : I j) ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i), naturality := sorry } })
          (Functor.map (Functor.obj (Functor.const J) c.pt) u) :
      (Q j).diag.obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')
Tactic: refine (Q j).isColimit.hom_ext fun i ↦ ?_