-- 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
simp :
  Eq (α := limit (StructuredArrow.proj Y₁ L ⋙ F) ⟶ F.obj j.right)
    (limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map (f ≫ f')) j) :
      limit (StructuredArrow.proj Y₁ L ⋙ F) ⟶
        (StructuredArrow.proj Y₁ L ⋙ F).obj (obj (StructuredArrow.map (f ≫ f')) j))
    (limit.π (StructuredArrow.proj Y₁ L ⋙ F) (obj (StructuredArrow.map f) (obj (StructuredArrow.map f') j)))
⊢ 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)

Tactic:
simp only [limit.lift_π, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.lift_π