-- 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 }
x : Total (I := I) Q
j : J
i : I j
⊢ CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Total (I := I) Q))
          (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 } }))
        (Sigma.mk (β := fun (j : J) ↦ I j) j i))
      (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 := ⋯ } })
        (Sigma.mk (β := fun (j : J) ↦ I j) j i))
      (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 := ⋯ } }) =
    c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i)

Tactic:
simp [P.isColimit.fac, (Q j).isColimit.fac]

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.IsColimit.fac