-- Mathlib/CategoryTheory/Closed/FunctorCategory/Basic.lean
lemma homEquiv_naturality_two_symm (f₂ : F₂ ⟶ F₂') (g : F₂' ⟶ functorEnrichedHom C F₁ F₃) :
    homEquiv.symm (f₂ ≫ g) = F₁ ◁ f₂ ≫ homEquiv.symm g

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
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
⊢ homEquiv.symm (f₂ ≫ g) = F₁ ◁ f₂ ≫ homEquiv.symm g

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
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
⊢ {
      app := fun j =>
        uncurry ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
      naturality := ⋯ } =
    F₁ ◁ f₂ ≫
      { app := fun j => uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
        naturality := ⋯ }

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
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
j : J
⊢ {
          app := fun j =>
            uncurry
              ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
          naturality := ⋯ }.app
      j =
    (F₁ ◁ f₂ ≫
          {
            app := fun j =>
              uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
            naturality := ⋯ }).app
      j

Tactic:
simp [← uncurry_natural_left]

Result:
no goals

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
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
⊢ {
      app := fun j =>
        uncurry ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
      naturality := ⋯ } =
    F₁ ◁ f₂ ≫
      { app := fun j => uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
        naturality := ⋯ }

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
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
j : J
⊢ {
          app := fun j =>
            uncurry
              ((f₂.app j ≫ g.app j) ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
          naturality := ⋯ }.app
      j =
    (F₁ ◁ f₂ ≫
          {
            app := fun j =>
              uncurry (g.app j ≫ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j))),
            naturality := ⋯ }).app
      j