-- 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'
simp :
  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 ≫
      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')))
⊢ 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')))

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

Premises used: CategoryTheory.Functor.comp_obj, 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.Under.forget_obj, CategoryTheory.NatTrans.id_app, CategoryTheory.Iso.refl_hom, CategoryTheory.Limits.end_.lift_π_assoc, CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom_map, CategoryTheory.Enriched.FunctorCategory.diagram_obj_obj