-- 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 G H : Functor.{w, v, w, u} J C
j : J
simp :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G)) (limit H) ⟶
      tensorObj.{v, u} (𝒞 := inst_1) (F.obj j) (tensorObj.{v, u} (𝒞 := inst_1) (G.obj j) (H.obj j)))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit (tensorObj (𝒞 := Functor.category) F G)) (limit H))
        (limit.lift (tensorObj (𝒞 := Functor.category) F G)
            { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G),
              π := { app := fun (j : J) ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } } ▷
          limit H)
        (NatTrans.app
          (Cone.π
            (Functor.obj (Cone.postcompose (Iso.hom (α_ F G H)))
              { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit (tensorObj (𝒞 := Functor.category) F G)) (limit H),
                π :=
                  { app := fun (j : J) ↦ limit.π (tensorObj (𝒞 := Functor.category) F G) j ⊗ₘ limit.π H j,
                    naturality := ⋯ } }))
          j) :
      tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G)) (limit H) ⟶
        tensorObj.{v, u} (𝒞 := inst_1) (F.obj j) (tensorObj.{v, u} (𝒞 := inst_1) (G.obj j) (H.obj j)))
    (Iso.hom (α_ (limit F) (limit G) (limit H)) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit (tensorObj (𝒞 := Functor.category) G H)))
          (limit F ◁
            limit.lift (tensorObj (𝒞 := Functor.category) G H)
              { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit G) (limit H),
                π := { app := fun (j : J) ↦ limit.π G j ⊗ₘ limit.π H j, naturality := ⋯ } })
          (limit.π F j ⊗ₘ limit.π (tensorObj (𝒞 := Functor.category) G H) j) :
      tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G)) (limit H) ⟶
        tensorObj.{v, u} (𝒞 := inst_1) (F.obj j) (tensorObj.{v, u} (𝒞 := inst_1) (G.obj j) (H.obj j)))
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G)) (limit H) ⟶
      tensorObj.{v, u} (𝒞 := inst_1) (F.obj j) (tensorObj.{v, u} (𝒞 := inst_1) (G.obj j) (H.obj j)))
    (CategoryStruct.comp (Y := limit (tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H)))
        (CategoryStruct.comp (Y :=
          tensorObj.{v, u} (𝒞 := inst_1) (limit (tensorObj (𝒞 := Functor.category) F G)) (limit H))
          (limit.lift (tensorObj (𝒞 := Functor.category) F G)
                { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G),
                  π := { app := fun (j : J) ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } } ⊗ₘ
              𝟙 (limit H) :
            tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G)) (limit H) ⟶
              tensorObj.{v, u} (𝒞 := inst_1) (limit (tensorObj (𝒞 := Functor.category) F G)) (limit H))
          (CategoryStruct.comp (Y :=
              limit (tensorObj (𝒞 := Functor.category) (tensorObj (𝒞 := Functor.category) F G) H))
              (limit.lift (tensorObj (𝒞 := Functor.category) (tensorObj (𝒞 := Functor.category) F G) H)
                { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit (tensorObj (𝒞 := Functor.category) F G)) (limit H),
                  π :=
                    { app := fun (j : J) ↦ limit.π (tensorObj (𝒞 := Functor.category) F G) j ⊗ₘ limit.π H j,
                      naturality := ⋯ } })
              (limMap (Iso.hom (α_ F G H))) :
            tensorObj.{v, u} (𝒞 := inst_1) (limit (tensorObj (𝒞 := Functor.category) F G)) (limit H) ⟶
              limit (tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H))))
        (limit.π (tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H)) j) :
      tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G)) (limit H) ⟶
        tensorObj.{v, u} (𝒞 := inst_1) (F.obj j) (tensorObj.{v, u} (𝒞 := inst_1) (G.obj j) (H.obj j)))
    (CategoryStruct.comp (Y := limit (tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H)))
        (Iso.hom (α_ (limit F) (limit G) (limit H)) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit (tensorObj (𝒞 := Functor.category) G H)))
            (𝟙 (limit F) ⊗ₘ
                limit.lift (tensorObj (𝒞 := Functor.category) G H)
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit G) (limit H),
                    π := { app := fun (j : J) ↦ limit.π G j ⊗ₘ limit.π H j, naturality := ⋯ } } :
              tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorObj.{v, u} (𝒞 := inst_1) (limit G) (limit H)) ⟶
                tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit (tensorObj (𝒞 := Functor.category) G H)))
            (limit.lift (tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H))
                { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit (tensorObj (𝒞 := Functor.category) G H)),
                  π :=
                    { app := fun (j : J) ↦ limit.π F j ⊗ₘ limit.π (tensorObj (𝒞 := Functor.category) G H) j,
                      naturality := ⋯ } } :
              Cone.pt.{w, v, w, u} (J := J) (F :=
                  tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H))
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit (tensorObj (𝒞 := Functor.category) G H)),
                    π :=
                      { app := fun (j : J) ↦ limit.π F j ⊗ₘ limit.π (tensorObj (𝒞 := Functor.category) G H) j,
                        naturality := ⋯ :
                        NatTrans
                          (Functor.obj (Functor.const J)
                            (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit (tensorObj (𝒞 := Functor.category) G H))))
                          (tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H)) } :
                    Cone (tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H)) } ⟶
                limit (tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H))))
        (limit.π (tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H)) j) :
      tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G)) (limit H) ⟶
        tensorObj.{v, u} (𝒞 := inst_1) (F.obj j) (tensorObj.{v, u} (𝒞 := inst_1) (G.obj j) (H.obj j)))

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

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