-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
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')))
⊢ 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')))
have 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 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: rw [this]