-- 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.HasPointwiseRightKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : StructuredArrow Y₃ L
dsimp :
  Eq (α := limit (StructuredArrow.proj Y₁ L ⋙ F) ⟶ F.obj j.right)
    (CategoryStruct.comp (Y := limit (StructuredArrow.proj Y₃ L ⋙ F))
        (limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
          { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
            π :=
              {
                app := fun (g : StructuredArrow Y₃ L) ↦
                  limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map (f ≫ f')) g),
                naturality := ⋯ } })
        (limit.π (StructuredArrow.proj Y₃ L ⋙ F) j) :
      limit (StructuredArrow.proj Y₁ L ⋙ F) ⟶ F.obj j.right)
    (CategoryStruct.comp (Y := limit (StructuredArrow.proj Y₃ L ⋙ F))
        (CategoryStruct.comp (Y := limit (StructuredArrow.proj Y₂ L ⋙ F))
          (limit.lift (StructuredArrow.proj Y₂ L ⋙ F)
              { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
                π :=
                  {
                    app := fun (g : StructuredArrow Y₂ L) ↦
                      limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map f) g),
                    naturality := ⋯ } } :
            Cone.pt (J := StructuredArrow Y₂ L) (F := StructuredArrow.proj Y₂ L ⋙ F)
                { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
                  π :=
                    {
                      app := fun (g : StructuredArrow Y₂ L) ↦
                        limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map f) g),
                      naturality := ⋯ :
                      NatTrans (obj (const (StructuredArrow Y₂ L)) (limit (StructuredArrow.proj Y₁ L ⋙ F)))
                        (StructuredArrow.proj Y₂ L ⋙ F) } :
                  Cone (StructuredArrow.proj Y₂ L ⋙ F) } ⟶
              limit (StructuredArrow.proj Y₂ L ⋙ F))
          (limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
              { pt := limit (StructuredArrow.proj Y₂ L ⋙ F),
                π :=
                  {
                    app := fun (g : StructuredArrow Y₃ L) ↦
                      limit.π (StructuredArrow.proj Y₂ L ⋙ F) (obj (StructuredArrow.map f') g),
                    naturality := ⋯ } } :
            Cone.pt (J := StructuredArrow Y₃ L) (F := StructuredArrow.proj Y₃ L ⋙ F)
                { pt := limit (StructuredArrow.proj Y₂ L ⋙ F),
                  π :=
                    {
                      app := fun (g : StructuredArrow Y₃ L) ↦
                        limit.π (StructuredArrow.proj Y₂ L ⋙ F) (obj (StructuredArrow.map f') g),
                      naturality := ⋯ :
                      NatTrans (obj (const (StructuredArrow Y₃ L)) (limit (StructuredArrow.proj Y₂ L ⋙ F)))
                        (StructuredArrow.proj Y₃ L ⋙ F) } :
                  Cone (StructuredArrow.proj Y₃ L ⋙ F) } ⟶
              limit (StructuredArrow.proj Y₃ L ⋙ F)))
        (limit.π (StructuredArrow.proj Y₃ L ⋙ F) j) :
      limit (StructuredArrow.proj Y₁ L ⋙ F) ⟶ F.obj j.right)
⊢ Eq (α :=
    Cone.pt (J := StructuredArrow Y₃ L) (F := StructuredArrow.proj Y₃ L ⋙ F)
        { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
          π :=
            {
              app := fun (g : StructuredArrow Y₃ L) ↦
                limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map (f ≫ f')) g),
              naturality := ⋯ :
              NatTrans (obj (const (StructuredArrow Y₃ L)) (limit (StructuredArrow.proj Y₁ L ⋙ F)))
                (StructuredArrow.proj Y₃ L ⋙ F) } :
          Cone (StructuredArrow.proj Y₃ L ⋙ F) } ⟶
      (StructuredArrow.proj Y₃ L ⋙ F).obj j)
    (CategoryStruct.comp (Y := limit (StructuredArrow.proj Y₃ L ⋙ F))
      (limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
        { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
          π :=
            {
              app := fun (g : StructuredArrow Y₃ L) ↦
                limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map (f ≫ f')) g),
              naturality := ⋯ } })
      (limit.π (StructuredArrow.proj Y₃ L ⋙ F) j))
    (CategoryStruct.comp (Y := limit (StructuredArrow.proj Y₃ L ⋙ F))
      (CategoryStruct.comp (Y := limit (StructuredArrow.proj Y₂ L ⋙ F))
        (limit.lift (StructuredArrow.proj Y₂ L ⋙ F)
            { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
              π :=
                {
                  app := fun (g : StructuredArrow Y₂ L) ↦
                    limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map f) g),
                  naturality := ⋯ } } :
          Cone.pt (J := StructuredArrow Y₂ L) (F := StructuredArrow.proj Y₂ L ⋙ F)
              { pt := limit (StructuredArrow.proj Y₁ L ⋙ F),
                π :=
                  {
                    app := fun (g : StructuredArrow Y₂ L) ↦
                      limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map f) g),
                    naturality := ⋯ :
                    NatTrans (obj (const (StructuredArrow Y₂ L)) (limit (StructuredArrow.proj Y₁ L ⋙ F)))
                      (StructuredArrow.proj Y₂ L ⋙ F) } :
                Cone (StructuredArrow.proj Y₂ L ⋙ F) } ⟶
            limit (StructuredArrow.proj Y₂ L ⋙ F))
        (limit.lift (StructuredArrow.proj Y₃ L ⋙ F)
            { pt := limit (StructuredArrow.proj Y₂ L ⋙ F),
              π :=
                {
                  app := fun (g : StructuredArrow Y₃ L) ↦
                    limit.π (StructuredArrow.proj Y₂ L ⋙ F) (obj (StructuredArrow.map f') g),
                  naturality := ⋯ } } :
          Cone.pt (J := StructuredArrow Y₃ L) (F := StructuredArrow.proj Y₃ L ⋙ F)
              { pt := limit (StructuredArrow.proj Y₂ L ⋙ F),
                π :=
                  {
                    app := fun (g : StructuredArrow Y₃ L) ↦
                      limit.π (StructuredArrow.proj Y₂ L ⋙ F) (obj (StructuredArrow.map f') g),
                    naturality := ⋯ :
                    NatTrans (obj (const (StructuredArrow Y₃ L)) (limit (StructuredArrow.proj Y₂ L ⋙ F)))
                      (StructuredArrow.proj Y₃ L ⋙ F) } :
                Cone (StructuredArrow.proj Y₃ L ⋙ F) } ⟶
            limit (StructuredArrow.proj Y₃ L ⋙ F)))
      (limit.π (StructuredArrow.proj Y₃ L ⋙ F) j))

Tactic:
dsimp