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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
      (F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) ⊗ₘ
          F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
        eComp W (F.obj (ForgetEnrichment.to W X)) (F.obj (ForgetEnrichment.to W Y)) (F.obj (ForgetEnrichment.to W Z)) =
    (ForgetEnrichment.homTo W f ⊗ₘ ForgetEnrichment.homTo W g) ≫
      (F.map (ForgetEnrichment.to W X) (ForgetEnrichment.to W Y) ⊗ₘ
          F.map (ForgetEnrichment.to W Y) (ForgetEnrichment.to W Z)) ≫
        eComp W (ForgetEnrichment.to.{w', v', u₂} W (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X))))
          (ForgetEnrichment.to.{w', v', u₂} W (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Y))))
          (ForgetEnrichment.to.{w', v', u₂} W (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z))))

Tactic:
rfl
-- 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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f_1 : X ⟶ Y
g_1 : Y ⟶ Z
f g :
  Quiver.Hom (V := ForgetEnrichment.{w', v', u₂} W D) (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X)))
    (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z)))
w : ForgetEnrichment.homTo W f = ForgetEnrichment.homTo W g
⊢ ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f) = ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g)

Tactic:
apply_fun ForgetEnrichment.homOf W at w

Premises used: CategoryTheory.ForgetEnrichment.homOf
-- 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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
X Y Z : ForgetEnrichment.{w', v', u₁} W C
f_1 : X ⟶ Y
g_1 : Y ⟶ Z
f g :
  Quiver.Hom (V := ForgetEnrichment.{w', v', u₂} W D) (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W X)))
    (ForgetEnrichment.of W (F.obj (ForgetEnrichment.to W Z)))
w : ForgetEnrichment.homOf W (ForgetEnrichment.homTo W f) = ForgetEnrichment.homOf W (ForgetEnrichment.homTo W g)
⊢ f = g

Tactic:
simpa using w
-- 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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
F : EnrichedFunctor.{w', v', u₁, u₂} W C D
G : EnrichedFunctor.{w', v', u₂, u₃} W D E
X Y : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
⊢ (comp W F G).forget.map f ≫
      Iso.hom
        ((fun (x : ForgetEnrichment.{w', v', u₁} W C) ↦
            (Iso.refl ((comp W F G).forget.obj x) : (comp W F G).forget.obj x ≅ (comp W F G).forget.obj x))
          Y) =
    Iso.hom
        ((fun (x : ForgetEnrichment.{w', v', u₁} W C) ↦
            (Iso.refl ((comp W F G).forget.obj x) : (comp W F G).forget.obj x ≅ (comp W F G).forget.obj x))
          X) ≫
      (F.forget ⋙ G.forget).map f

Tactic:
simp [comp, forget]

Premises used: CategoryTheory.EnrichedFunctor.forget, CategoryTheory.EnrichedFunctor.comp
-- 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
W : Type v'
inst_3 : Category.{w', v'} W
inst_4 : MonoidalCategory.{w', v'} W
C : Type u₁
inst_5 : EnrichedCategory.{w', v', u₁} W C
D : Type u₂
inst_6 : EnrichedCategory.{w', v', u₂} W D
E : Type u₃
inst_7 : EnrichedCategory.{w', v', u₃} W E
X Y : ForgetEnrichment.{w', v', u₁} W C
f : X ⟶ Y
⊢ Eq (α := Functor.obj (forget (id W C)) X ⟶ Functor.obj.{w', w', u₁, u₁} (𝟭 (ForgetEnrichment.{w', v', u₁} W C)) Y)
    (Functor.map (forget (id W C)) f ≫
      Iso.hom
        ((fun (x : ForgetEnrichment.{w', v', u₁} W C) ↦
            (Iso.refl (Functor.obj (forget (id W C)) x) :
              Functor.obj (forget (id W C)) x ≅ Functor.obj (forget (id W C)) x))
          Y))
    (Iso.hom
        ((fun (x : ForgetEnrichment.{w', v', u₁} W C) ↦
            (Iso.refl (Functor.obj (forget (id W C)) x) :
              Functor.obj (forget (id W C)) x ≅ Functor.obj (forget (id W C)) x))
          X) ≫
      Functor.map (𝟭 (ForgetEnrichment.{w', v', u₁} W C)) f)

Tactic:
simp [forget]

Premises used: CategoryTheory.EnrichedFunctor.forget
-- Module: Mathlib.CategoryTheory.Enriched.Basic
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
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
α β : F ⟶ G
h : ∀ (X : C), α.out.app X = β.out.app X
rcases :
  ∀ (α : F.forget ⟶ G.forget) (h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = β.out.app X),
    { out := α : EnrichedNatTrans F G } = β
⊢ α = β

Tactic:
rcases α with ⟨α⟩
-- Module: Mathlib.CategoryTheory.Enriched.Basic
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
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
β : F ⟶ G
α : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = β.out.app X
rcases :
  ∀ (β : F.forget ⟶ G.forget) (h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = { out := β }.out.app X),
    { out := α : EnrichedNatTrans F G } = { out := β }
⊢ { out := α : EnrichedNatTrans F G } = β

Tactic:
rcases β with ⟨β⟩
-- Module: Mathlib.CategoryTheory.Enriched.Basic
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
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = { out := β }.out.app X
e_out : α = β
⊢ { out := α : EnrichedNatTrans F G } = { out := β }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Enriched.Basic
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
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = { out := β }.out.app X
e_out : ∀ (x : ForgetEnrichment.{w, v, u₁} V C), α.app x = β.app x
⊢ α = β

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Enriched.Basic
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
F G : EnrichedFunctor.{w, v, u₁, u₂} V C D
α β : F.forget ⟶ G.forget
h : ∀ (X : C), { out := α : EnrichedNatTrans F G }.out.app X = { out := β }.out.app X
x : ForgetEnrichment.{w, v, u₁} V C
⊢ α.app x = β.app x

Tactic:
apply h
-- Module: Mathlib.CategoryTheory.Enriched.Basic
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
⊢ Iso.hom
        (HalfBraiding.β
          (Sigma.snd (β := fun (X : V) ↦ HalfBraiding.{w, v} X) (Functor.obj (Center.ofBraided V) (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)

Tactic:
have p := σ.naturality X Y
-- Module: Mathlib.CategoryTheory.Enriched.Basic
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
        (HalfBraiding.β
          (Sigma.snd (β := fun (X : V) ↦ HalfBraiding.{w, v} X) (Functor.obj (Center.ofBraided V) (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)
dsimp :
  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)
⊢ Iso.hom
        (HalfBraiding.β
          (Sigma.snd (β := fun (X : V) ↦ HalfBraiding.{w, v} X) (Functor.obj (Center.ofBraided V) (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)

Tactic:
dsimp at p ⊢
-- 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 u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : Functor.{v, v, u₁, u₂} C D
X : C
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)
⊢ 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))

Tactic:
ext ⟨⟩
-- 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 u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : Functor.{v, v, u₁, u₂} C D
X : C
⊢ 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:
F.map_id X

Premises used: CategoryTheory.Functor.map_id
-- 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 u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : Functor.{v, v, u₁, u₂} C D
X : C
⊢ 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:
exact F.map_id X

Premises used: CategoryTheory.Functor.map_id
-- 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 u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : Functor.{v, v, u₁, u₂} C D
X Y Z : C
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))
⊢ 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)))

Tactic:
ext ⟨f, g⟩
-- 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 u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : Functor.{v, v, u₁, u₂} C D
X Y Z : C
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:
F.map_comp f g

Premises used: CategoryTheory.Functor.map_comp
-- 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 u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : Functor.{v, v, u₁, u₂} C D
X Y Z : C
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:
exact F.map_comp f g

Premises used: CategoryTheory.Functor.map_comp
-- 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:
(σ.hom x).naturality f

Premises used: CategoryTheory.NatTrans.naturality, TypeCat.Hom.hom, DFunLike.coe