awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
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
inst_4 : BraidedCategory.{w, v} V
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
X_1 Y_1 : Vᵒᵖ
f : X_1 ⟶ Y_1
σ : GradedNatTrans (Functor.obj (Center.ofBraided V) (unop X_1)) F G
X Y : C
p :
  Iso.hom (β_ (unop X_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      ((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop ≫ σ.app Y) ≫
          (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y)))) ≫
        eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw₁ :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop) ≫
            (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y)) ≫
          (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y)))) ≫
        eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
rw₂ :
  Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      ((𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop) ≫
          (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y)) ≫
        (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y))) ≫
          eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
      (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
have rw₃ : Iso.hom (β_ (unop Y_1) (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y)) ≫
    (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ f.unop) ≫
      (𝟙 (@EnrichedCategory.Hom.{w, v, u₁} _ inst inst_1 _ _ X Y) ⊗ₘ σ.app Y) ≫
        (F.map X Y ⊗ₘ 𝟙 (@EnrichedCategory.Hom.{w, v, u₂} _ inst inst_1 _ _ (F.obj Y) (G.obj Y))) ≫
          eComp V (F.obj X) (F.obj Y) (G.obj Y) =
  (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Tactic: rw [← id_tensor_comp_tensor_id (f.unop ≫ σ.app Y) _, id_tensor_comp, Category.assoc,
          Category.assoc, ← braiding_naturality_assoc, id_tensor_comp_tensor_id_assoc, p,
          tensorHom_comp_tensorHom_assoc, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
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 u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : Functor.{v, v, u₁, u₂} C D
X : C
⊢ Eq (α :=
    (𝟙_ (Type v)) (𝒞 := types) ⟶
      @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ (F.obj X) (F.obj X))
    (CategoryStruct.comp (Y := @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X X)
      (eId (Type v) X)
      (↾fun (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X X) ↦ F.map f))
    (eId (Type v) (F.obj X))
have h : Eq (α := @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ (F.obj X) (F.obj X))
  (TypeCat.Fun.toFun
    (ConcreteCategory.hom (FC := TypeCat.Fun)
      (CategoryStruct.comp (Y := @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X X)
        (eId (Type v) X)
        (↾fun (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X X) ↦ F.map f)))
    PUnit.unit)
  (TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (eId (Type v) (F.obj X))) PUnit.unit)
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.Basic (goal)
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 u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : Functor.{v, v, u₁, u₂} C D
X Y Z : C
⊢ Eq (α :=
    Quiver.Hom (V := Type v)
      (tensorObj (𝒞 := types) (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y)
        (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ Y Z))
      (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ (F.obj X) (F.obj Z)))
    (eComp (Type v) X Y Z ≫
      ↾fun (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Z) ↦ F.map f)
    (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := types)
        (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ (F.obj X) (F.obj Y))
        (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ (F.obj Y) (F.obj Z)))
      ((↾fun (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y) ↦ F.map f) ⊗ₘ
        ↾fun (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ Y Z) ↦ F.map f)
      (eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z)))
have h : ∀ (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y)
  (g : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ Y Z),
  Eq (α := @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ (F.obj X) (F.obj Z))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (eComp (Type v) X Y Z ≫
          ↾fun (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Z) ↦ F.map f))
      (f, g))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := types)
            (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ (F.obj X) (F.obj Y))
            (@EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ (F.obj Y) (F.obj Z)))
          ((↾fun (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ X Y) ↦
              F.map f) ⊗ₘ
            ↾fun (f : @EnrichedCategory.Hom _ types SemiCartesianMonoidalCategory.toMonoidalCategory _ _ Y Z) ↦ F.map f)
          (eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z))))
      (f, g))
Tactic: ext ⟨f, g⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.EnrichedCat (goal)
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
⊢ whiskerRight { out := α.out ≫ β.out : EnrichedNatTrans F H } I = whiskerRight α I ≫ whiskerRight β I
have h : ∀ (X : C),
  (whiskerRight { out := α.out ≫ β.out : EnrichedNatTrans F H } I).out.app X =
    (whiskerRight α I ≫ whiskerRight β I).out.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.EnrichedCat (goal)
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
⊢ (whiskerRight { out := α.out ≫ β.out : EnrichedNatTrans F H } I).out.app X =
    (whiskerRight α I ≫ whiskerRight β I).out.app X
have 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)))
Tactic: simp only [whiskerRight_out_app, NatTrans.comp_app, EnrichedFunctor.category_comp_out,
    EnrichedFunctor.forget, EnrichedFunctor.comp_obj, EnrichedFunctor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.EnrichedCat (goal)
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
⊢ whiskerLeft F β ≫ whiskerRight α I = whiskerRight α H ≫ whiskerLeft G β
have h : ∀ (X : C), (whiskerLeft F β ≫ whiskerRight α I).out.app X = (whiskerRight α H ≫ whiskerLeft G β).out.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.EnrichedCat (goal)
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
⊢ (whiskerLeft F β ≫ whiskerRight α I).out.app X = (whiskerRight α H ≫ whiskerLeft G β).out.app X
have 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)))
Tactic: simp only [EnrichedFunctor.forget_obj, EnrichedFunctor.comp_obj,
    EnrichedFunctor.category_comp_out, NatTrans.comp_app, whiskerLeft_out_app,
    whiskerRight_out_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
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) ⟶ 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)
    ((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)
have trans : 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: trans eHomEquiv V (τ.app i ≫ F₂.map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
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) ⟶ 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))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
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 _ _ (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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
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
⊢ 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))
have 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))
Tactic: simp only [eHomEquiv_comp, Equiv.apply_symm_apply, Iso.cancel_iso_inv_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
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
| (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)
have rw : Iso.hom (ρ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
  g ≫
    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: rw [tensorHom_def_assoc, MonoidalCategory.whiskerRight_id_assoc, assoc,
            enrichedHom_condition' V F₁ F₂ f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Enriched.FunctorCategory (goal)
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
| (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))
have rw : Iso.hom (ρ_ (tensorUnit.{v₁, u₁} V (𝒞 := inst))) ≫
  g ≫
    end_.π (diagram 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: rw [tensorHom_def'_assoc, MonoidalCategory.whiskerLeft_comp_assoc,
            id_whiskerLeft_assoc, id_whiskerLeft_assoc, Iso.inv_hom_id_assoc, unitors_equal]