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
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.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j ≫
      Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))) ≫
        eId V (F₁.obj j) ▷ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ≫
          eComp V (F₁.obj j) (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j)
⊢ 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)

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
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.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j ≫ 𝟙 (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
    (end_.π (diagram V F₁ F₂) j)
h₁ h₂ :
  Eq.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j) (end_.π (diagram V F₁ F₂) j)
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j ≫
      Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))) ≫
        eId V (F₁.obj j) ▷ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ≫
          eComp V (F₁.obj j) (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j)

Tactic:
rw [e_id_comp, comp_id]

Premises used: CategoryTheory.e_id_comp, CategoryTheory.Category.comp_id
-- 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₂))
            (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedId V 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₂))
        (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedId V 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)) ≫
        obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j ◁ eId V (F₂.obj 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₂))
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedId V 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,
    ← MonoidalCategory.whiskerLeft_comp_assoc, enrichedId_π,
    whisker_exchange_assoc, MonoidalCategory.whiskerRight_id, assoc, assoc,
    Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.tensorHom_def', CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.whiskerRight_id, CategoryTheory.Enriched.FunctorCategory.enrichedComp_π, CategoryTheory.Enriched.FunctorCategory.enrichedId_π, CategoryTheory.Category.id_comp
-- 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.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j ≫
      Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))) ≫
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁ eId V (F₂.obj j) ≫
          eComp V (F₁.obj j) (F₂.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j)
⊢ 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)) ≫
        obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j ◁ eId V (F₂.obj j) ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) 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
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.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j ≫ 𝟙 (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
    (end_.π (diagram V F₁ F₂) j)
h₁ h₂ :
  Eq.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j) (end_.π (diagram V F₁ F₂) j)
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j ≫
      Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))) ≫
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁ eId V (F₂.obj j) ≫
          eComp V (F₁.obj j) (F₂.obj j) (F₂.obj j))
    (end_.π (diagram V F₁ F₂) j)

Tactic:
rw [e_comp_id, comp_id]

Premises used: CategoryTheory.e_comp_id, CategoryTheory.Category.comp_id
-- 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₃ 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₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
h :
  ∀ (j : J),
    Eq (α :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
          (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 := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₄))
        (Iso.inv
            (α_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
              (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₄))
            (enrichedComp V F₁ F₂ F₃ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄) (enrichedComp V F₁ F₃ F₄))
        (end_.π (diagram V F₁ F₄) j))
      (CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram 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₄))
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄) (enrichedComp V F₁ F₂ F₄))
        (end_.π (diagram V F₁ F₄) j))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄)) ⟶
      enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄)
    (Iso.inv
        (α_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (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₄))
        (enrichedComp V F₁ F₂ F₃ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄) (enrichedComp V F₁ 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₄))
      (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄) (enrichedComp V F₁ 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₃ 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₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
j : J
rw :
  (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
    Iso.inv
        (α_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j)
          (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) 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) ▷
          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)
| CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₄))
    (Iso.inv
        (α_ (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
          (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₄))
        (enrichedComp V F₁ F₂ F₃ ▷ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄) (enrichedComp V F₁ F₃ F₄))
    (end_.π (diagram V F₁ F₄) j)

Tactic:
rw [assoc, assoc, enrichedComp_π,
      tensorHom_def_assoc, ← comp_whiskerRight_assoc, enrichedComp_π,
      comp_whiskerRight_assoc, ← whisker_exchange_assoc,
      ← whisker_exchange_assoc, ← tensorHom_def'_assoc, ← associator_inv_naturality_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.tensorHom_def'_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.MonoidalCategory.tensorHom_def_assoc, CategoryTheory.MonoidalCategory.associator_inv_naturality_assoc, 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₃ 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₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
j : J
rw :
  (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) 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) ≫
      eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj j)
| CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram 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₄))
      (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ◁ enrichedComp V F₂ F₃ F₄) (enrichedComp V F₁ F₂ F₄))
    (end_.π (diagram V F₁ F₄) j)

Tactic:
rw [assoc, enrichedComp_π, tensorHom_def'_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc,
      enrichedComp_π, MonoidalCategory.whiskerLeft_comp_assoc, whisker_exchange_assoc,
      whisker_exchange_assoc, ← tensorHom_def_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.tensorHom_def'_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.tensorHom_def_assoc, 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₃ 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₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
j : J
h :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (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 j) (F₄.obj j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      Iso.inv
          (α_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj j) (F₄.obj j))) ≫
        eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ▷
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj j) (F₄.obj j) ≫
          eComp V (F₁.obj j) (F₃.obj j) (F₄.obj j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁
          eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫
        eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (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)
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      Iso.inv
          (α_ (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j)
            (obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₂ F₃) (Opposite.op j)) 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) ▷
            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 ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) 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) ≫
        eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₂.obj j) (F₄.obj 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
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ 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₄
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
j : J
h h₁ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (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 j) (F₄.obj j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁
          eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫
        eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁
          eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫
        eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
        (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 j) (F₄.obj j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      Iso.inv
          (α_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj j) (F₃.obj j))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj j) (F₄.obj j))) ≫
        eComp V (F₁.obj j) (F₂.obj j) (F₃.obj j) ▷
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₃.obj j) (F₄.obj j) ≫
          eComp V (F₁.obj j) (F₃.obj j) (F₄.obj j))
    ((end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j ⊗ₘ end_.π (diagram V F₃ F₄) j) ≫
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j) ◁
          eComp V (F₂.obj j) (F₃.obj j) (F₄.obj j) ≫
        eComp V (F₁.obj j) (F₂.obj j) (F₄.obj j))

Tactic:
rw [e_assoc]

Premises used: CategoryTheory.e_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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
j j' : J
f : j ⟶ j'
⊢ HasEnrichedHom V (Under.map f ⋙ Under.forget j ⋙ F₁) (Under.map f ⋙ Under.forget j ⋙ F₂)

Tactic:
inferInstanceAs (HasEnrichedHom V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂))

Premises used: _private.0.CategoryTheory.Enriched.FunctorCategory.instHasEnrichedHomUnderCompMapForget._proof_1