awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Enriched.Basic
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C_1 : Type u₁
inst_2 : EnrichedCategory.{w, v, u₁} V C_1
C : Type v
inst_3 : EnrichedCategory (Type v) C
D : Type v
inst_4 : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ :
  Functor.obj
    (Functor.obj yoneda
      (Quiver.Hom (V := C ⥤ D)
        ((enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) F : C ⥤ D)
        ((enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) G : C ⥤ D)))
    α
X Y : C
x : Sigma.fst (β := fun (X : Type v) ↦ HalfBraiding X) (Functor.obj (Center.ofBraided (Type v)) (unop α))
f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            (HalfBraiding.β
              (Sigma.snd (β := fun (X : Type v) ↦ HalfBraiding X) (Functor.obj (Center.ofBraided (Type v)) (unop α)))
              (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y)) ≫
          (F.map X Y ⊗ₘ
              ↾fun
                  (x :
                    Sigma.fst (β := fun (X : Type v) ↦ HalfBraiding X)
                      (Functor.obj (Center.ofBraided (Type v)) (unop α))) ↦
                NatTrans.app
                  ((TypeCat.Hom.hom σ :
                      (a : unop α) →
                        (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) F ⟶
                          (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) G)
                    x)
                  Y) ≫
            eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y)))
      (x, f) =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (((↾fun
                (x :
                  Sigma.fst (β := fun (X : Type v) ↦ HalfBraiding X)
                    (Functor.obj (Center.ofBraided (Type v)) (unop α))) ↦
              NatTrans.app
                ((TypeCat.Hom.hom σ :
                    (a : unop α) →
                      (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) F ⟶
                        (enrichedFunctorTypeEquivFunctor : (a : EnrichedFunctor (Type v) C D) → C ⥤ D) G)
                  x)
                X) ⊗ₘ
            G.map X Y) ≫
          eComp (Type v) (F.obj X) (G.obj X) (G.obj Y)))
      (x, f)

Tactic:
exact (σ.hom x).naturality f

Premises used: CategoryTheory.NatTrans.naturality, TypeCat.Hom.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Enriched.EnrichedCat
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u
inst_2 : EnrichedCategory.{w, v, u} V C
D : Type u₁
inst_3 : EnrichedCategory.{w, v, u₁} V D
E : Type u₂
inst_4 : EnrichedCategory.{w, v, u₂} V E
F G H : EnrichedFunctor.{w, v, u, u₁} V C D
α : F ⟶ G
β : G ⟶ H
I : EnrichedFunctor.{w, v, u₁, u₂} V D E
h :
  ∀ (X : C),
    (whiskerRight { out := α.out ≫ β.out : EnrichedNatTrans F H } I).out.app X =
      (whiskerRight α I ≫ whiskerRight β I).out.app X
⊢ whiskerRight { out := α.out ≫ β.out : EnrichedNatTrans F H } I = whiskerRight α I ≫ whiskerRight β I

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Enriched.EnrichedCat
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u
inst_2 : EnrichedCategory.{w, v, u} V C
D : Type u₁
inst_3 : EnrichedCategory.{w, v, u₁} V D
E : Type u₂
inst_4 : EnrichedCategory.{w, v, u₂} V E
F G H : EnrichedFunctor.{w, v, u, u₁} V C D
α : F ⟶ G
β : G ⟶ H
I : EnrichedFunctor.{w, v, u₁, u₂} V D E
X : C
h :
  homOf V (homTo V (α.out.app X ≫ β.out.app X) ≫ I.map (F.obj («to».{w, v, u} V X)) (H.obj («to».{w, v, u} V X))) =
    homOf V (homTo V (α.out.app X) ≫ I.map (F.obj («to».{w, v, u} V X)) (G.obj («to».{w, v, u} V X))) ≫
      homOf V (homTo V (β.out.app X) ≫ I.map (G.obj («to».{w, v, u} V X)) (H.obj («to».{w, v, u} V X)))
⊢ (whiskerRight { out := α.out ≫ β.out : EnrichedNatTrans F H } I).out.app X =
    (whiskerRight α I ≫ whiskerRight β I).out.app X

Tactic:
simp only [whiskerRight_out_app, NatTrans.comp_app, EnrichedFunctor.category_comp_out,
    EnrichedFunctor.forget, EnrichedFunctor.comp_obj, EnrichedFunctor.comp_map]

Premises used: CategoryTheory.EnrichedFunctor.comp_map, CategoryTheory.EnrichedFunctor.category_comp_out, CategoryTheory.EnrichedFunctor.forget, CategoryTheory.EnrichedFunctor.comp_obj, CategoryTheory.EnrichedCat.whiskerRight_out_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Enriched.EnrichedCat
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u
inst_2 : EnrichedCategory.{w, v, u} V C
D : Type u₁
inst_3 : EnrichedCategory.{w, v, u₁} V D
E : Type u₂
inst_4 : EnrichedCategory.{w, v, u₂} V E
F G H : EnrichedFunctor.{w, v, u, u₁} V C D
α : F ⟶ G
β : G ⟶ H
I : EnrichedFunctor.{w, v, u₁, u₂} V D E
X : C
⊢ homOf V (homTo V (α.out.app X ≫ β.out.app X) ≫ I.map (F.obj («to».{w, v, u} V X)) (H.obj («to».{w, v, u} V X))) =
    homOf V (homTo V (α.out.app X) ≫ I.map (F.obj («to».{w, v, u} V X)) (G.obj («to».{w, v, u} V X))) ≫
      homOf V (homTo V (β.out.app X) ≫ I.map (G.obj («to».{w, v, u} V X)) (H.obj («to».{w, v, u} V X)))

Tactic:
simp [← ForgetEnrichment.homOf_comp]

Premises used: CategoryTheory.ForgetEnrichment.homOf_comp
-- Module: Mathlib.CategoryTheory.Enriched.EnrichedCat
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u
inst_2 : EnrichedCategory.{w, v, u} V C
D : Type u₁
inst_3 : EnrichedCategory.{w, v, u₁} V D
E : Type u₂
inst_4 : EnrichedCategory.{w, v, u₂} V E
F G : EnrichedFunctor.{w, v, u, u₁} V C D
H I : EnrichedFunctor.{w, v, u₁, u₂} V D E
α : F ⟶ G
β : H ⟶ I
h : ∀ (X : C), (whiskerLeft F β ≫ whiskerRight α I).out.app X = (whiskerRight α H ≫ whiskerLeft G β).out.app X
⊢ whiskerLeft F β ≫ whiskerRight α I = whiskerRight α H ≫ whiskerLeft G β

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Enriched.EnrichedCat
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u
inst_2 : EnrichedCategory.{w, v, u} V C
D : Type u₁
inst_3 : EnrichedCategory.{w, v, u₁} V D
E : Type u₂
inst_4 : EnrichedCategory.{w, v, u₂} V E
F G : EnrichedFunctor.{w, v, u, u₁} V C D
H I : EnrichedFunctor.{w, v, u₁, u₂} V D E
α : F ⟶ G
β : H ⟶ I
X : C
h :
  β.out.app (ForgetEnrichment.of V (F.obj («to».{w, v, u} V X))) ≫
      homOf V (homTo V (α.out.app X) ≫ I.map (F.obj («to».{w, v, u} V X)) (G.obj («to».{w, v, u} V X))) =
    homOf V (homTo V (α.out.app X) ≫ H.map (F.obj («to».{w, v, u} V X)) (G.obj («to».{w, v, u} V X))) ≫
      β.out.app (ForgetEnrichment.of V (G.obj («to».{w, v, u} V X)))
⊢ (whiskerLeft F β ≫ whiskerRight α I).out.app X = (whiskerRight α H ≫ whiskerLeft G β).out.app X

Tactic:
simp only [EnrichedFunctor.forget_obj, EnrichedFunctor.comp_obj,
    EnrichedFunctor.category_comp_out, NatTrans.comp_app, whiskerLeft_out_app,
    whiskerRight_out_app]

Premises used: CategoryTheory.EnrichedFunctor.forget_obj, CategoryTheory.EnrichedFunctor.category_comp_out, CategoryTheory.EnrichedFunctor.comp_obj, CategoryTheory.EnrichedCat.whiskerLeft_out_app, CategoryTheory.EnrichedCat.whiskerRight_out_app, CategoryTheory.NatTrans.comp_app
-- Module: Mathlib.CategoryTheory.Enriched.EnrichedCat
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u
inst_2 : EnrichedCategory.{w, v, u} V C
D : Type u₁
inst_3 : EnrichedCategory.{w, v, u₁} V D
E : Type u₂
inst_4 : EnrichedCategory.{w, v, u₂} V E
F G : EnrichedFunctor.{w, v, u, u₁} V C D
H I : EnrichedFunctor.{w, v, u₁, u₂} V D E
α : F ⟶ G
β : H ⟶ I
X : C
⊢ β.out.app (ForgetEnrichment.of V (F.obj («to».{w, v, u} V X))) ≫
      homOf V (homTo V (α.out.app X) ≫ I.map (F.obj («to».{w, v, u} V X)) (G.obj («to».{w, v, u} V X))) =
    homOf V (homTo V (α.out.app X) ≫ H.map (F.obj («to».{w, v, u} V X)) (G.obj («to».{w, v, u} V X))) ≫
      β.out.app (ForgetEnrichment.of V (G.obj («to».{w, v, u} V X)))

Tactic:
(β.out.naturality (α.out.app (ForgetEnrichment.of V X))).symm

Premises used: CategoryTheory.ForgetEnrichment.of, CategoryTheory.EnrichedNatTrans.out, CategoryTheory.ForgetEnrichment.to, CategoryTheory.ForgetEnrichment.homOf, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Enriched.EnrichedCat
Goal:
V : Type v
inst : Category.{w, v} V
inst_1 : MonoidalCategory.{w, v} V
C : Type u
inst_2 : EnrichedCategory.{w, v, u} V C
D : Type u₁
inst_3 : EnrichedCategory.{w, v, u₁} V D
E : Type u₂
inst_4 : EnrichedCategory.{w, v, u₂} V E
F G : EnrichedFunctor.{w, v, u, u₁} V C D
H I : EnrichedFunctor.{w, v, u₁, u₂} V D E
α : F ⟶ G
β : H ⟶ I
X : C
⊢ β.out.app (ForgetEnrichment.of V (F.obj («to».{w, v, u} V X))) ≫
      homOf V (homTo V (α.out.app X) ≫ I.map (F.obj («to».{w, v, u} V X)) (G.obj («to».{w, v, u} V X))) =
    homOf V (homTo V (α.out.app X) ≫ H.map (F.obj («to».{w, v, u} V X)) (G.obj («to».{w, v, u} V X))) ≫
      β.out.app (ForgetEnrichment.of V (G.obj («to».{w, v, u} V X)))

Tactic:
exact (β.out.naturality (α.out.app (ForgetEnrichment.of V X))).symm

Premises used: CategoryTheory.ForgetEnrichment.of, CategoryTheory.EnrichedNatTrans.out, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.NatTrans.app
-- 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₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    (enrichedHomπ V F₁ F₂ i ≫ eHomWhiskerLeft V (F₁.obj i) (F₂.map f))
    (enrichedHomπ V F₁ F₂ j ≫ eHomWhiskerRight V (F₁.map f) (F₂.obj j))

Tactic:
end_.condition (diagram V F₁ F₂) f

Premises used: Quiver.Hom.unop, CategoryTheory.Limits.end_.condition, CategoryTheory.Enriched.FunctorCategory.diagram, CategoryTheory.eHomWhiskerLeft, CategoryTheory.eHomWhiskerRight
-- 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₂ : Functor.{v₃, v₂, u₃, u₂} J C
inst_5 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂ ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    (enrichedHomπ V F₁ F₂ i ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i))
          (tensorUnit.{v₁, u₁} V (𝒞 := inst)))
        (Iso.inv (ρ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₂.obj i) (F₂.obj j)))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj i) ◁
            (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f))
          (eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j))))
    (enrichedHomπ V F₁ F₂ j ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
        (Iso.inv (λ_ (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
            (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
          ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ▷
            @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j))
          (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j))))

Tactic:
end_.condition (diagram V F₁ F₂) f

Premises used: Quiver.Hom.unop, CategoryTheory.Limits.end_.condition, CategoryTheory.Enriched.FunctorCategory.diagram, CategoryTheory.eHomWhiskerLeft, CategoryTheory.eHomWhiskerRight
-- 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
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
dsimp :
  Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj i ⟶ F₂.obj i) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₂.obj i) (τ.app i) ≫
        eHomWhiskerLeft V (F₁.obj i) (F₂.map f) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₂.obj j) (τ.app i ≫ F₂.map f) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) j)
    ((fun (j : J) ↦
          ((eHomEquiv V :
                (a : Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶ F₂.obj j) →
                  𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶[V] F₂.obj j)
              (τ.app j) :
            tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
              @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op j)))
                (F₂.obj j)))
        i ≫
      map (obj (diagram V F₁ F₂) (Opposite.op i)) f)
    ((eHomEquiv V :
        (a : Opposite.unop (F₁.op.obj (Opposite.op i)) ⟶ F₂.obj j) →
          𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op i)) ⟶[V] F₂.obj j)
      (τ.app i ≫ F₂.map f))

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
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj i ⟶ F₂.obj i) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₂.obj i) (τ.app i) ≫
        eHomWhiskerLeft V (F₁.obj i) (F₂.map f) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₂.obj j) (τ.app i ≫ F₂.map f) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))

Tactic:
simp only [eHomEquiv_comp, tensorHom_def_assoc, MonoidalCategory.whiskerRight_id,
        ← unitors_equal, assoc, Iso.inv_hom_id_assoc, eHomWhiskerLeft]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.unitors_equal, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.whiskerRight_id, CategoryTheory.eHomWhiskerLeft, CategoryTheory.eHomEquiv_comp, CategoryTheory.MonoidalCategory.tensorHom_def_assoc
-- 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
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
dsimp :
  Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₂.obj j) (τ.app i ≫ F₂.map f) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj j ⟶ F₂.obj j) → 𝟙_ V ⟶ F₁.obj j ⟶[V] F₂.obj j) (τ.app j) ≫
        eHomWhiskerRight V (F₁.map f) (F₂.obj j) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj j))
    ((eHomEquiv V :
          (a : Opposite.unop (F₁.op.obj (Opposite.op i)) ⟶ F₂.obj j) →
            𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op i)) ⟶[V] F₂.obj j)
        (τ.app i ≫ F₂.map f) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op i))) (F₂.obj j))
    ((fun (j : J) ↦
            ((eHomEquiv V :
                  (a : Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶ F₂.obj j) →
                    𝟙_ V ⟶ Opposite.unop (F₁.op.obj (Opposite.op j)) ⟶[V] F₂.obj j)
                (τ.app j) :
              tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶
                @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (Opposite.unop (F₁.op.obj (Opposite.op j)))
                  (F₂.obj j)))
          j ≫
        NatTrans.app (map (diagram V F₁ F₂) f.op) j :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ obj.{v₃, v₁, u₃, u₁} (obj (diagram V F₁ F₂) (Opposite.op i)) 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
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
τ : F₁ ⟶ F₂
i j : J
f : i ⟶ j
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₂.obj j) (τ.app i ≫ F₂.map f) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj j ⟶ F₂.obj j) → 𝟙_ V ⟶ F₁.obj j ⟶[V] F₂.obj j) (τ.app j) ≫
        eHomWhiskerRight V (F₁.map f) (F₂.obj j) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))

Tactic:
simp only [← NatTrans.naturality, eHomEquiv_comp, tensorHom_def', id_whiskerLeft,
        assoc, Iso.inv_hom_id_assoc, eHomWhiskerRight]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.id_whiskerLeft, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.tensorHom_def', CategoryTheory.NatTrans.naturality, CategoryTheory.eHomEquiv_comp, CategoryTheory.eHomWhiskerRight
-- 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
K : Type u₄
inst_4 : Category.{v₄, u₄} K
inst_5 : EnrichedOrdinaryCategory.{v₁, v₂, u₂, u₁} V C
F₁ F₂ F₃ F₄ : Functor.{v₃, v₂, u₃, u₂} J C
inst_6 : HasEnrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
g : tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ enrichedHom.{v₁, v₂, v₃, u₁, u₂, u₃} V F₁ F₂
i j : J
f : i ⟶ j
simp :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
      @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₁.obj j))
          (@EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj j) (F₂.obj j)))
        ((eHomEquiv V : (a : F₁.obj i ⟶ F₁.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₁.obj j) (F₁.map f) ⊗ₘ
          g ≫ end_.π (diagram V F₁ F₂) j)
        (eComp V (F₁.obj i) (F₁.obj j) (F₂.obj j)) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((g ≫ end_.π (diagram V F₁ F₂) i ⊗ₘ
          (eHomEquiv V : (a : F₂.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₂.obj i ⟶[V] F₂.obj j) (F₂.map f)) ≫
        eComp V (F₁.obj i) (F₂.obj i) (F₂.obj j) :
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) (tensorUnit.{v₁, u₁} V (𝒞 := inst)) ⟶
        @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₂.obj j)
        (F₁.map f ≫
          (Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ F₁.obj j ⟶[V] F₂.obj j) → F₁.obj j ⟶ F₂.obj j)
            (g ≫ end_.π (diagram V F₁ F₂) j)) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))
    ((eHomEquiv V : (a : F₁.obj i ⟶ F₂.obj j) → 𝟙_ V ⟶ F₁.obj i ⟶[V] F₂.obj j)
        ((Equiv.symm (eHomEquiv V) : (a : 𝟙_ V ⟶ F₁.obj i ⟶[V] F₂.obj i) → F₁.obj i ⟶ F₂.obj i)
            (g ≫ end_.π (diagram V F₁ F₂) i) ≫
          F₂.map f) :
      tensorUnit.{v₁, u₁} V (𝒞 := inst) ⟶ @EnrichedCategory.Hom.{v₁, u₁, u₂} _ inst inst_1 _ _ (F₁.obj i) (F₂.obj j))

Tactic:
simp only [eHomEquiv_comp, Equiv.apply_symm_apply, Iso.cancel_iso_inv_left]

Premises used: Equiv.apply_symm_apply, CategoryTheory.Iso.cancel_iso_inv_left, CategoryTheory.eHomEquiv_comp