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₂
X : J
h :
  ∀ (j : Under.{v₃, u₃} X),
    CategoryStruct.comp (Y := end_ (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)))
        (precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
          (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)))
        (end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j) =
      𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) ≫
        end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j
⊢ precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
      (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)) =
    𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ 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
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₂
X : J
j : Under.{v₃, u₃} X
h :
  Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j.right) (F₂.obj j.right))
    (enrichedHomπ V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) (obj (Under.map (𝟙 X)) j))
    (end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j)
⊢ CategoryStruct.comp (Y := end_ (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)))
      (precompEnrichedHom' V (Under.map (𝟙 X)) (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₁))
        (Iso.refl (Under.map (𝟙 X) ⋙ Under.forget X ⋙ F₂)))
      (end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j) =
    𝟙 (enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) ≫
      end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j

Tactic:
simp only [diagram_obj_obj, Functor.comp_obj, Under.forget_obj, end_.lift_π,
      Under.map_obj_right, Iso.refl_inv, NatTrans.id_app, eHomWhiskerRight_id, Iso.refl_hom,
      eHomWhiskerLeft_id, comp_id, id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Under.map_obj_right, CategoryTheory.Category.comp_id, CategoryTheory.eHomWhiskerLeft_id, CategoryTheory.Iso.refl_inv, CategoryTheory.eHomWhiskerRight_id, CategoryTheory.Limits.end_.lift_π, CategoryTheory.Under.forget_obj, CategoryTheory.NatTrans.id_app, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp, 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
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₂
X : J
j : Under.{v₃, u₃} X
h : obj (Under.map (𝟙 X)) j = j
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j.right) (F₂.obj j.right))
    (enrichedHomπ V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) (obj (Under.map (𝟙 X)) j))
    (end_.π (diagram V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂)) j)

Tactic:
congr 1
-- 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₂
X : J
j : Under.{v₃, u₃} X
h : { left := j.left, right := j.right, hom := j.hom : Comma.{0, v₃, v₃, 0, u₃, u₃} (fromPUnit X) (𝟭 J) } = j
⊢ obj (Under.map (𝟙 X)) j = j

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
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₂
X : J
j : Under.{v₃, u₃} X
⊢ { left := j.left, right := j.right, hom := j.hom : Comma.{0, v₃, v₃, 0, u₃, u₃} (fromPUnit X) (𝟭 J) } = j

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₂
X Y Z : J
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (j : Under.{v₃, u₃} Z),
    Eq.{v₁ + 1} (α :=
      enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
        obj (obj (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) (Opposite.op j)) j)
      (CategoryStruct.comp (Y := end_ (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)))
        (precompEnrichedHom' V (Under.map (f ≫ g)) (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₁))
          (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₂)))
        (end_.π (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) j))
      (CategoryStruct.comp (Y := end_ (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)))
        (CategoryStruct.comp (Y := enrichedHom V (Under.forget Y ⋙ F₁) (Under.forget Y ⋙ F₂))
          (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₁))
            (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₂)))
          (precompEnrichedHom' V (Under.map g) (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₁))
            (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₂))))
        (end_.π (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) j))
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
      enrichedHom V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂))
    (precompEnrichedHom' V (Under.map (f ≫ g)) (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₁))
      (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₂)))
    (CategoryStruct.comp (Y := enrichedHom V (Under.forget Y ⋙ F₁) (Under.forget Y ⋙ F₂))
      (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₁))
        (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₂)))
      (precompEnrichedHom' V (Under.map g) (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₁))
        (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ 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
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₂
X Y Z : J
f : X ⟶ Y
g : Y ⟶ Z
j : Under.{v₃, u₃} Z
h :
  Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j.right) (F₂.obj j.right))
    (enrichedHomπ V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ((Under.map (f ≫ g)).obj j) :
      enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget X ⋙ F₁).obj ((Under.map (f ≫ g)).obj j))
          ((Under.forget X ⋙ F₂).obj ((Under.map (f ≫ g)).obj j)))
    (enrichedHomπ V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ((Under.map f).obj ((Under.map g).obj j)))
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
      obj (obj (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) (Opposite.op j)) j)
    (CategoryStruct.comp (Y := end_ (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)))
      (precompEnrichedHom' V (Under.map (f ≫ g)) (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₁))
        (Iso.refl (Under.map (f ≫ g) ⋙ Under.forget X ⋙ F₂)))
      (end_.π (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) j))
    (CategoryStruct.comp (Y := end_ (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)))
      (CategoryStruct.comp (Y := enrichedHom V (Under.forget Y ⋙ F₁) (Under.forget Y ⋙ F₂))
        (precompEnrichedHom' V (Under.map f) (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₁))
          (Iso.refl (Under.map f ⋙ Under.forget X ⋙ F₂)))
        (precompEnrichedHom' V (Under.map g) (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₁))
          (Iso.refl (Under.map g ⋙ Under.forget Y ⋙ F₂))))
      (end_.π (diagram V (Under.forget Z ⋙ F₁) (Under.forget Z ⋙ F₂)) j))

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

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.eHomWhiskerRight_id, CategoryTheory.Limits.end_.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
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₂
X Y Z : J
f : X ⟶ Y
g : Y ⟶ Z
j : Under.{v₃, u₃} Z
h : (Under.map (f ≫ g)).obj j = (Under.map f).obj ((Under.map g).obj j)
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j.right) (F₂.obj j.right))
    (enrichedHomπ V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ((Under.map (f ≫ g)).obj j) :
      enrichedHom V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ ((Under.forget X ⋙ F₁).obj ((Under.map (f ≫ g)).obj j))
          ((Under.forget X ⋙ F₂).obj ((Under.map (f ≫ g)).obj j)))
    (enrichedHomπ V (Under.forget X ⋙ F₁) (Under.forget X ⋙ F₂) ((Under.map f).obj ((Under.map g).obj j)))

Tactic:
congr 1
-- 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₂
X Y Z : J
f : X ⟶ Y
g : Y ⟶ Z
j : Under.{v₃, u₃} Z
⊢ (Under.map (f ≫ g)).obj j = (Under.map f).obj ((Under.map g).obj j)

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
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'
dsimp :
  Eq (α := s.pt ⟶ @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))
      (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
        s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
      (eHomWhiskerLeft V (F₁.obj j) (F₂.map f) :
        Quiver.Hom.{v₁, u₁} (V := V) (@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'))))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (s.π.app j' ≫ enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j')) :
        s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (eHomWhiskerRight V (F₁.map f) (F₂.obj j') :
        Quiver.Hom.{v₁, u₁} (V := V) (@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'))))
⊢ Eq.{v₁ + 1} (α := s.pt ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j')
    ((fun (j : J) ↦
          (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
            s.pt ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op j)) j))
        j ≫
      map (obj (diagram V F₁ F₂) (Opposite.op j)) f)
    ((fun (j : J) ↦
          (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
            s.pt ⟶ 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 : 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'
rw :
  Eq (α := s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
    (s.π.app 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)))
    (s.π.app j ≫
      map (functorEnrichedHom V F₁ F₂) 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 (𝟙 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'))))
          (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))
⊢ Eq (α := s.pt ⟶ @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))
      (s.π.app j ≫ enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) :
        s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
      (eHomWhiskerLeft V (F₁.obj j) (F₂.map f) :
        Quiver.Hom.{v₁, u₁} (V := V) (@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'))))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (s.π.app j' ≫ enrichedHomπ V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂) (Under.mk (𝟙 j')) :
        s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j') (F₂.obj j'))
      (eHomWhiskerRight V (F₁.map f) (F₂.obj j') :
        Quiver.Hom.{v₁, u₁} (V := V) (@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'))))

Tactic:
rw [← s.w f, assoc, assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.w
-- 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'
⊢ Eq.{v₁ + 1} (α :=
    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 f)))
    (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk (𝟙 j)) ≫
      eHomWhiskerLeft V ((Under.forget j ⋙ F₁).obj (Under.mk (𝟙 j))) ((Under.forget j ⋙ F₂).map (Under.homMk f ⋯)))
    (enrichedHomπ V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.mk f) ≫
      eHomWhiskerRight V ((Under.forget j ⋙ F₁).map (Under.homMk f ⋯)) ((Under.forget j ⋙ F₂).obj (Under.mk f)))

Tactic:
have := enrichedHom_condition V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)
      (Under.homMk f : Under.mk (𝟙 j) ⟶ Under.mk 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 : 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')))
e_a : Under.mk f = (Under.map f).obj (Under.mk (𝟙 j'))
⊢ Eq (α := s.pt ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j'))
    (s.π.app 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 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')))
    (s.π.app 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.map f).obj (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.map f).obj (Under.mk (𝟙 j'))))
              ((Under.forget j ⋙ F₂).obj ((Under.map f).obj (Under.mk (𝟙 j')))))
        (eHomWhiskerRight V (F₁.map f) (F₂.obj j')))

Tactic:
congr 3
-- 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')))
e_a : Under.mk f = { left := Comma.left.{0, v₃, v₃, 0, u₃, u₃} (Under.mk (𝟙 j')), right := j', hom := f }
⊢ Under.mk f = (Under.map f).obj (Under.mk (𝟙 j'))

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

Premises used: CategoryTheory.Comma.mapLeft, CategoryTheory.Under.map