-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
@[reassoc]
lemma functorEnriched_assoc [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₂ F₃]
    [HasFunctorEnrichedHom V F₃ F₄] [HasFunctorEnrichedHom V F₁ F₃]
    [HasFunctorEnrichedHom V F₂ F₄] [HasFunctorEnrichedHom V F₁ F₄] :
    (α_ _ _ _).inv ≫ functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄ ≫
      functorEnrichedComp V F₁ F₃ F₄ =
        functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄ ≫
          functorEnrichedComp V F₁ F₂ F₄

Proof state:
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasFunctorEnrichedHom V F₂ F₃
inst✝³ : HasFunctorEnrichedHom V F₃ F₄
inst✝² : HasFunctorEnrichedHom V F₁ F₃
inst✝¹ : HasFunctorEnrichedHom V F₂ F₄
inst✝ : HasFunctorEnrichedHom V F₁ F₄
⊢ (α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)).inv ≫
      functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄ ≫ functorEnrichedComp V F₁ F₃ F₄ =
    functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄ ≫ functorEnrichedComp V F₁ F₂ F₄

Tactic:
ext j

Result:
case w.h
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasFunctorEnrichedHom V F₂ F₃
inst✝³ : HasFunctorEnrichedHom V F₃ F₄
inst✝² : HasFunctorEnrichedHom V F₁ F₃
inst✝¹ : HasFunctorEnrichedHom V F₂ F₄
inst✝ : HasFunctorEnrichedHom V F₁ F₄
j : J
⊢ ((α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)).inv ≫
          functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄ ≫ functorEnrichedComp V F₁ F₃ F₄).app
      j =
    (functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄ ≫ functorEnrichedComp V F₁ F₂ F₄).app j

Proof state:
case w.h
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasFunctorEnrichedHom V F₂ F₃
inst✝³ : HasFunctorEnrichedHom V F₃ F₄
inst✝² : HasFunctorEnrichedHom V F₁ F₃
inst✝¹ : HasFunctorEnrichedHom V F₂ F₄
inst✝ : HasFunctorEnrichedHom V F₁ F₄
j : J
⊢ (α_ (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
          (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
          (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))).inv ≫
      enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ▷
          enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄) ≫
        enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄) =
    enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ◁
        enrichedComp V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄) ≫
      enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)

Tactic:
rw [enriched_assoc]

Result:
no goals

Proof state:
case w.h
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasFunctorEnrichedHom V F₂ F₃
inst✝³ : HasFunctorEnrichedHom V F₃ F₄
inst✝² : HasFunctorEnrichedHom V F₁ F₃
inst✝¹ : HasFunctorEnrichedHom V F₂ F₄
inst✝ : HasFunctorEnrichedHom V F₁ F₄
j : J
⊢ ((α_ (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃) (functorEnrichedHom V F₃ F₄)).inv ≫
          functorEnrichedComp V F₁ F₂ F₃ ▷ functorEnrichedHom V F₃ F₄ ≫ functorEnrichedComp V F₁ F₃ F₄).app
      j =
    (functorEnrichedHom V F₁ F₂ ◁ functorEnrichedComp V F₂ F₃ F₄ ≫ functorEnrichedComp V F₁ F₂ F₄).app j

Tactic:
dsimp

Result:
case w.h
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ F₄ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasFunctorEnrichedHom V F₂ F₃
inst✝³ : HasFunctorEnrichedHom V F₃ F₄
inst✝² : HasFunctorEnrichedHom V F₁ F₃
inst✝¹ : HasFunctorEnrichedHom V F₂ F₄
inst✝ : HasFunctorEnrichedHom V F₁ F₄
j : J
⊢ (α_ (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
          (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))
          (enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄))).inv ≫
      enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) ▷
          enrichedHom V (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄) ≫
        enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄) =
    enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) ◁
        enrichedComp V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₄) ≫
      enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₄)