awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i :
  IsIso (C := Functor.{v, v, u, u'} C D) (X := ihom A ⋙ F) (Y := F ⋙ ihom (F.obj A))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
          (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
        (natTrans (frobeniusMorphism F h A)) :
      ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
⊢ IsIso (X := tensorLeft (F.obj A) ⋙ L) (Y := L ⋙ tensorLeft A) (natTrans (frobeniusMorphism F h A))

Tactic:
exact @conjugateEquiv_of_iso _ _ _ _ _ _ _ _ _ _ _ i

Premises used: CategoryTheory.conjugateEquiv_of_iso
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (X := tensorLeft (F.obj A) ⋙ L) (Y := L ⋙ tensorLeft A) (frobeniusMorphism F h A)
rw :
  IsIso (C := Functor.{v, v, u, u'} C D) (X := ihom A ⋙ F) (Y := F ⋙ ihom (F.obj A))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
          (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
        (natTrans (frobeniusMorphism F h A)) :
      ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
⊢ IsIso (X := ihom A ⋙ F) (Y := F ⋙ ihom (F.obj A)) (natTrans (expComparison F A))

Tactic:
rw [← frobeniusMorphism_mate F h]

Premises used: CategoryTheory.frobeniusMorphism_mate
-- Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u'} D
F : Functor.{v, v, u, u'} C D
L : Functor.{v, v, u', u} D C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : MonoidalClosed.{v, u'} D
inst_6 : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (X := tensorLeft (F.obj A) ⋙ L) (Y := L ⋙ tensorLeft A) (frobeniusMorphism F h A)
⊢ IsIso (C := Functor.{v, v, u, u'} C D) (X := ihom A ⋙ F) (Y := F ⋙ ihom (F.obj A))
    ((conjugateEquiv (h.comp (ihom.adjunction A)) (Adjunction.comp (ihom.adjunction (F.obj A)) h) :
          (a : tensorLeft (F.obj A) ⋙ L ⟶ L ⋙ tensorLeft A) → ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))
        (natTrans (frobeniusMorphism F h A)) :
      ihom A ⋙ F ⟶ F ⋙ ihom (F.obj A))

Tactic:
infer_instance
-- 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
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
j : J
k₁ k₂ : Under.{v₂, u₂} j
φ : k₁ ⟶ k₂
dsimp :
  Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₁.right))
      (F₂.map k₁.hom ≫ curry (f.app k₁.right)) (eHomWhiskerLeft C (F₁.obj k₁.right) (F₃.map (Under.Hom.right φ))))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
      (F₂.map k₂.hom ≫ curry (f.app k₂.right)) (eHomWhiskerRight C (F₁.map (Under.Hom.right φ)) (F₃.obj k₂.right)))
⊢ Eq (α :=
    F₂.obj j ⟶ Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k₁)) k₂)
    ((fun (k : Under.{v₂, u₂} j) ↦
          (F₂.map k.hom ≫ curry (f.app k.right) :
            F₂.obj j ⟶
              Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k))
        k₁ ≫
      Functor.map (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k₁)) φ)
    ((fun (k : Under.{v₂, u₂} j) ↦
          (F₂.map k.hom ≫ curry (f.app k.right) :
            F₂.obj j ⟶
              Functor.obj (Functor.obj (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k))
        k₂ ≫
      NatTrans.app (Functor.map (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) φ.op) k₂)

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
f : tensorObj (𝒞 := Functor.category) F₁ F₂ ⟶ F₃
j : J
k₁ k₂ : Under.{v₂, u₂} j
φ : k₁ ⟶ k₂
simp :
  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) ≫ Functor.map (ihom (F₁.obj k₁.right)) (F₃.map (Under.Hom.right φ)))
    (F₂.map k₂.hom ≫
      CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
        (curry (f.app k₂.right)) (NatTrans.app (pre (F₁.map (Under.Hom.right φ))) (F₃.obj k₂.right)))
⊢ Eq (α := F₂.obj j ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₂.right))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₁.right)) (F₃.obj k₁.right))
      (F₂.map k₁.hom ≫ curry (f.app k₁.right)) (eHomWhiskerLeft C (F₁.obj k₁.right) (F₃.map (Under.Hom.right φ))))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj k₂.right)) (F₃.obj k₂.right))
      (F₂.map k₂.hom ≫ curry (f.app k₂.right)) (eHomWhiskerRight C (F₁.map (Under.Hom.right φ)) (F₃.obj k₂.right)))

Tactic:
simp only [enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Category.assoc,
            enrichedOrdinaryCategorySelf_eHomWhiskerRight]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft
-- 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' : J
φ : j ⟶ j'
dsimp :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    ((F₁.map φ ⊗ₘ F₂.map φ) ≫
      uncurry (g.app j' ≫ enrichedHomπ C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃) (Under.mk (𝟙 j'))))
    (uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))) ≫ F₃.map φ)
⊢ Eq (α := (tensorObj (𝒞 := Functor.category) F₁ F₂).obj j ⟶ F₃.obj j')
    ((tensorObj (𝒞 := Functor.category) F₁ F₂).map φ ≫
      uncurry (g.app j' ≫ enrichedHomπ C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃) (Under.mk (𝟙 j'))))
    (uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))) ≫ F₃.map φ)

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' : J
φ : j ⟶ j'
rw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y :=
          Functor.obj
            (Functor.obj (diagram C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) (Opposite.op (Under.mk (𝟙 j'))))
            (Under.mk (𝟙 j')))
          (CategoryStruct.comp (Y :=
            @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
              ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
              ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
            (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))))
            (CategoryStruct.comp (Y :=
              @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _ ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
              (NatTrans.app
                (pre (NatTrans.app (Iso.inv (Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₁))) (Under.mk (𝟙 j'))))
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
              (eHomWhiskerLeft C ((Under.forget j' ⋙ F₁).obj (Under.mk (𝟙 j')))
                (NatTrans.app (Iso.hom (Iso.refl (Under.map φ ⋙ Under.forget j ⋙ F₃))) (Under.mk (𝟙 j'))))))
          (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
          (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    ((F₁.map φ ⊗ₘ F₂.map φ) ≫
      uncurry (g.app j' ≫ enrichedHomπ C (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃) (Under.mk (𝟙 j'))))
    (uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))) ≫ F₃.map φ)

Tactic:
rw [← uncurry_natural_right, tensorHom_def'_assoc, ← uncurry_pre_app,
          ← uncurry_natural_left, Category.assoc, Category.assoc,
          NatTrans.naturality_assoc, functorEnrichedHom_map,
          end_.lift_π_assoc, enrichedOrdinaryCategorySelf_eHomWhiskerRight]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalClosed.uncurry_natural_right, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight, CategoryTheory.MonoidalClosed.uncurry_pre_app, CategoryTheory.MonoidalCategory.tensorHom_def'_assoc, CategoryTheory.MonoidalClosed.uncurry_natural_left, CategoryTheory.Limits.end_.lift_π_assoc, CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_map, CategoryTheory.NatTrans.naturality_assoc
-- 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' : J
φ : j ⟶ j'
rw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
            enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
              @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
                ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
          (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
          (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
          (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
            (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
              enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
                @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
                  ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
                  ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
            (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
              (NatTrans.app (pre (𝟙 (F₁.obj j'))) (F₃.obj j')) (eHomWhiskerLeft C (F₁.obj j') (𝟙 (F₃.obj j')))))
          (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
          (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))

Tactic:
rw [pre_id, NatTrans.id_app, enrichedOrdinaryCategorySelf_eHomWhiskerLeft,
          Functor.map_id, Category.comp_id, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.MonoidalClosed.pre_id, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft
-- 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' : J
φ : j ⟶ j'
e_a :
  Eq (α :=
    enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j'))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
            ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
            ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
      (NatTrans.app (pre (F₁.map φ)) (F₃.obj j')))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
      (Functor.map (ihom (F₁.obj j)) (F₃.map φ)))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (F₁.obj j) (F₂.obj j) ⟶ F₃.obj j')
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
            enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
              @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
                ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
                ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
          (NatTrans.app (pre (F₁.map φ)) (F₃.obj j'))))
    (uncurry
      (g.app j ≫
        CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
          (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
          (Functor.map (ihom (F₁.obj j)) (F₃.map φ))))

Tactic:
congr 2
-- 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' : J
φ : j ⟶ j'
e_a :
  Eq (α :=
    enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j'))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
            ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
            ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
      (eHomWhiskerRight C (F₁.map φ) (F₃.obj j')))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
      (eHomWhiskerLeft C (F₁.obj j) (F₃.map φ)))
⊢ Eq (α :=
    enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j'))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
            ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
            ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
      (NatTrans.app (pre (F₁.map φ)) (F₃.obj j')))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
      (Functor.map (ihom (F₁.obj j)) (F₃.map φ)))

Tactic:
rw [← enrichedOrdinaryCategorySelf_eHomWhiskerRight,
          ← enrichedOrdinaryCategorySelf_eHomWhiskerLeft]

Premises used: CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight, CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft
-- 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' : J
φ : j ⟶ j'
α : Under.mk (𝟙 j) ⟶ (Under.map φ).obj (Under.mk (𝟙 j')) := Under.homMk φ ⋯
⊢ Eq (α :=
    enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j'))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
            ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
            ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
      (eHomWhiskerRight C (F₁.map φ) (F₃.obj j')))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
      (eHomWhiskerLeft C (F₁.obj j) (F₃.map φ)))

Tactic:
(enrichedHom_condition C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) α).symm

Premises used: CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition, CategoryTheory.Functor.comp, CategoryTheory.Under.forget, Eq.symm
-- 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' : J
φ : j ⟶ j'
α : Under.mk (𝟙 j) ⟶ (Under.map φ).obj (Under.mk (𝟙 j')) := Under.homMk φ ⋯
⊢ Eq (α :=
    enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j'))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j')) (F₃.obj j'))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) :
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₁} _ inst inst_1 _ _
            ((Under.forget j ⋙ F₁).obj ((Under.map φ).obj (Under.mk (𝟙 j'))))
            ((Under.forget j ⋙ F₃).obj ((Under.map φ).obj (Under.mk (𝟙 j')))))
      (eHomWhiskerRight C (F₁.map φ) (F₃.obj j')))
    (CategoryStruct.comp (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom (F₁.obj j)) (F₃.obj j))
      (enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)))
      (eHomWhiskerLeft C (F₁.obj j) (F₃.map φ)))

Tactic:
exact (enrichedHom_condition C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) α).symm

Premises used: CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition, CategoryTheory.Functor.comp, CategoryTheory.Under.forget, Eq.symm
-- 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₃
w :
  ∀ (j : 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
⊢ (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) =
    g

Tactic:
ext j