awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
w :
  ∀ (j : J),
    Eq.{v₁ + 1} (α :=
      obj.{v₃, v₁, u₃, u₁} ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)) j ⟶
        obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₃) j)
      (NatTrans.app ((functorHomEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₃) (f ≫ g)) j)
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := category) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
            ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)))
          (Iso.inv (λ_ ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃))
            ((functorHomEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂) f ⊗ₘ
              (functorHomEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₂ F₃) g)
            (functorEnrichedComp V F₁ F₂ F₃)))
        j)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₃, v₁, u₃, u₁} J V) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
      (functorEnrichedHom V F₁ F₃))
    ((functorHomEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₃) (f ≫ g) :
      Quiver.Hom (V := Functor.{v₃, v₁, u₃, u₁} J V) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
        (functorEnrichedHom V F₁ F₃))
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := category) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
          ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)))
        (Iso.inv (λ_ ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))))
        (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃))
          ((functorHomEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂) f ⊗ₘ
            (functorHomEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₂ F₃) g)
          (functorEnrichedComp V F₁ F₂ F₃)) :
      Quiver.Hom (V := Functor.{v₃, v₁, u₃, u₁} J V) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
        (functorEnrichedHom V F₁ F₃))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
w :
  Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
    (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃)
        ((homEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₁ F₃) (f ≫ g))
        (precompEnrichedHom V F₁ F₃ (Under.forget j)) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
    (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) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
            (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)))
          (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
              ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f)
              (precompEnrichedHom V F₁ F₂ (Under.forget j)) ⊗ₘ
            CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
              ((homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g)
              (precompEnrichedHom V F₂ F₃ (Under.forget j)))
          (enrichedComp V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃))) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃))
⊢ Eq.{v₁ + 1} (α :=
    obj.{v₃, v₁, u₃, u₁} ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)) j ⟶
      obj.{v₃, v₁, u₃, u₁} (functorEnrichedHom V F₁ F₃) j)
    (NatTrans.app ((functorHomEquiv V : (a : F₁ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₃) (f ≫ g)) j)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := category) ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))
          ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category)))
        (Iso.inv (λ_ ((𝟙_ (Functor.{v₃, v₁, u₃, u₁} J V)) (𝒞 := category))))
        (CategoryStruct.comp (Y := tensorObj (𝒞 := category) (functorEnrichedHom V F₁ F₂) (functorEnrichedHom V F₂ F₃))
          ((functorHomEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₁ F₂) f ⊗ₘ
            (functorHomEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ (J ⥤ V) ⟶ functorEnrichedHom V F₂ F₃) g)
          (functorEnrichedComp V F₁ F₂ F₃)))
      j)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Enriched.FunctorCategory
Goal:
V : Type u₁
inst : Category.{v₁, u₁} V
inst_1 : MonoidalCategory.{v₁, u₁} V
C : Type u₂
inst_2 : Category.{v₂, u₂} C
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
inst_7 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_8 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃
inst_9 : HasFunctorEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
inst_10 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under.{v₃, u₃} j
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
      obj (obj (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)) (Opposite.op k)) k)
    (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) (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
          (enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃))
        ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f ⊗ₘ
          (homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) g)
        (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₃) (enrichedComp V F₁ F₂ F₃)
          (enrichedHomπ V F₁ F₃ (obj (Under.forget j) k) ≫
            eHomWhiskerRight V (NatTrans.app (Iso.inv (Iso.refl (Under.forget j ⋙ F₁))) k)
                (F₃.obj (obj (Under.forget j) k)) ≫
              eHomWhiskerLeft V ((Under.forget j ⋙ F₁).obj k)
                (NatTrans.app (Iso.hom (Iso.refl (Under.forget j ⋙ F₃))) k)))))
    (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) (enrichedHom V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂))
          (enrichedHom V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)))
        (CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂)
            ((homEquiv V : (a : F₁ ⟶ F₂) → 𝟙_ V ⟶ enrichedHom V F₁ F₂) f)
            (precompEnrichedHom V F₁ F₂ (Under.forget j)) ⊗ₘ
          CategoryStruct.comp (Y := enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₂ F₃)
            ((homEquiv V : (a : F₂ ⟶ F₃) → 𝟙_ V ⟶ enrichedHom V F₂ F₃) 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))))

Tactic:
simp [tensorHom_comp_tensorHom_assoc]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
rw :
  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 β.hom ≫ eHomWhiskerRight V α.inv Y₁) ≫
      eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv)
    (𝟙 (@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 α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom) ≫
      eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))

Tactic:
rw [← eHom_whisker_exchange]

Premises used: CategoryTheory.eHom_whisker_exchange
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
a : eHomWhiskerRight V (α.hom ≫ α.inv) Y₁
| eHomWhiskerRight V α.inv Y₁ ≫ eHomWhiskerRight V α.hom Y₁

Tactic:
rw [← eHomWhiskerRight_comp]

Premises used: CategoryTheory.eHomWhiskerRight_comp
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
slice_lhs :
  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 β.hom ≫ eHomWhiskerRight V (α.hom ≫ α.inv) Y₁ ≫ eHomWhiskerLeft V X β.inv)
    (𝟙 (@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 β.hom ≫ eHomWhiskerRight V α.inv Y₁) ≫
      eHomWhiskerRight V α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))

Tactic:
slice_lhs 2 3 => rw [← eHomWhiskerRight_comp]

Premises used: CategoryTheory.eHomWhiskerRight_comp
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ 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 β.hom ≫ eHomWhiskerRight V (α.hom ≫ α.inv) Y₁ ≫ eHomWhiskerLeft V X β.inv)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))

Tactic:
simp [← eHomWhiskerLeft_comp]

Premises used: CategoryTheory.eHomWhiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
rw :
  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₁ β.inv ≫ eHomWhiskerRight V α.hom Y) ≫
      eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom)
    (𝟙 (@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 α.hom Y₁ ≫ eHomWhiskerLeft V X β.inv) ≫
      eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))

Tactic:
rw [← eHom_whisker_exchange]

Premises used: CategoryTheory.eHom_whisker_exchange
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
a : eHomWhiskerRight V (α.inv ≫ α.hom) Y
| eHomWhiskerRight V α.hom Y ≫ eHomWhiskerRight V α.inv Y

Tactic:
rw [← eHomWhiskerRight_comp]

Premises used: CategoryTheory.eHomWhiskerRight_comp
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
slice_lhs :
  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₁ β.inv ≫ eHomWhiskerRight V (α.inv ≫ α.hom) Y ≫ eHomWhiskerLeft V X₁ β.hom)
    (𝟙 (@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₁ β.inv ≫ eHomWhiskerRight V α.hom Y) ≫
      eHomWhiskerRight V α.inv Y ≫ eHomWhiskerLeft V X₁ β.hom)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))

Tactic:
slice_lhs 2 3 => rw [← eHomWhiskerRight_comp]

Premises used: CategoryTheory.eHomWhiskerRight_comp
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ 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₁ β.inv ≫ eHomWhiskerRight V (α.inv ≫ α.hom) Y ≫ eHomWhiskerLeft V X₁ β.hom)
    (𝟙 (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁))

Tactic:
simp [← eHomWhiskerLeft_comp]

Premises used: CategoryTheory.eHomWhiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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} (α :=
    Iso.{v', u'} (C := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
    (eHomCongr V (refl X) (refl Y)) (refl (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
w :
  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₃))
    (hom (eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂))) (hom (eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂))
⊢ Eq.{v' + 1} (α :=
    Iso.{v', u'} (C := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₃ Y₃))
    (eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂)) (eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ 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₃))
    (hom (eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂))) (hom (eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂))

Tactic:
simp [eHom_whisker_exchange_assoc]

Premises used: CategoryTheory.eHom_whisker_exchange_assoc
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
⊢ Eq.{v' + 1} (α :=
    Iso.{v', u'} (C := V) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
      (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y))
    (symm (eHomCongr V α β)) (eHomCongr V α.symm β.symm)

Tactic:
rfl

Premises used: CategoryTheory.Iso.eHomCongr, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
simp :
  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) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Z₁)
    (inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst))) ≫
        hom (ρ_ (tensorUnit.{v', u'} V (𝒞 := inst))) ≫
          CategoryStruct.comp (Y := @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
            ((eHomEquiv V : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f)
            (eHomWhiskerRight V α.inv Y ≫
              eHomWhiskerLeft V X₁ β.hom ≫
                CategoryStruct.comp (Y :=
                  tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
                    (tensorUnit.{v', u'} V (𝒞 := inst)))
                  (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 ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g ≫
                    @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁ ◁ eHomWhiskerRight V β.inv Z ≫
                      @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁ ◁ eHomWhiskerLeft V Y₁ γ.hom ≫
                        eComp V X₁ Y₁ Z₁)) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ 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) ≫ hom (eHomCongr V α γ) :
      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)))
        (inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁)
            (tensorUnit.{v', u'} V (𝒞 := inst)))
          (((eHomEquiv V : (a : X ⟶ Y) → 𝟙_ V ⟶ X ⟶[V] Y) f ≫ hom (eHomCongr V α β)) ▷
            tensorUnit.{v', u'} V (𝒞 := inst))
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Y₁ ◁
              ((eHomEquiv V : (a : Y ⟶ Z) → 𝟙_ V ⟶ Y ⟶[V] Z) g ≫ hom (eHomCongr V β γ)) ≫
            eComp V X₁ Y₁ Z₁)) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X₁ Z₁)

Tactic:
simp only [eHomCongr, MonoidalCategory.whiskerRight_id, assoc,
    MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Iso.eHomCongr, CategoryTheory.MonoidalCategory.whiskerRight_id
-- Module: Mathlib.CategoryTheory.Enriched.HomCongr
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 X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
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) ≫ inv (eHomCongr V α γ) :
      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)))
        (inv (λ_ (tensorUnit.{v', u'} V (𝒞 := inst))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v', u'} (𝒞 := inst) (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y)
            (tensorUnit.{v', u'} V (𝒞 := inst)))
          (((eHomEquiv V : (a : X₁ ⟶ Y₁) → 𝟙_ V ⟶ X₁ ⟶[V] Y₁) f ≫ inv (eHomCongr V α β)) ▷
            tensorUnit.{v', u'} V (𝒞 := inst))
          (@EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Y ◁
              ((eHomEquiv V : (a : Y₁ ⟶ Z₁) → 𝟙_ V ⟶ Y₁ ⟶[V] Z₁) g ≫ inv (eHomCongr V β γ)) ≫
            eComp V X Y Z)) :
      tensorUnit.{v', u'} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v', u', u} _ inst inst_1 _ _ X Z)

Tactic:
eHomCongr_comp V α.symm β.symm γ.symm f g

Premises used: CategoryTheory.Iso.eHomCongr_comp, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
J' : Type u₂
inst_1 : Category.{v₂, u₂} J'
V : Type u'
inst_2 : Category.{v', u'} V
inst_3 : MonoidalCategory.{v', u'} V
C : Type u
inst_4 : Category.{v, u} C
inst_5 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
F : Functor.{v₁, v, u₁, u} J C
inst_6 : HasConicalLimit.{v₁, u₁, v', v, u, u'} V F
⊢ HasLimit F

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
J' : Type u₂
inst_1 : Category.{v₂, u₂} J'
V : Type u'
inst_2 : Category.{v', u'} V
inst_3 : MonoidalCategory.{v', u'} V
C : Type u
inst_4 : Category.{v, u} C
inst_5 : EnrichedOrdinaryCategory.{v', v, u, u'} V C
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v₂, v₁, u₂, u₁} J' J
inst_6 : G.IsEquivalence
inst_7 : HasConicalLimit.{v₂, u₂, v', v, u, u'} V (G ⋙ F)
⊢ HasConicalLimit.{v₁, u₁, v', v, u, u'} V F

Tactic:
have e : G.inv ⋙ G ⋙ F ≅ F := G.asEquivalence.invFunIdAssoc F
  HasConicalLimit.of_iso V e

Premises used: CategoryTheory.Enriched.HasConicalLimit.of_iso, CategoryTheory.Functor.asEquivalence, CategoryTheory.Equivalence.invFunIdAssoc