-- 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:
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₃'
⊢ { app := fun j => end_.lift (fun k => F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯, naturality := ⋯ } =
    { 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₃'

Tactic:
ext j

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
⊢ { 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

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
⊢ 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₃')

Tactic:
ext k

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
⊢ 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

Proof state:
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₃'
⊢ homEquiv (f ≫ f₃) =
    homEquiv f ≫
      (ρ_ (functorEnrichedHom C F₁ F₃)).inv ≫
        functorEnrichedHom C F₁ F₃ ◁ (functorHomEquiv C) f₃ ≫ functorEnrichedComp C F₁ F₃ F₃'

Tactic:
dsimp [homEquiv]

Result:
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₃'
⊢ { app := fun j => end_.lift (fun k => F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right)) ⋯, naturality := ⋯ } =
    { 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₃'

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) ≫
        (ρ_ (((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)

Tactic:
dsimp

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) ≫
        (ρ_ ((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)