-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic
Goal:
J : Type w
inst : SmallCategory J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasLimitsOfShape.{w, w, v, u} J C
inst_3 : MonoidalCategory.{v, u} C
F : Functor.{w, v, w, u} J C
j : J
simp :
  Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
    (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
          { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
            π :=
              { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                  (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } } ▷
        limit F ≫
      (Functor.obj (C :=
              Cone (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) F))
              (Cone.postcompose (Iso.hom (λ_ F)))
              {
                pt :=
                  tensorObj.{v, u} (𝒞 := inst_1)
                    (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) (limit F),
                π :=
                  {
                    app := fun (j : J) ↦
                      limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j ⊗ₘ limit.π F j,
                    naturality := ⋯ :
                    NatTrans
                      (Functor.obj (Functor.const J)
                        (tensorObj.{v, u} (𝒞 := inst_1)
                          (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
                          (limit F)))
                      (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))
                        F) } :
                Cone
                  (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))
                    F) }).π.app
        j)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := limit F)
      (CategoryStruct.comp (Y :=
        tensorObj.{v, u} (𝒞 := inst_1)
          (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) (limit F))
        (limit.lift (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
              { pt := tensorUnit.{v, u} C (𝒞 := inst_1),
                π :=
                  { app := fun (x : J) ↦ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst_1)), naturality := ⋯ :
                    NatTrans.{w, v, w, u} (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1)))
                      (Functor.obj (Functor.const J) (tensorUnit.{v, u} C (𝒞 := inst_1))) } } ⊗ₘ
            𝟙 (limit F) :
          tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶
            tensorObj.{v, u} (𝒞 := inst_1)
              (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) (limit F))
        (CategoryStruct.comp (Y :=
            limit (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) F))
            (limit.lift (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) F)
              {
                pt :=
                  tensorObj.{v, u} (𝒞 := inst_1)
                    (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) (limit F),
                π :=
                  {
                    app := fun (j : J) ↦
                      limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j ⊗ₘ limit.π F j,
                    naturality := ⋯ } })
            (limMap (Iso.hom (λ_ F))) :
          tensorObj.{v, u} (𝒞 := inst_1)
              (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) (limit F) ⟶
            limit F))
      (limit.π F j))

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

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