-- 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₁
dsimp :
  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))
⊢ Eq (α :=
    (CostructuredArrow.proj L Y₁ ⋙ F).obj j ⟶
      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 ≫ f')) g),
              naturality := ⋯ } })
    (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 := ⋯ } }))
    (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 := ⋯ } })))

Tactic:
dsimp