awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j : J
w :
  end_.lift
      (fun (k : Under.{v₂, u₂} j) ↦
        F₂.map k.hom ≫
          curry
            (uncurry
              (g.app k.right ≫
                enrichedHomπ C (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₃) (Under.mk (𝟙 k.right)))))
      ⋯ =
    g.app j
⊢ NatTrans.app
      ((fun (f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃) ↦
          ({ app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯,
              naturality := ⋯ } :
            NatTrans F₂ (functorEnrichedHom C F₁ F₃)))
        ((fun (g : F₂ ⟶ functorEnrichedHom C F₁ F₃) ↦
            ({
                app := fun (j : J) ↦
                  uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
                naturality := ⋯ } :
              NatTrans (tensorObj (𝒞 := Functor.category) F₁ F₂) F₃))
          g))
      j =
    g.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j : J
w :
  ∀ (k : Under.{v₂, u₂} j),
    CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)))
        (end_.lift
          (fun (k : Under.{v₂, u₂} j) ↦
            F₂.map k.hom ≫
              curry
                (uncurry
                  (g.app k.right ≫
                    enrichedHomπ C (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₃) (Under.mk (𝟙 k.right)))))
          ⋯)
        (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k) =
      g.app j ≫ end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k
⊢ end_.lift
      (fun (k : Under.{v₂, u₂} j) ↦
        F₂.map k.hom ≫
          curry
            (uncurry
              (g.app k.right ≫
                enrichedHomπ C (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₃) (Under.mk (𝟙 k.right)))))
      ⋯ =
    g.app j

Tactic:
ext k
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j : J
k : Under.{v₂, u₂} j
w :
  g.app j ≫
      enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)
        { left := Comma.left.{0, v₂, v₂, 0, u₂, u₂} (Under.mk (𝟙 k.right)), right := k.right,
          hom := k.hom ≫ 𝟙 k.right } =
    g.app j ≫ end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k
⊢ CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)))
      (end_.lift
        (fun (k : Under.{v₂, u₂} j) ↦
          F₂.map k.hom ≫
            curry
              (uncurry
                (g.app k.right ≫
                  enrichedHomπ C (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₃) (Under.mk (𝟙 k.right)))))
        ⋯)
      (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k) =
    g.app j ≫ end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k

Tactic:
simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, enrichedCategorySelf_hom,
      curry_uncurry, NatTrans.naturality_assoc, functorEnrichedHom_obj, functorEnrichedHom_map,
      Under.map, Comma.mapLeft, Functor.const_obj_obj, Functor.id_obj, Discrete.natTrans_app,
      StructuredArrow.left_eq_id, end_.lift_π, Under.mk_right, Under.mk_hom, Iso.refl_inv,
      NatTrans.id_app, enrichedOrdinaryCategorySelf_eHomWhiskerRight, pre_id, Iso.refl_hom,
      enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Functor.map_id, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight, CategoryTheory.Under.mk_hom, CategoryTheory.StructuredArrow.left_eq_id, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalClosed.pre_id, CategoryTheory.Iso.refl_inv, CategoryTheory.Under.mk_right, CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_obj, CategoryTheory.Comma.mapLeft, CategoryTheory.Functor.map_id, CategoryTheory.Limits.end_.lift_π, CategoryTheory.Functor.id_obj, CategoryTheory.Under.forget_obj, CategoryTheory.NatTrans.id_app, CategoryTheory.MonoidalClosed.enrichedCategorySelf_hom, CategoryTheory.Functor.const_obj_obj, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft, CategoryTheory.Under.map, CategoryTheory.MonoidalClosed.curry_uncurry, CategoryTheory.Iso.refl_hom, CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_map, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Discrete.natTrans_app, CategoryTheory.Enriched.FunctorCategory.diagram_obj_obj
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j : J
k : Under.{v₂, u₂} j
w : k.hom ≫ 𝟙 k.right = k.hom
⊢ g.app j ≫
      enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)
        { left := Comma.left.{0, v₂, v₂, 0, u₂, u₂} (Under.mk (𝟙 k.right)), right := k.right,
          hom := k.hom ≫ 𝟙 k.right } =
    g.app j ≫ end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j : J
k : Under.{v₂, u₂} j
⊢ k.hom ≫ 𝟙 k.right = k.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ : Functor.{v₂, v₁, u₂, u₁} J C
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
dsimp :
  Eq (α := tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)
    {
      app := fun (j : J) ↦
        uncurry ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
      naturality := ⋯ }
    (F₁ ◁ f₂ ≫
      {
        app := fun (j : J) ↦
          uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
        naturality := ⋯ })
⊢ Eq (α := tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)
    ((Equiv.symm homEquiv : (a : F₂ ⟶ functorEnrichedHom C F₁ F₃) → F₁ ⊗ F₂ ⟶ F₃) (f₂ ≫ g) :
      tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)
    (F₁ ◁ f₂ ≫ (Equiv.symm homEquiv : (a : F₂' ⟶ functorEnrichedHom C F₁ F₃) → F₁ ⊗ F₂' ⟶ F₃) g :
      tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)

Tactic:
dsimp [homEquiv]

Premises used: CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ : Functor.{v₂, v₁, u₂, u₁} J C
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
w :
  ∀ (j : J),
    Eq (α := (tensorObj (𝒞 := Functor.category) F₁ F₂).obj j ⟶ F₃.obj j)
      (NatTrans.app
        {
          app := fun (j : J) ↦
            uncurry
              ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
          naturality := ⋯ }
        j)
      (NatTrans.app
        (F₁ ◁ f₂ ≫
          {
            app := fun (j : J) ↦
              uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
            naturality := ⋯ })
        j)
⊢ Eq (α := tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃)
    {
      app := fun (j : J) ↦
        uncurry ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
      naturality := ⋯ }
    (F₁ ◁ f₂ ≫
      {
        app := fun (j : J) ↦
          uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
        naturality := ⋯ })

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ : Functor.{v₂, v₁, u₂, u₁} J C
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
j : J
⊢ Eq (α := (tensorObj (𝒞 := Functor.category) F₁ F₂).obj j ⟶ F₃.obj j)
    (NatTrans.app
      {
        app := fun (j : J) ↦
          uncurry ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
        naturality := ⋯ }
      j)
    (NatTrans.app
      (F₁ ◁ f₂ ≫
        {
          app := fun (j : J) ↦
            uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
          naturality := ⋯ })
      j)

Tactic:
simp [← uncurry_natural_left]

Premises used: CategoryTheory.MonoidalClosed.uncurry_natural_left
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
dsimp :
  Eq (α := F₂ ⟶ functorEnrichedHom C F₁ F₃')
    {
      app := fun (j : J) ↦
        end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯,
      naturality := ⋯ }
    (CategoryStruct.comp (Y := functorEnrichedHom C F₁ F₃)
      { app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯,
        naturality := ⋯ }
      (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
          (functorEnrichedHom C F₁ F₃ ◁
            (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
          (functorEnrichedComp C F₁ F₃ F₃')))
⊢ Eq (α := F₂ ⟶ functorEnrichedHom C F₁ F₃')
    ((homEquiv : (a : F₁ ⊗ F₂ ⟶ F₃') → F₂ ⟶ functorEnrichedHom C F₁ F₃') (f ≫ f₃) : F₂ ⟶ functorEnrichedHom C F₁ F₃')
    (CategoryStruct.comp (Y := functorEnrichedHom C F₁ F₃)
        ((homEquiv : (a : F₁ ⊗ F₂ ⟶ F₃) → F₂ ⟶ functorEnrichedHom C F₁ F₃) f)
        (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
          CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
            (functorEnrichedHom C F₁ F₃ ◁
              (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
            (functorEnrichedComp C F₁ F₃ F₃')) :
      F₂ ⟶ functorEnrichedHom C F₁ F₃')

Tactic:
dsimp [homEquiv]

Premises used: CategoryTheory.MonoidalClosed.FunctorCategory.homEquiv
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
w :
  ∀ (j : J),
    Eq (α := F₂.obj j ⟶ Functor.obj (functorEnrichedHom C F₁ F₃') j)
      (NatTrans.app
        {
          app := fun (j : J) ↦
            end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯,
          naturality := ⋯ }
        j)
      (NatTrans.app
        (CategoryStruct.comp (Y := functorEnrichedHom C F₁ F₃)
          { app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯,
            naturality := ⋯ }
          (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
            CategoryStruct.comp (Y :=
              tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
              (functorEnrichedHom C F₁ F₃ ◁
                (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
              (functorEnrichedComp C F₁ F₃ F₃')))
        j)
⊢ Eq (α := F₂ ⟶ functorEnrichedHom C F₁ F₃')
    {
      app := fun (j : J) ↦
        end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯,
      naturality := ⋯ }
    (CategoryStruct.comp (Y := functorEnrichedHom C F₁ F₃)
      { app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯,
        naturality := ⋯ }
      (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
          (functorEnrichedHom C F₁ F₃ ◁
            (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
          (functorEnrichedComp C F₁ F₃ F₃')))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
w :
  Eq (α := F₂.obj j ⟶ enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃'))
    (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯)
    (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
      Iso.inv (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
            (enrichedHom C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
          (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
            CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
              ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
              (precompEnrichedHom C F₃ F₃' (Under.forget j)))
          (enrichedComp C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
⊢ Eq (α := F₂.obj j ⟶ Functor.obj (functorEnrichedHom C F₁ F₃') j)
    (NatTrans.app
      {
        app := fun (j : J) ↦
          end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯,
        naturality := ⋯ }
      j)
    (NatTrans.app
      (CategoryStruct.comp (Y := functorEnrichedHom C F₁ F₃)
        { app := fun (j : J) ↦ end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯,
          naturality := ⋯ }
        (Iso.inv (ρ_ (functorEnrichedHom C F₁ F₃)) ≫
          CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category) (functorEnrichedHom C F₁ F₃) (functorEnrichedHom C F₃ F₃'))
            (functorEnrichedHom C F₁ F₃ ◁
              (functorHomEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ (J ⥤ C) ⟶ functorEnrichedHom C F₃ F₃') f₃)
            (functorEnrichedComp C F₁ F₃ F₃')))
      j)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
w :
  ∀ (k : Under.{v₂, u₂} j),
    Eq (α :=
      F₂.obj j ⟶ Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) (Opposite.op k)) k)
      (CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')))
        (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯)
        (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) k))
      (CategoryStruct.comp (Y := end_ (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')))
        (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
          Iso.inv (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))) ≫
            CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
                (enrichedHom C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
              (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
                CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
                  ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
                  (precompEnrichedHom C F₃ F₃' (Under.forget j)))
              (enrichedComp C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
        (end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) k))
⊢ Eq (α := F₂.obj j ⟶ enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃'))
    (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯)
    (end_.lift (fun (k : Under.{v₂, u₂} j) ↦ F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
      Iso.inv (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
            (enrichedHom C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))
          (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
            CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
              ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
              (precompEnrichedHom C F₃ F₃' (Under.forget j)))
          (enrichedComp C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')))

Tactic:
ext k
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : MonoidalClosed.{v₁, u₁} C
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : Functor.{v₂, v₁, u₂, u₁} J C
inst_5 : ∀ (F₁ F₂ : Functor.{v₂, v₁, u₂, u₁} J C), HasEnrichedHom C F₁ F₂
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under.{v₂, u₂} j
w :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃'.obj k.right))
    (F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right))
    (F₂.map k.hom ≫
      curry (f.app k.right) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
            (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (Iso.inv (ρ_ (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right))
              (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₃.obj k.right)) (F₃'.obj k.right)))
            (Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k.right)) (F₃.obj k.right) ◁
              CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
                ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
                (enrichedHomπ C F₃ F₃' k.right ≫
                  NatTrans.app (pre (𝟙 (F₃.obj k.right))) (F₃'.obj k.right) ≫
                    Functor.map (ihom (F₃.obj k.right)) (𝟙 (F₃'.obj k.right))))
            (eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right))))
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        Iso.inv
            (ρ_ (Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k)) ≫
          Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k ◁
              CategoryStruct.comp (Y := enrichedHom C F₃ F₃')
                ((Enriched.FunctorCategory.homEquiv C : (a : F₃ ⟶ F₃') → 𝟙_ C ⟶ enrichedHom C F₃ F₃') f₃)
                (enrichedHomπ C F₃ F₃' (Functor.obj (Under.forget j) k) ≫
                  NatTrans.app (pre (NatTrans.app (Iso.inv (Iso.refl (Under.forget j ⋙ F₃))) k))
                      (F₃'.obj (Functor.obj (Under.forget j) k)) ≫
                    Functor.map (ihom ((Under.forget j ⋙ F₃).obj k))
                      (NatTrans.app (Iso.hom (Iso.refl (Under.forget j ⋙ F₃'))) k)) ≫
            eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
              ((Under.forget j ⋙ F₃').obj k)

Tactic:
dsimp