-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
lemma functorHomEquiv_comp [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂]
    [HasFunctorEnrichedHom V F₂ F₃] [HasEnrichedHom V F₂ F₃]
    [HasFunctorEnrichedHom V F₁ F₃] [HasEnrichedHom V F₁ F₃]
    (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) :
    (functorHomEquiv V) (f ≫ g) = (λ_ (𝟙_ (J ⥤ V))).inv ≫
      ((functorHomEquiv V) f ⊗ (functorHomEquiv V) g) ≫ 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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
⊢ (functorHomEquiv V) (f ≫ g) =
    (λ_ (𝟙_ (J ⥤ V))).inv ≫ ((functorHomEquiv V) f ⊗ (functorHomEquiv V) g) ≫ 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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ ((functorHomEquiv V) (f ≫ g)).app j =
    ((λ_ (𝟙_ (J ⥤ V))).inv ≫ ((functorHomEquiv V) f ⊗ (functorHomEquiv V) g) ≫ 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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ (homEquiv V) (f ≫ g) ≫ precompEnrichedHom V F₁ F₃ (Under.forget j) =
    (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗
          (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
        enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)

Tactic:
ext k

Result:
case w.h.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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ ((homEquiv V) (f ≫ g) ≫ precompEnrichedHom V F₁ F₃ (Under.forget j)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k =
    ((λ_ (𝟙_ V)).inv ≫
        ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗
            (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
          enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k

Proof state:
case w.h.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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ ((homEquiv V) (f ≫ g) ≫ precompEnrichedHom V F₁ F₃ (Under.forget j)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k =
    ((λ_ (𝟙_ V)).inv ≫
        ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗
            (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
          enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) ≫
      end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) k

Tactic:
rw [homEquiv_comp, assoc, assoc, assoc, assoc, assoc, end_.lift_π, enrichedComp_π]

Result:
case w.h.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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ⊗ (homEquiv V) g) ≫
        enrichedComp V F₁ F₂ F₃ ≫
          enrichedHomπ V F₁ F₃ ((Under.forget j).obj k) ≫
            eHomWhiskerRight V ((Iso.refl (Under.forget j ⋙ F₁)).inv.app k) (F₃.obj ((Under.forget j).obj k)) ≫
              eHomWhiskerLeft V ((Under.forget j ⋙ F₁).obj k) ((Iso.refl (Under.forget j ⋙ F₃)).hom.app k) =
    (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗
          (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
        (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k ⊗
            end_.π (diagram V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) k) ≫
          eComp V (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₂).obj k)
            ((Under.forget j ⋙ F₃).obj k)

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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ ((functorHomEquiv V) (f ≫ g)).app j =
    ((λ_ (𝟙_ (J ⥤ V))).inv ≫ ((functorHomEquiv V) f ⊗ (functorHomEquiv V) g) ≫ 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₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
⊢ (homEquiv V) (f ≫ g) ≫ precompEnrichedHom V F₁ F₃ (Under.forget j) =
    (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗
          (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
        enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)