-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
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
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 := ⋯ } } :
      (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 := ⋯, map_comp := ⋯ :
              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))
⊢ 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')

Tactic:
simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id,
          (Q j).isColimit.fac]

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.comp_id, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map