awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
g : tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
i j : J
f : i ⟶ j
rw :
  Iso.hom (ρ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
    g ≫
      enrichedHomπ V F₁ F₂ j ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
          (Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
            ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ▷
              @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
            (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)))
| (g ≫ end_.π (diagram V F₁ F₂) i ⊗ₘ
      (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f)) ≫
    eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j)

Tactic:
rw [tensorHom_def_assoc, MonoidalCategory.whiskerRight_id_assoc, assoc,
            enrichedHom_condition' V F₁ F₂ f]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Enriched.FunctorCategory.enrichedHom_condition', CategoryTheory.MonoidalCategory.tensorHom_def_assoc, CategoryTheory.MonoidalCategory.whiskerRight_id_assoc
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
g : tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
i j : J
f : i ⟶ j
rw :
  Iso.hom (ρ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
    g ≫
      end_.π (diagram V F₁ F₂) j ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
          (Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
              (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
            ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ▷
              @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
            (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)))
| (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
        (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
      ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ⊗ₘ
        g ≫ end_.π (diagram V F₁ F₂) j)
      (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)) :
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))

Tactic:
rw [tensorHom_def'_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
            id_whiskerLeft_assoc, id_whiskerLeft_assoc, Iso.inv_hom_id_assoc, unitors_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_equal, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.id_whiskerLeft_assoc, CategoryTheory.MonoidalCategory.tensorHom_def'_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
τ : F₁ ⟶ F₂
⊢ (fun (g : tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) ↦
        ({
            app := fun (j : J) ↦
              (Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ F₁.obj j ⟶[V] F₂.obj j) → F₁.obj j ⟶ F₂.obj j)
                (g ≫ end_.π (diagram V F₁ F₂) j),
            naturality := ⋯ } :
          NatTrans F₁ F₂))
      ((fun (τ : F₁ ⟶ F₂) ↦
          (end_.lift
              (fun (j : J) ↦
                (eHomEquiv V :
                    (a : Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶ F₂.obj j) →
                      𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶[V] F₂.obj j)
                  (τ.app j))
              ⋯ :
            tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂)))
        τ) =
    τ

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
g : tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
⊢ (fun (τ : F₁ ⟶ F₂) ↦
        (end_.lift
            (fun (j : J) ↦
              (eHomEquiv V :
                  (a : Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶ F₂.obj j) →
                    𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶[V] F₂.obj j)
                (τ.app j))
            ⋯ :
          tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂)))
      ((fun (g : tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) ↦
          ({
              app := fun (j : J) ↦
                (Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ F₁.obj j ⟶[V] F₂.obj j) → F₁.obj j ⟶ F₂.obj j)
                  (g ≫ end_.π (diagram V F₁ F₂) j),
              naturality := ⋯ } :
            NatTrans F₁ F₂))
        g) =
    g

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
τ : F₁ ⟶ F₂
j : J
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) τ) (enrichedHomπ V F₁ F₂ j) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj j ⟶ F₂.obj j) → 𝟙_ V ⟶ F₁.obj j ⟶[V] F₂.obj j) (τ.app j) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))

Tactic:
simp [homEquiv]

Premises used: CategoryTheory.Enriched.FunctorCategory.homEquiv
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁
j : J
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₁) (Opposite.op j)) j)
    (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁) (enrichedId V F₁)
      (end_.π (diagram V F₁ F₁) j))
    (eId V (F₁.obj j))

Tactic:
simp [enrichedId]

Premises used: CategoryTheory.Enriched.FunctorCategory.enrichedId
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁)
    ((homEquiv V : (a : F₁ ⟶ F₁) → 𝟙_ V ⟶ enrichedHom V F₁ F₁) (𝟙 F₁) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁)
    (enrichedId V F₁ : tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁)

Tactic:
rfl

Premises used: CategoryTheory.Enriched.FunctorCategory.enrichedId, rfl
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
i j : J
f : i ⟶ j
dsimp :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₃.obj j))
    (((end_.π (diagram V F₁ F₂) i ⊗ₘ end_.π (diagram V F₂ F₃) i) ≫ eComp V (F₁.obj i) (F₂.obj i) (F₃.obj i)) ≫
      eHomWhiskerLeft V (F₁.obj i) (F₃.map f))
    (((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j)) ≫
      eHomWhiskerRight V (F₁.map f) (F₃.obj j))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
      obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op i)) j)
    ((fun (j : J) ↦
          ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
              eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
                (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
              obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) j))
        i ≫
      map (obj (diagram V F₁ F₃) (Opposite.op i)) f)
    ((fun (j : J) ↦
          ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
              eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j) :
            tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
                (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
              obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) j))
        j ≫
      NatTrans.app (map (diagram V F₁ F₃) f.op) j)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    end_.{v₃, v₁, u₃, u₁} (diagram V F₂ F₃) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op i)) j)
    (end_.π (diagram V F₂ F₃) i ≫ map (obj (diagram V F₂ F₃) (Opposite.op i)) f)
    (end_.π (diagram V F₂ F₃) j ≫ NatTrans.app (map (diagram V F₂ F₃) f.op) j)

Tactic:
have := end_.condition (diagram V F₂ F₃) f
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) j)
    (end_.π (diagram V F₁ F₂) i ≫ map (obj (diagram V F₁ F₂) (Opposite.op i)) f)
    (end_.π (diagram V F₁ F₂) j ≫ NatTrans.app (map (diagram V F₁ F₂) f.op) j)

Tactic:
have := end_.condition (diagram V F₁ F₂) f
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
j : J
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃) ⟶
      obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) j)
    (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃) (enrichedComp V F₁ F₂ F₃)
      (end_.π (diagram V F₁ F₃) j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₃.obj j))

Tactic:
simp [enrichedComp]

Premises used: CategoryTheory.Enriched.FunctorCategory.enrichedComp
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
h :
  ∀ (j : J),
    Eq.{v₁ + 1} (α :=
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) j)
      (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₃))
          ((homEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₁ F₃) (f ≫ g)) (end_.π (diagram V F₁ F₃) j) :
        tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) j)
      (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₃))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
            (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
            (CategoryStruct.comp (Y :=
              tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
                (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃))
              ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f ⊗ₘ
                (homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g)
              (enrichedComp V F₁ F₂ F₃)))
          (end_.π (diagram V F₁ F₃) j) :
        tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) j)
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
    ((homEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₁ F₃) (f ≫ g) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
        (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
            (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃))
          ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f ⊗ₘ
            (homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g)
          (enrichedComp V F₁ F₂ F₃)) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) j)
    (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₃))
        ((homEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₁ F₃) (f ≫ g)) (end_.π (diagram V F₁ F₃) j) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) j)
    (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₃))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
          (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
          (CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
              (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃))
            ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f ⊗ₘ
              (homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g)
            (enrichedComp V F₁ F₂ F₃)))
        (end_.π (diagram V F₁ F₃) j) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₃) (Opposite.op j)) j)

Tactic:
simp only [homEquiv_apply_π, NatTrans.comp_app, eHomEquiv_comp, assoc,
    enrichedComp_π, Functor.op_obj, tensorHom_comp_tensorHom_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Enriched.FunctorCategory.homEquiv_apply_π, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc, CategoryTheory.eHomEquiv_comp, CategoryTheory.NatTrans.comp_app, CategoryTheory.Enriched.FunctorCategory.enrichedComp_π, CategoryTheory.Functor.op_obj
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
h :
  ∀ (j : J),
    CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂))
        (Iso.inv (λ_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)) ≫
          CategoryStruct.comp (Y :=
            tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁)
              (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂))
            (enrichedId V F₁ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedComp V F₁ F₁ F₂))
        (end_.π (diagram V F₁ F₂) j) =
      𝟙 (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j
⊢ Iso.inv (λ_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂))
        (enrichedId V F₁ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedComp V F₁ F₁ F₂) =
    𝟙 (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
j : J
h :
  Eq (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j)
    (end_.π (diagram V F₁ F₂) j ≫
      Iso.inv (λ_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j)) ≫
        eId V (F₁.obj j) ▷ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j)
⊢ CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂))
      (Iso.inv (λ_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₁)
            (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂))
          (enrichedId V F₁ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedComp V F₁ F₁ F₂))
      (end_.π (diagram V F₁ F₂) j) =
    𝟙 (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j

Tactic:
rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def, assoc,
    ← comp_whiskerRight_assoc, enrichedId_π, ← whisker_exchange_assoc,
    id_whiskerLeft, assoc, assoc, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_whiskerLeft, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.Enriched.FunctorCategory.enrichedComp_π, CategoryTheory.Enriched.FunctorCategory.enrichedId_π, CategoryTheory.Category.id_comp