-- Mathlib/CategoryTheory/Closed/FunctorCategory/Basic.lean
lemma homEquiv_naturality_three [∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂]
    (f : F₁ ⊗ F₂ ⟶ F₃) (f₃ : F₃ ⟶ F₃') :
    homEquiv (f ≫ f₃) = homEquiv f ≫ (ρ_ _).inv ≫ _ ◁ functorHomEquiv _ f₃ ≫
      functorEnrichedComp C F₁ F₃ F₃'

Proof state:
case w.h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
⊢ { app := fun j => end_.lift (fun k => F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯, naturality := ⋯ }.app
      j =
    ({ app := fun j => end_.lift (fun k => F₂.map k.hom ≫ curry (f.app k.right)) ⋯, naturality := ⋯ } ≫
          (ρ_ (functorEnrichedHom C F₁ F₃)).inv ≫
            functorEnrichedHom C F₁ F₃ ◁ (functorHomEquiv C) f₃ ≫ functorEnrichedComp C F₁ F₃ F₃').app
      j

Tactic:
dsimp

Result:
case w.h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
⊢ end_.lift (fun k => F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯ =
    end_.lift (fun k => F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
      (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))).inv ≫
        enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
            ((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
          enrichedComp C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')

Proof state:
case w.h.h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
          (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁
              ((Enriched.FunctorCategory.homEquiv C) f₃ ≫
                enrichedHomπ C F₃ F₃' k.right ≫
                  (pre (𝟙 (F₃.obj k.right))).app (F₃'.obj k.right) ≫
                    (ihom (F₃.obj k.right)).map (𝟙 (F₃'.obj k.right))) ≫
            eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)

Tactic:
rw [pre_id, NatTrans.id_app, Functor.map_id, Category.comp_id,
  Category.comp_id, homEquiv_apply_π, curry_natural_right]

Result:
case w.h.h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right) ≫ (ihom (F₁.obj k.right)).map (f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
          (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁ (eHomEquiv C) (f₃.app k.right) ≫
            eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)

Proof state:
case w.h.h.e_a.e_a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
      (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁ (eHomEquiv C) (f₃.app k.right) ≫
        eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right) =
    (ihom (F₁.obj k.right)).map (f₃.app k.right)

Tactic:
apply enrichedOrdinaryCategorySelf_eHomWhiskerLeft

Result:
no goals

Proof state:
case w.h.h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ end_.lift (fun k => F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯ ≫
      end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) k =
    (end_.lift (fun k => F₂.map k.hom ≫ curry (f.app k.right)) ⋯ ≫
        (ρ_ (enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))).inv ≫
          enrichedHom C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ◁
              ((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
            enrichedComp C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) ≫
      end_.π (diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃')) k

Tactic:
rw [Category.assoc, Category.assoc, Category.assoc, end_.lift_π, enrichedComp_π,
  tensorHom_def, Category.assoc, whisker_exchange_assoc, whiskerRight_id_assoc,
  Iso.inv_hom_id_assoc, end_.lift_π_assoc, Category.assoc,
  ← MonoidalCategory.whiskerLeft_comp_assoc, Category.assoc, end_.lift_π,
  enrichedOrdinaryCategorySelf_eHomWhiskerRight,
  enrichedOrdinaryCategorySelf_eHomWhiskerLeft]

Result:
case w.h.h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        (ρ_ (((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k)).inv ≫
          ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
              ((Enriched.FunctorCategory.homEquiv C) f₃ ≫
                enrichedHomπ C F₃ F₃' ((Under.forget j).obj k) ≫
                  (pre ((Iso.refl (Under.forget j ⋙ F₃)).inv.app k)).app (F₃'.obj ((Under.forget j).obj k)) ≫
                    (ihom ((Under.forget j ⋙ F₃).obj k)).map ((Iso.refl (Under.forget j ⋙ F₃')).hom.app k)) ≫
            eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
              ((Under.forget j ⋙ F₃').obj k)