-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma enriched_id_comp [HasEnrichedHom V F₁ F₁] [HasEnrichedHom V F₁ F₂] :
    (λ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫
      enrichedComp V F₁ F₁ F₂ = 𝟙 _

Proof state:
case 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₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j ≫
      (λ_ (EnrichedCategory.Hom (F₁.obj j) (F₂.obj j))).inv ≫
        eId V (F₁.obj j) ▷ EnrichedCategory.Hom (F₁.obj j) (F₂.obj j) ≫ eComp V (F₁.obj j) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
rw [e_id_comp, comp_id]

Result:
no goals

Proof state:
case 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₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ ((λ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂) ≫
      end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j

Tactic:
rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def, assoc,
  ← comp_whiskerRight_assoc, enrichedId_π, ← whisker_exchange_assoc,
  id_whiskerLeft, assoc, assoc, Iso.inv_hom_id_assoc]

Result:
case 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₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j ≫
      (λ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv ≫
        eId V (F₁.obj j) ▷ ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

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₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂ =
    𝟙 (enrichedHom V F₁ F₂)

Tactic:
ext j

Result:
case 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₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ ((λ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂) ≫
      end_.π (diagram V F₁ F₂) j =
    𝟙 (enrichedHom V F₁ F₂) ≫ end_.π (diagram V F₁ F₂) j

Proof state:
case 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₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j ≫
      (λ_ (((diagram V F₁ F₂).obj (Opposite.op j)).obj j)).inv ≫
        eId V (F₁.obj j) ▷ ((diagram V F₁ F₂).obj (Opposite.op j)).obj j ≫
          eComp V (Opposite.unop (F₁.op.obj (Opposite.op j))) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j

Tactic:
dsimp

Result:
case 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₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
j : J
⊢ end_.π (diagram V F₁ F₂) j ≫
      (λ_ (EnrichedCategory.Hom (F₁.obj j) (F₂.obj j))).inv ≫
        eId V (F₁.obj j) ▷ EnrichedCategory.Hom (F₁.obj j) (F₂.obj j) ≫ eComp V (F₁.obj j) (F₁.obj j) (F₂.obj j) =
    end_.π (diagram V F₁ F₂) j