-- Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
inst_3 : Category.{v_4, u_4} H
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
F : Functor.{v_1, v_4, u_1, u_4} C H
inst_4 : L.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
simp :
  Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map (f ≫ f')) j) :
      (CostructuredArrow.proj L Y₃ ⋙ F).obj (obj (CostructuredArrow.map (f ≫ f')) j) ⟶
        colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map f') (obj (CostructuredArrow.map f) j)))
⊢ Eq (α := F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y₁ ⋙ F))
        (colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j)
        (colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
            ι :=
              {
                app := fun (g : CostructuredArrow L Y₁) ↦
                  colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map (f ≫ f')) g),
                naturality := ⋯ } }) :
      F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))
    (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y₁ ⋙ F))
        (colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j)
        (CategoryStruct.comp (Y := colimit (CostructuredArrow.proj L Y₂ ⋙ F))
          (colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
              { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
                ι :=
                  {
                    app := fun (g : CostructuredArrow L Y₁) ↦
                      colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) (obj (CostructuredArrow.map f) g),
                    naturality := ⋯ } } :
            colimit (CostructuredArrow.proj L Y₁ ⋙ F) ⟶
              Cocone.pt (J := CostructuredArrow L Y₁) (F := CostructuredArrow.proj L Y₁ ⋙ F)
                { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
                  ι :=
                    {
                      app := fun (g : CostructuredArrow L Y₁) ↦
                        colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) (obj (CostructuredArrow.map f) g),
                      naturality := ⋯ } })
          (colimit.desc (CostructuredArrow.proj L Y₂ ⋙ F)
            { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
              ι :=
                {
                  app := fun (g : CostructuredArrow L Y₂) ↦
                    colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) (obj (CostructuredArrow.map f') g),
                  naturality := ⋯ } })) :
      F.obj j.left ⟶ colimit (CostructuredArrow.proj L Y₃ ⋙ F))

Tactic:
simp only [colimit.ι_desc, colimit.ι_desc_assoc, comp_obj, CostructuredArrow.proj_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.CostructuredArrow.proj_obj, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.ι_desc_assoc