awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Enriched.Opposite
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
inst_2 : BraidedCategory.{v₁, u₁} V
C : Type u
inst_3 : EnrichedCategory.{v₁, u₁, u} V C
D : Type u
inst_4 : Category.{v, u} D
inst_5 : EnrichedOrdinaryCategory.{v₁, v, u, u₁} V D
X Y Z : Dᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
    ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
        (Iso.inv (λ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ Y Z)
            (@EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Y))
          ((Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g ⊗ₘ
            (Equiv.trans (Equiv.symm Quiver.Hom.opEquiv) homEquiv : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f)
          (eComp V (Opposite.unop Z) (Opposite.unop Y) (Opposite.unop X))) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u} _ inst inst_1 _ _ X Z)

Tactic:
exact homEquiv_comp g.unop f.unop

Premises used: CategoryTheory.EnrichedOrdinaryCategory.homEquiv_comp, Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X : C
⊢ Eq.{v' + 1} (α := tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X X)
    ((eHomEquiv V : (a : X ⟶ X) → 𝟙_ V ⟶ X ⟶[V] X) (𝟙 X) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X X)
    (eId V X : tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X X)

Tactic:
EnrichedOrdinaryCategory.homEquiv_id _

Premises used: CategoryTheory.EnrichedOrdinaryCategory.homEquiv_id
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v' + 1} (α := tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z)
    ((eHomEquiv V : (a : X ⟶ Z) → 𝟙_ V ⟶ X ⟶[V] Z) (f ≫ g) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z)
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst)) (tensorUnit.{v', u'} V (𝒞 := inst)))
        (Iso.inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst))))
        (((eHomEquiv V : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f ⊗ₘ (eHomEquiv V : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g) ≫
          eComp V X Y Z) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z)

Tactic:
EnrichedOrdinaryCategory.homEquiv_comp _ _

Premises used: CategoryTheory.EnrichedOrdinaryCategory.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y : C
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
    (eHomWhiskerRight V (𝟙 X) Y) (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))

Tactic:
simp [eHomWhiskerRight]

Premises used: CategoryTheory.eHomWhiskerRight
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
dsimp :
  Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y))
        (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y)))
        ((eHomEquiv V : (a : X ⟶ X'') → 𝟙_ V ⟶ X ⟶[V] X'') (f ≫ f') ▷
            @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y ≫
          eComp V X X'' Y) :
      Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y))
          (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y)))
          ((eHomEquiv V : (a : X' ⟶ X'') → 𝟙_ V ⟶ X' ⟶[V] X'') f' ▷
              @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y ≫
            eComp V X' X'' Y))
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y))
          (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)))
          ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷
              @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y ≫
            eComp V X X' Y)) :
      Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X'' Y)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
    (eHomWhiskerRight V (f ≫ f') Y) (eHomWhiskerRight V f' Y ≫ eHomWhiskerRight V f Y)

Tactic:
dsimp [eHomWhiskerRight]

Premises used: CategoryTheory.eHomWhiskerRight
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X X' : C
f : X ⟶ X'
Y Z : C
dsimp :
  Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (eComp V X' Y Z ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Z))
        (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Z)))
        ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Z ≫
          eComp V X X' Z))
    (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y))
          (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)))
          ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷
              @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y ≫
            eComp V X X' Y) ▷
        @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
      eComp V X Y Z)
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (eComp V X' Y Z ≫ eHomWhiskerRight V f Z)
    (eHomWhiskerRight V f Y ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫ eComp V X Y Z)

Tactic:
dsimp [eHomWhiskerRight]

Premises used: CategoryTheory.eHomWhiskerRight
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
          (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
        (Iso.inv
          (λ_
            (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
              (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))))
        ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷
            tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
              (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z) ≫
          @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X X' ◁ eComp V X' Y Z ≫ eComp V X X' Z) :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (CategoryStruct.comp (Y :=
            tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
              (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y))
            (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)))
            ((eHomEquiv V : (a : X ⟶ X') → 𝟙_ V ⟶ X ⟶[V] X') f ▷
                @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y ≫
              eComp V X X' Y) ▷
          @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
        eComp V X Y Z :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X' Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))

Tactic:
simp [e_assoc']

Premises used: CategoryTheory.e_assoc'
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y : C
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
    (eHomWhiskerLeft V X (𝟙 Y)) (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))

Tactic:
simp [eHomWhiskerLeft]

Premises used: CategoryTheory.eHomWhiskerLeft
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
dsimp :
  Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y''))
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (tensorUnit.{v', u'} V (𝒞 := inst)))
        (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁
            (eHomEquiv V : (a : Y ⟶ Y'') → 𝟙_ V ⟶ Y ⟶[V] Y'') (g ≫ g') ≫
          eComp V X Y Y'') :
      Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y''))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y')
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
            (tensorUnit.{v', u'} V (𝒞 := inst)))
          (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)))
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁ (eHomEquiv V : (a : Y ⟶ Y') → 𝟙_ V ⟶ Y ⟶[V] Y') g ≫
            eComp V X Y Y'))
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y')
            (tensorUnit.{v', u'} V (𝒞 := inst)))
          (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y')))
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y' ◁
              (eHomEquiv V : (a : Y' ⟶ Y'') → 𝟙_ V ⟶ Y' ⟶[V] Y'') g' ≫
            eComp V X Y' Y'')) :
      Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y''))
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y''))
    (eHomWhiskerLeft V X (g ≫ g')) (eHomWhiskerLeft V X g ≫ eHomWhiskerLeft V X g')

Tactic:
dsimp [eHomWhiskerLeft]

Premises used: CategoryTheory.eHomWhiskerLeft
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y Z Z' : C
g : Z ⟶ Z'
dsimp :
  Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z'))
    (eComp V X Y Z ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z)
          (tensorUnit.{v', u'} V (𝒞 := inst)))
        (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z)))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z ◁ (eHomEquiv V : (a : Z ⟶ Z') → 𝟙_ V ⟶ Z ⟶[V] Z') g ≫
          eComp V X Z Z'))
    (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁
        CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)
            (tensorUnit.{v', u'} V (𝒞 := inst)))
          (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ◁ (eHomEquiv V : (a : Z ⟶ Z') → 𝟙_ V ⟶ Z ⟶[V] Z') g ≫
            eComp V Y Z Z') ≫
      eComp V X Y Z')
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z'))
    (eComp V X Y Z ≫ eHomWhiskerLeft V X g)
    (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁ eHomWhiskerLeft V Y g ≫ eComp V X Y Z')

Tactic:
dsimp [eHomWhiskerLeft]

Premises used: CategoryTheory.eHomWhiskerLeft
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y Z Z' : C
g : Z ⟶ Z'
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z'))
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst)
          (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
          (tensorUnit.{v', u'} V (𝒞 := inst)))
        (Iso.inv
          (ρ_
            (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
              (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))))
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
              (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z) ◁
            (eHomEquiv V : (a : Z ⟶ Z') → 𝟙_ V ⟶ Z ⟶[V] Z') g ≫
          eComp V X Y Z ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Z Z' ≫ eComp V X Z Z') :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z'))
    (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁
          CategoryStruct.comp (Y :=
            tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)
              (tensorUnit.{v', u'} V (𝒞 := inst)))
            (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ◁
                (eHomEquiv V : (a : Z ⟶ Z') → 𝟙_ V ⟶ Z ⟶[V] Z') g ≫
              eComp V Y Z Z') ≫
        eComp V X Y Z' :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z'))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y Y₁ Z : C
α : Y ≅ Y₁
dsimp :
  Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (CategoryStruct.comp (Y :=
        tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (CategoryStruct.comp (Y :=
            tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
              (tensorUnit.{v', u'} V (𝒞 := inst)))
            (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)))
            (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁
                (eHomEquiv V : (a : Y ⟶ Y₁) → 𝟙_ V ⟶ Y ⟶[V] Y₁) α.hom ≫
              eComp V X Y Y₁) ▷
          @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁ ◁
            CategoryStruct.comp (Y :=
              tensorObj.{v', u'} (𝒞 := inst) (tensorUnit.{v', u'} V (𝒞 := inst))
                (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
              (Iso.inv (λ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z)))
              ((eHomEquiv V : (a : Y₁ ⟶ Y) → 𝟙_ V ⟶ Y₁ ⟶[V] Y) α.inv ▷
                  @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
                eComp V Y₁ Y Z) ≫
          eComp V X Y₁ Z) :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (eComp V X Y Z :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (eHomWhiskerLeft V X α.hom ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
      @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁ ◁ eHomWhiskerRight V α.inv Z ≫ eComp V X Y₁ Z)
    (eComp V X Y Z)

Tactic:
dsimp [eHomWhiskerLeft, eHomWhiskerRight]

Premises used: CategoryTheory.eHomWhiskerLeft, CategoryTheory.eHomWhiskerRight
-- Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic
Goal:
V : Type u'
inst : Category.{v', u'} V
inst_1 : MonoidalCategory.{v', u'} V
C : Type u
inst_2 : Category.{v, u} C
inst_3 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
X Y Y₁ Z : C
α : Y ≅ Y₁
change :
  Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    ((eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
      eComp V X Y Z)
    (eComp V X Y Z)
⊢ Eq.{v' + 1} (α :=
    Quiver.Hom.{v', u'} (V := V)
      (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)
            (CategoryStruct.comp (Y :=
              tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
                (tensorUnit.{v', u'} V (𝒞 := inst)))
              (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)))
              (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁
                  (eHomEquiv V : (a : Y ⟶ Y₁) → 𝟙_ V ⟶ Y ⟶[V] Y₁) α.hom ≫
                eComp V X Y Y₁))
            (CategoryStruct.comp (Y :=
              tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)
                (tensorUnit.{v', u'} V (𝒞 := inst)))
              (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁)))
              (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y₁ ◁
                  (eHomEquiv V : (a : Y₁ ⟶ Y) → 𝟙_ V ⟶ Y₁ ⟶[V] Y) α.inv ≫
                eComp V X Y₁ Y)) ▷
          @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z ≫
        eComp V X Y Z :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))
    (eComp V X Y Z :
      Quiver.Hom.{v', u'} (V := V)
        (tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ Y Z))
        (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z))

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

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.eHomWhiskerLeft, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv