awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw :
  limit.π F j ▷ limit G ▷ limit H ≫
    Iso.hom (α_ (F.obj j) (limit G) (limit H)) ≫
      F.obj j ◁
        NatTrans.app
          (Cone.π
            { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit G) (limit H),
              π := { app := fun (j : J) ↦ limit.π G j ⊗ₘ limit.π H j, naturality := ⋯ } })
          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)

Tactic:
rw [tensorHom_def, ← whisker_exchange,
        ← whiskerLeft_comp_assoc, limit.lift_π,
        whisker_exchange, ← associator_naturality_left_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.associator_naturality_left_assoc, CategoryTheory.Limits.limit.lift_π
-- 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
conv_rhs :
  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)))
    (((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ Iso.hom (α_ (F.obj j) (G.obj j) (H.obj j)))
    (limit.π F j ▷ limit G ▷ limit H ≫
      Iso.hom (α_ (F.obj j) (limit G) (limit H)) ≫
        F.obj j ◁
          NatTrans.app
            (Cone.π
              { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit G) (limit H),
                π := { app := fun (j : J) ↦ limit.π G j ⊗ₘ limit.π H j, naturality := ⋯ } })
            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)))
    (((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ Iso.hom (α_ (F.obj j) (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))

Tactic:
conv_rhs => rw [tensorHom_def, ← whisker_exchange,
        ← whiskerLeft_comp_assoc, limit.lift_π,
        whisker_exchange, ← associator_naturality_left_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.associator_naturality_left_assoc, CategoryTheory.Limits.limit.lift_π
-- 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
dsimp :
  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)))
    (((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ Iso.hom (α_ (F.obj j) (G.obj j) (H.obj j)))
    (limit.π F j ▷ limit G ▷ limit H ≫
      Iso.hom (α_ (F.obj j) (limit G) (limit H)) ≫ F.obj j ◁ (limit.π G j ⊗ₘ limit.π H 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)))
    (((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ Iso.hom (α_ (F.obj j) (G.obj j) (H.obj j)))
    (limit.π F j ▷ limit G ▷ limit H ≫
      Iso.hom (α_ (F.obj j) (limit G) (limit H)) ≫
        F.obj j ◁
          NatTrans.app
            (Cone.π
              { pt := tensorObj.{v, u} (𝒞 := inst_1) (limit G) (limit H),
                π := { app := fun (j : J) ↦ limit.π G j ⊗ₘ limit.π H j, naturality := ⋯ } })
            j)

Tactic:
dsimp only
-- 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
rw : ((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ Iso.hom (α_ (F.obj j) (G.obj j) (H.obj j))
| limit.π F j ▷ limit G ▷ limit H ≫ Iso.hom (α_ (F.obj j) (limit G) (limit H)) ≫ F.obj j ◁ (limit.π G j ⊗ₘ limit.π H j)

Tactic:
rw [tensorHom_def, whiskerLeft_comp,
        ← associator_naturality_middle_assoc,
        ← associator_naturality_right, ← comp_whiskerRight_assoc,
        ← tensorHom_def, ← tensorHom_def_assoc]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.MonoidalCategory.tensorHom_def_assoc, CategoryTheory.MonoidalCategory.associator_naturality_right
-- 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
conv_rhs :
  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)))
    (((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ Iso.hom (α_ (F.obj j) (G.obj j) (H.obj j)))
    (limit.π F j ▷ limit G ▷ limit H ≫
      Iso.hom (α_ (F.obj j) (limit G) (limit H)) ≫ F.obj j ◁ (limit.π G j ⊗ₘ limit.π H j))
conv_rhs₁ :
  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)))
    (((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ Iso.hom (α_ (F.obj j) (G.obj j) (H.obj j)))
    (((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ Iso.hom (α_ (F.obj j) (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)))
    (((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ Iso.hom (α_ (F.obj j) (G.obj j) (H.obj j)))
    (limit.π F j ▷ limit G ▷ limit H ≫
      Iso.hom (α_ (F.obj j) (limit G) (limit H)) ≫ F.obj j ◁ (limit.π G j ⊗ₘ limit.π H j))

Tactic:
conv_rhs => rw [tensorHom_def, whiskerLeft_comp,
        ← associator_naturality_middle_assoc,
        ← associator_naturality_right, ← comp_whiskerRight_assoc,
        ← tensorHom_def, ← tensorHom_def_assoc]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.MonoidalCategory.tensorHom_def_assoc, CategoryTheory.MonoidalCategory.associator_naturality_right
-- 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
dsimp :
  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 :=
      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)
      ((limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j ⊗ₘ limit.π F j) ≫ Iso.hom (λ_ (F.obj 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)
    (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)

Tactic:
dsimp
-- 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)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F))
      (CategoryStruct.comp (Y := limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
          (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.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j) ▷
        limit F)
      (Iso.hom (λ_ (limit F)) ≫ limit.π F 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 :=
      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)
      ((limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j ⊗ₘ limit.π F j) ≫ Iso.hom (λ_ (F.obj j))))

Tactic:
simp only [tensorHom_def, id_whiskerLeft, Category.assoc,
        Iso.inv_hom_id, Category.comp_id, ← comp_whiskerRight_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.id_whiskerLeft, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc
-- 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
erw :
  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 := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F))
      (NatTrans.app
          (Cone.π
            { 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))) } })
          j ▷
        limit F)
      (Iso.hom (λ_ (limit F)) ≫ limit.π F 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 := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F))
      (CategoryStruct.comp (Y := limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
          (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.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j) ▷
        limit F)
      (Iso.hom (λ_ (limit F)) ≫ limit.π F j))

Tactic:
erw [limit.lift_π]

Premises used: CategoryTheory.Limits.limit.lift_π
-- 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
rw :
  Iso.hom (λ_ (limit F)) ≫ limit.π F j =
    𝟙 (tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F)) ≫
      Iso.hom (λ_ (limit F)) ≫ limit.π F j
rw₁ rw₂ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F) ⟶ F.obj j)
    (Iso.hom (λ_ (limit F)) ≫ limit.π F j) (Iso.hom (λ_ (limit F)) ≫ limit.π F 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 := tensorObj.{v, u} (𝒞 := inst_1) (tensorUnit.{v, u} C (𝒞 := inst_1)) (limit F))
      (NatTrans.app
          (Cone.π
            { 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))) } })
          j ▷
        limit F)
      (Iso.hom (λ_ (limit F)) ≫ limit.π F j))

Tactic:
rw [id_whiskerRight, Category.id_comp]

Premises used: CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.Category.id_comp
-- 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
dsimp :
  Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst_1) (limit F)
        (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 j ⊗ₘ limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j) ≫ Iso.hom (ρ_ (F.obj j))))
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (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))) } } ≫
      (Functor.obj (C :=
              Cone (tensorObj (𝒞 := Functor.category) F ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))))
              (Cone.postcompose (Iso.hom (ρ_ F)))
              {
                pt :=
                  tensorObj.{v, u} (𝒞 := inst_1) (limit F)
                    (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))),
                π :=
                  {
                    app := fun (j : J) ↦
                      limit.π F j ⊗ₘ limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j,
                    naturality := ⋯ :
                    NatTrans
                      (Functor.obj (Functor.const J)
                        (tensorObj.{v, u} (𝒞 := inst_1) (limit F)
                          (limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))))
                      (tensorObj (𝒞 := Functor.category) F
                        ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) } :
                Cone
                  (tensorObj (𝒞 := Functor.category) F
                    ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category))) }).π.app
        j)

Tactic:
dsimp
-- 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) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)))
      (limit F ◁
        CategoryStruct.comp (Y := limit.{w, w, v, u} (J := J) ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)))
          (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.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j))
      (Iso.hom (ρ_ (limit F)) ≫ limit.π F j))
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (limit F) (tensorUnit.{v, u} C (𝒞 := inst_1)) ⟶ F.obj j)
    (Iso.hom (ρ_ (limit F)) ≫ limit.π F j)
    (CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst_1) (limit F)
        (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 j ⊗ₘ limit.π ((𝟙_ (Functor.{w, v, w, u} J C)) (𝒞 := Functor.category)) j) ≫ Iso.hom (ρ_ (F.obj j))))

Tactic:
simp only [tensorHom_def, ← whisker_exchange, whiskerRight_id, Category.assoc, Iso.inv_hom_id,
        Category.comp_id, ← whiskerLeft_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whisker_exchange, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.whiskerRight_id