-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Limits
Goal:
J : Type w
inst : Category.{v_1, w} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
F : J ⥤ Mon.{v, u} C
c : Cone (F ⋙ forget C)
hc : IsLimit c
apply :
  ∀ (j : J),
    Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶ (F ⋙ forget C).obj j)
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
            (hc.lift
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                    π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ▷
                c.pt :
              tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶
                tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
            (hc.lift
                { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                  π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
              Cone.pt.{v_1, v, w, u} (J := J) (F := F ⋙ forget C)
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                    π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ⟶
                c.pt) ≫
          c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶ (F ⋙ forget C).obj j)
      ((Iso.hom (α_ c.pt c.pt c.pt) ≫
            CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
              (c.pt ◁
                  hc.lift
                    { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                      π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
                tensorObj.{v, u} (𝒞 := inst_1) c.pt (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) ⟶
                  tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
              (hc.lift
                  { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                    π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
                Cone.pt.{v_1, v, w, u} (J := J) (F := F ⋙ forget C)
                    { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                      π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ⟶
                  c.pt)) ≫
          c.π.app j :
        tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶ (F ⋙ forget C).obj j)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶ c.pt)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
        (hc.lift
              { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ▷
            c.pt :
          tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶
            tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
        (hc.lift
            { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
              π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
          Cone.pt.{v_1, v, w, u} (J := J) (F := F ⋙ forget C)
              { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ⟶
            c.pt) :
      tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶ c.pt)
    (Iso.hom (α_ c.pt c.pt c.pt) ≫
        CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
          (c.pt ◁
              hc.lift
                { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                  π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
            tensorObj.{v, u} (𝒞 := inst_1) c.pt (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) ⟶
              tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt)
          (hc.lift
              { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } :
            Cone.pt.{v_1, v, w, u} (J := J) (F := F ⋙ forget C)
                { pt := tensorObj.{v, u} (𝒞 := inst_1) c.1 c.1,
                  π := { app := fun (X : J) ↦ (c.π.app X ⊗ₘ c.π.app X) ≫ μ, naturality := ⋯ } } ⟶
              c.pt) :
      tensorObj.{v, u} (𝒞 := inst_1) (tensorObj.{v, u} (𝒞 := inst_1) c.pt c.pt) c.pt ⟶ c.pt)

Tactic:
apply hc.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext