-- 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'
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 := ⋯ } } :
      (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 := ⋯ } } :
            { 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) :
      (Q j).diag.obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')
have simp : Eq (α := (Q j).diag.obj i ⟶ c.pt)
  ((Q j).ι.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 ⟶ c.pt)
  (c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i) :
    {
            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 := sorry, map_comp := sorry :
            Total (I := I) Q ⥤ C }.obj
        (Sigma.mk (β := fun (j : J) ↦ I j) j i) ⟶
      Functor.obj (Functor.obj (Functor.const (Total (I := I) Q)) c.pt) (Sigma.mk (β := fun (j : J) ↦ I j) j i))
Tactic: simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id,
          (Q j).isColimit.fac]