-- Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
/-- Given an isomorphism `α : Y ≅ Y₁` in C, the enriched composition map
`eComp V X Y Z : (X ⟶[V] Y) ⊗ (Y ⟶[V] Z) ⟶ (X ⟶[V] Z)` factors through the `V`
object `(X ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z)` via the map defined by whiskering in the
middle with `α.hom` and `α.inv`. -/
@[reassoc]
lemma eHom_whisker_cancel {X Y Y₁ Z : C} (α : Y  ≅ Y₁) :
    eHomWhiskerLeft V X α.hom ▷ _ ≫ _ ◁ eHomWhiskerRight V α.inv Z ≫
      eComp V X Y₁ Z = eComp V X Y Z

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ ((ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) α.hom ≫ eComp V X Y Y₁) ▷
        EnrichedCategory.Hom Y Z ≫
      EnrichedCategory.Hom X Y₁ ◁
          ((λ_ (EnrichedCategory.Hom Y Z)).inv ≫ (eHomEquiv V) α.inv ▷ EnrichedCategory.Hom Y Z ≫ eComp V Y₁ Y Z) ≫
        eComp V X Y₁ Z =
    eComp V X Y Z

Tactic:
simp only [MonoidalCategory.whiskerLeft_comp_assoc, whisker_assoc_symm,
  triangle_assoc_comp_left_inv_assoc, e_assoc', assoc]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ ((ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) α.hom ≫ eComp V X Y Y₁) ▷
        EnrichedCategory.Hom Y Z ≫
      (ρ_ (EnrichedCategory.Hom X Y₁)).inv ▷ EnrichedCategory.Hom Y Z ≫
        (EnrichedCategory.Hom X Y₁ ◁ (eHomEquiv V) α.inv) ▷ EnrichedCategory.Hom Y Z ≫
          eComp V X Y₁ Y ▷ EnrichedCategory.Hom Y Z ≫ eComp V X Y Z =
    eComp V X Y Z

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ eHomWhiskerLeft V X α.hom ▷ EnrichedCategory.Hom Y Z ≫
      EnrichedCategory.Hom X Y₁ ◁ eHomWhiskerRight V α.inv Z ≫ eComp V X Y₁ Z =
    eComp V X Y Z

Tactic:
dsimp [eHomWhiskerLeft, eHomWhiskerRight]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ ((ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) α.hom ≫ eComp V X Y Y₁) ▷
        EnrichedCategory.Hom Y Z ≫
      EnrichedCategory.Hom X Y₁ ◁
          ((λ_ (EnrichedCategory.Hom Y Z)).inv ≫ (eHomEquiv V) α.inv ▷ EnrichedCategory.Hom Y Z ≫ eComp V Y₁ Y Z) ≫
        eComp V X Y₁ Z =
    eComp V X Y Z

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ (eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ EnrichedCategory.Hom Y Z ≫ eComp V X Y Z = eComp V X Y Z

Tactic:
simp [← eHomWhiskerLeft_comp]

Result:
no goals

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ ((ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) α.hom ≫ eComp V X Y Y₁) ▷
        EnrichedCategory.Hom Y Z ≫
      (ρ_ (EnrichedCategory.Hom X Y₁)).inv ▷ EnrichedCategory.Hom Y Z ≫
        (EnrichedCategory.Hom X Y₁ ◁ (eHomEquiv V) α.inv) ▷ EnrichedCategory.Hom Y Z ≫
          eComp V X Y₁ Y ▷ EnrichedCategory.Hom Y Z ≫ eComp V X Y Z =
    eComp V X Y Z

Tactic:
simp only [← comp_whiskerRight_assoc]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ (((ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) α.hom ≫ eComp V X Y Y₁) ≫
          (ρ_ (EnrichedCategory.Hom X Y₁)).inv ≫ EnrichedCategory.Hom X Y₁ ◁ (eHomEquiv V) α.inv ≫ eComp V X Y₁ Y) ▷
        EnrichedCategory.Hom Y Z ≫
      eComp V X Y Z =
    eComp V X Y Z

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ (((ρ_ (EnrichedCategory.Hom X Y)).inv ≫ EnrichedCategory.Hom X Y ◁ (eHomEquiv V) α.hom ≫ eComp V X Y Y₁) ≫
          (ρ_ (EnrichedCategory.Hom X Y₁)).inv ≫ EnrichedCategory.Hom X Y₁ ◁ (eHomEquiv V) α.inv ≫ eComp V X Y₁ Y) ▷
        EnrichedCategory.Hom Y Z ≫
      eComp V X Y Z =
    eComp V X Y Z

Tactic:
change (eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ _ ≫ _ = _

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ (eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ EnrichedCategory.Hom Y Z ≫ eComp V X Y Z = eComp V X Y Z