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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j j' : J
f : j ⟶ j'
this :
  Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
      (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
        enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j)))
            ((Under.forget j ⋙ F₂).obj (Under.mk (𝟙 j))))
      (eHomWhiskerLeft V (F₁.obj j) (F₂.map f)))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) :
        enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ⟶
          @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget j ⋙ F₁).obj (Under.mk f))
            ((Under.forget j ⋙ F₂).obj (Under.mk f)))
      (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
⊢ Under.mk f = { left := Comma.left.{0, v₃, v₃, 0, u₃, u₃} (Under.mk (𝟙 j')), right := j', hom := f }

Tactic:
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
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
dsimp :
  CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
      (precompEnrichedHom V F₁ F₂ (Under.forget j)) =
    s.π.app j
⊢ CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
      (NatTrans.app (Cone.π (coneFunctorEnrichedHom V F₁ F₂)) j) =
    s.π.app j

Tactic:
dsimp [coneFunctorEnrichedHom]

Premises used: CategoryTheory.Enriched.FunctorCategory.coneFunctorEnrichedHom
-- 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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
h :
  ∀ (k : Under.{v₃, u₃} j),
    CategoryStruct.comp (Y := end_ (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)))
        (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
          (precompEnrichedHom V F₁ F₂ (Under.forget j)))
        (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k) =
      s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k
⊢ CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
      (precompEnrichedHom V F₁ F₂ (Under.forget j)) =
    s.π.app j

Tactic:
ext k
-- 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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
k : Under.{v₃, u₃} j
⊢ s.π.app j ≫ map (functorEnrichedHom V F₁ F₂) k.hom = s.π.app k.right

Tactic:
have := s.w k.hom
-- 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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
k : Under.{v₃, u₃} j
this :
  Eq (α := s.pt ⟶ enrichedHom V (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₂))
    (s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)))
    (s.π.app k.right)
h :
  s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map k.hom).obj (Under.mk (𝟙 k.right))) =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k
⊢ CategoryStruct.comp (Y := end_ (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)))
      (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂) (lift s)
        (precompEnrichedHom V F₁ F₂ (Under.forget j)))
      (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k) =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k

Tactic:
simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, lift, functorEnrichedHom_obj,
    assoc, end_.lift_π, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
    eHomWhiskerLeft_id, comp_id, ← this, Under.map_obj_right, Under.mk_right]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Under.map_obj_right, CategoryTheory.Category.comp_id, CategoryTheory.eHomWhiskerLeft_id, CategoryTheory.Iso.refl_inv, CategoryTheory.Under.mk_right, CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_obj, CategoryTheory.eHomWhiskerRight_id, CategoryTheory.Limits.end_.lift_π, CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.lift, CategoryTheory.Under.forget_obj, CategoryTheory.NatTrans.id_app, CategoryTheory.Iso.refl_hom, CategoryTheory.Enriched.FunctorCategory.diagram_obj_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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
k : Under.{v₃, u₃} j
this :
  Eq (α := s.pt ⟶ enrichedHom V (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₂))
    (s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)))
    (s.π.app k.right)
h : (Under.map k.hom).obj (Under.mk (𝟙 k.right)) = k
⊢ s.π.app j ≫
      enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ((Under.map k.hom).obj (Under.mk (𝟙 k.right))) =
    s.π.app j ≫ end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k

Tactic:
congr
-- 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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
k : Under.{v₃, u₃} j
this :
  Eq (α := s.pt ⟶ enrichedHom V (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₂))
    (s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)))
    (s.π.app k.right)
h :
  { left := Comma.left.{0, v₃, v₃, 0, u₃, u₃} (Under.mk (𝟙 k.right)), right := k.right, hom := k.hom :
      Comma.{0, v₃, v₃, 0, u₃, u₃} (fromPUnit j) (𝟭 J) } =
    k
⊢ (Under.map k.hom).obj (Under.mk (𝟙 k.right)) = k

Tactic:
simp [Under.map, Comma.mapLeft]

Premises used: CategoryTheory.Comma.mapLeft, CategoryTheory.Under.map
-- 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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
j : J
k : Under.{v₃, u₃} j
this :
  Eq (α := s.pt ⟶ enrichedHom V (Under.forget k.right ⋙ F₁) (Under.forget k.right ⋙ F₂))
    (s.π.app j ≫
      precompEnrichedHom' V (Under.map k.hom) (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map k.hom ⋙ Under.forget j ⋙ F₂)))
    (s.π.app k.right)
⊢ { left := Comma.left.{0, v₃, v₃, 0, u₃, u₃} (Under.mk (𝟙 k.right)), right := k.right, hom := k.hom :
      Comma.{0, v₃, v₃, 0, u₃, u₃} (fromPUnit j) (𝟭 J) } =
    k

Tactic:
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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
m : s.pt ⟶ Cone.pt.{v₃, v₁, u₃, u₁} (F := functorEnrichedHom V F₁ F₂) (coneFunctorEnrichedHom V F₁ F₂)
hm : ∀ (j : J), m ≫ NatTrans.app (Cone.π (coneFunctorEnrichedHom V F₁ F₂)) j = s.π.app j
dsimp : m = lift s
⊢ m = lift s

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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
m : s.pt ⟶ Cone.pt.{v₃, v₁, u₃, u₁} (F := functorEnrichedHom V F₁ F₂) (coneFunctorEnrichedHom V F₁ F₂)
hm : ∀ (j : J), m ≫ NatTrans.app (Cone.π (coneFunctorEnrichedHom V F₁ F₂)) j = s.π.app j
h :
  ∀ (j : J),
    m ≫ end_.π (diagram V F₁ F₂) j =
      CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂)) (lift s) (end_.π (diagram V F₁ F₂) j)
⊢ m = lift s

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
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₂
inst_7 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
s : Cone.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₂)
m : s.pt ⟶ Cone.pt.{v₃, v₁, u₃, u₁} (F := functorEnrichedHom V F₁ F₂) (coneFunctorEnrichedHom V F₁ F₂)
hm : ∀ (j : J), m ≫ NatTrans.app (Cone.π (coneFunctorEnrichedHom V F₁ F₂)) j = s.π.app j
j : J
⊢ m ≫ end_.π (diagram V F₁ F₂) j =
    CategoryStruct.comp (Y := end_.{v₃, v₁, u₃, u₁} (diagram V F₁ F₂)) (lift s) (end_.π (diagram V F₁ F₂) j)

Tactic:
simpa using ((hm j).trans (fac s j).symm) =≫ enrichedHomπ V _ _ (Under.mk (𝟙 j))

Premises used: CategoryTheory.Enriched.FunctorCategory.isLimitConeFunctorEnrichedHom.fac, CategoryTheory.Enriched.FunctorCategory.enrichedHomπ, CategoryTheory.Under.mk, CategoryTheory.CategoryStruct.id, Eq.symm, Eq.trans
-- 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₂
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
j j' : J
f : j ⟶ j'
dsimp :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
        (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ⟶
      enrichedHom V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂))
        (enrichedHom V (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)))
      (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)) ⊗ₘ
        precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)))
      (enrichedComp V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)))
    (CategoryStruct.comp (Y := enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
      (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
      (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
        (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃))))
⊢ Eq.{v₁ + 1} (α :=
    obj.{v₃, v₁, u₃, u₁} (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃)) j ⟶
      obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₃) j')
    (map (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃)) f ≫
      enrichedComp V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃))
    (CategoryStruct.comp (Y := obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₃) j)
      (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
      (map (functorEnrichedHom V F₁ F₃) f))

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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
j j' : J
f : j ⟶ j'
k : Under.{v₃, u₃} j'
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
        (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj k.right) (F₃.obj k.right))
    ((CategoryStruct.comp (Y := enrichedHom V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂))
          (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂)))
          (end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂)) k) ⊗ₘ
        CategoryStruct.comp (Y := enrichedHom V (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃))
          (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₂))
            (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)))
          (end_.π (diagram V (Under.forget j' ⋙ F₂) (Under.forget j' ⋙ F₃)) k)) ≫
      eComp V (F₁.obj k.right) (F₂.obj k.right) (F₃.obj k.right))
    (CategoryStruct.comp (Y := enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
      (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
      (CategoryStruct.comp (Y := end_ (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)))
        (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget j ⋙ F₃)))
        (end_.π (diagram V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₃)) k)))

Tactic:
simp
-- 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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
inst_8 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
w :
  ∀ (j : J),
    Eq.{v₁ + 1} (α :=
      obj.{v₃, v₁, u₃, u₁}
          (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂)
            (tensorObj (𝒞 := category) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)))
          j ⟶
        obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₄) j)
      (NatTrans.app
        (Iso.inv (α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)) ≫
          CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₃) (functorEnrichedHom V F₃ F₄))
            (functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄) (functorEnrichedComp V F₁ F₃ F₄))
        j)
      (NatTrans.app
        (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₄))
          (functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄) (functorEnrichedComp V F₁ F₂ F₄))
        j)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₃, v₁, u₃, u₁} J V)
      (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂)
        (tensorObj (𝒞 := category) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)))
      (functorEnrichedHom V F₁ F₄))
    (Iso.inv (α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)) ≫
      CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₃) (functorEnrichedHom V F₃ F₄))
        (functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄) (functorEnrichedComp V F₁ F₃ F₄))
    (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₄))
      (functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄) (functorEnrichedComp 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 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₃ F₄
inst_8 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₄
inst_10 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₄
j : J
w :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
        (tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
          (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))) ⟶
      enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₄))
    (Iso.inv
        (α_ (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
          (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
          (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
          (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄)))
        (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ▷
          enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))
        (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄)))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
        (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)))
      (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ◁
        enrichedComp V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))
      (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)))
⊢ Eq.{v₁ + 1} (α :=
    obj.{v₃, v₁, u₃, u₁}
        (tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂)
          (tensorObj (𝒞 := category) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)))
        j ⟶
      obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₄) j)
    (NatTrans.app
      (Iso.inv (α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)) ≫
        CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₃) (functorEnrichedHom V F₃ F₄))
          (functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄) (functorEnrichedComp V F₁ F₃ F₄))
      j)
    (NatTrans.app
      (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₄))
        (functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄) (functorEnrichedComp V F₁ F₂ F₄))
      j)

Tactic:
dsimp