-- 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
X Y X' Y' : Functor.{w, v, w, u} J C
f : X ⟶ Y
g : X' ⟶ Y'
j : J
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst_1) (Functor.obj lim X) (Functor.obj lim X') ⟶
      (tensorObj (𝒞 := Functor.category) Y Y').obj j)
    (CategoryStruct.comp (Y := limit (tensorObj (𝒞 := Functor.category) Y Y'))
      ((Functor.map lim f ⊗ₘ Functor.map lim g) ≫
        (fun (F G : Functor.{w, v, w, u} J C) ↦
            (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 := ⋯ } } :
              Cone.pt.{w, v, w, u} (J := J) (F := 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 := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G)))
                          (tensorObj (𝒞 := Functor.category) F G) } :
                    Cone (tensorObj (𝒞 := Functor.category) F G) } ⟶
                limit (tensorObj (𝒞 := Functor.category) F G)))
          Y Y')
      (limit.π (tensorObj (𝒞 := Functor.category) Y Y') j))
    (CategoryStruct.comp (Y := limit (tensorObj (𝒞 := Functor.category) Y Y'))
      ((fun (F G : Functor.{w, v, w, u} J C) ↦
              (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 := ⋯ } } :
                Cone.pt.{w, v, w, u} (J := J) (F := 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 := ⋯ :
                          NatTrans (Functor.obj (Functor.const J) (tensorObj.{v, u} (𝒞 := inst_1) (limit F) (limit G)))
                            (tensorObj (𝒞 := Functor.category) F G) } :
                      Cone (tensorObj (𝒞 := Functor.category) F G) } ⟶
                  limit (tensorObj (𝒞 := Functor.category) F G)))
            X X' ≫
          Functor.map lim (f ⊗ₘ g) :
        tensorObj.{v, u} (𝒞 := inst_1) (Functor.obj lim X) (Functor.obj lim X') ⟶
          Functor.obj lim (tensorObj (𝒞 := Functor.category) Y Y'))
      (limit.π (tensorObj (𝒞 := Functor.category) Y Y') j))
have dsimp : Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit X) (limit X') ⟶ tensorObj.{v, u} (𝒞 := inst_1) (Y.obj j) (Y'.obj j))
  (CategoryStruct.comp (Y := limit (tensorObj (𝒞 := Functor.category) Y Y'))
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit Y) (limit Y')) (limMap f ⊗ₘ limMap g)
      (limit.lift (tensorObj (𝒞 := Functor.category) Y Y')
        { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit Y) (limit Y'),
          π := { app := fun (j : J) ↦ limit.π Y j ⊗ₘ limit.π Y' j, naturality := sorry } }))
    (limit.π (tensorObj (𝒞 := Functor.category) Y Y') j))
  (CategoryStruct.comp (Y := limit (tensorObj (𝒞 := Functor.category) Y Y'))
    (CategoryStruct.comp (Y := limit (tensorObj (𝒞 := Functor.category) X X'))
      (limit.lift (tensorObj (𝒞 := Functor.category) X X')
        { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit X) (limit X'),
          π := { app := fun (j : J) ↦ limit.π X j ⊗ₘ limit.π X' j, naturality := sorry } })
      (limMap (f ⊗ₘ g)))
    (limit.π (tensorObj (𝒞 := Functor.category) Y Y') j))
Tactic: dsimp