-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Basic (goal)
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
⊢ 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)
        ((limit.π (tensorObj (𝒞 := Functor.category) F G) j ⊗ₘ limit.π H j) ≫
          Iso.hom (α_ (F.obj j) (G.obj j) (H.obj 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)))
have conv_lhs : 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)))
  ((NatTrans.app
          (Cone.π
            { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G),
              π := { app := fun (j : J) ↦ limit.π F j ⊗ₘ limit.π G j, naturality := sorry } })
          j ⊗ₘ
        limit.π H j) ≫
      Iso.hom (α_ (F.obj j) (G.obj j) (H.obj 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 := sorry } })
        (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)))
Tactic: conv_lhs => rw [tensorHom_def, Category.assoc, ← comp_whiskerRight_assoc,
        limit.lift_π, tensor_whiskerLeft, Category.assoc, Category.assoc,
        Iso.inv_hom_id, Category.comp_id,
        ← associator_naturality_right, ← tensorHom_def_assoc]