-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Internal.Limits (goal)
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
⊢ 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)
have 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 := sorry } } ▷
              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 := sorry } } :
            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 := sorry } } ⟶
              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 := sorry } } :
              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 := sorry } } :
              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 := sorry } } ⟶
                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)
Tactic: apply hc.hom_ext