awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
dsimp :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    (NatTrans.app μ X ≫ A.map f : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (Mon.X (functorObjObj A X)) (Mon.X (functorObjObj A X)) ⟶
      Mon.X (functorObjObj A Y))
    (μ ≫ A.map f) ((A.map f ⊗ₘ A.map f) ≫ μ)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y : C
f : X ⟶ Y
rw :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    ((tensorObj (𝒞 := Functor.category) A A).map f ≫ NatTrans.app μ Y) ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y)
rw₁ rw₂ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y) ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y)
    ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y)
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    (NatTrans.app μ X ≫ A.map f : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)
    ((A.map f ⊗ₘ A.map f) ≫ NatTrans.app μ Y : tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X) ⟶ A.obj Y)

Tactic:
rw [← μ[A].naturality, tensorObj_map]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Monoidal.tensorObj_map, CategoryTheory.MonObj.mul
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X : C
w :
  Eq (α := Mon.X (functorObjObj A X) ⟶ Mon.X (functorObjObj A X))
    (Mon.Hom.hom { hom := A.map (𝟙 X), isMonHom_hom := ⋯ }) (Mon.Hom.hom (𝟙 (functorObjObj A X)))
⊢ Eq (α := Quiver.Hom (V := Mon.{v₂, u₂} D) (functorObjObj A X) (functorObjObj A X))
    { hom := A.map (𝟙 X), isMonHom_hom := ⋯ } (𝟙 (functorObjObj A X))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X : C
w : A.map (𝟙 X) = 𝟙 (A.obj X)
⊢ Eq (α := Mon.X (functorObjObj A X) ⟶ Mon.X (functorObjObj A X))
    (Mon.Hom.hom { hom := A.map (𝟙 X), isMonHom_hom := ⋯ }) (Mon.Hom.hom (𝟙 (functorObjObj A X)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X : C
w w₁ : Eq.{v₂ + 1} (α := A.obj X ⟶ A.obj X) (𝟙 (A.obj X)) (𝟙 (A.obj X))
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)

Tactic:
rw [CategoryTheory.Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w :
  Eq.{v₂ + 1} (α := Mon.X (functorObjObj A X) ⟶ Mon.X (functorObjObj A Z))
    (Mon.Hom.hom { hom := A.map (f ≫ g), isMonHom_hom := ⋯ })
    (Mon.Hom.hom
      (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isMonHom_hom := ⋯ }
        { hom := A.map g, isMonHom_hom := ⋯ }))
⊢ Eq.{v₂ + 1} (α := Quiver.Hom (V := Mon.{v₂, u₂} D) (functorObjObj A X) (functorObjObj A Z))
    { hom := A.map (f ≫ g), isMonHom_hom := ⋯ }
    (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isMonHom_hom := ⋯ }
      { hom := A.map g, isMonHom_hom := ⋯ })

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : A.map (f ≫ g) = A.map f ≫ A.map g
⊢ Eq.{v₂ + 1} (α := Mon.X (functorObjObj A X) ⟶ Mon.X (functorObjObj A Z))
    (Mon.Hom.hom { hom := A.map (f ≫ g), isMonHom_hom := ⋯ })
    (Mon.Hom.hom
      (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isMonHom_hom := ⋯ }
        { hom := A.map g, isMonHom_hom := ⋯ }))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : MonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w w₁ : A.map f ≫ A.map g = A.map f ≫ A.map g
⊢ A.map (f ≫ g) = A.map f ≫ A.map g

Tactic:
rw [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
dsimp :
  Eq (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (A.map f ≫ NatTrans.app ε Y : A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (NatTrans.app ε X :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
⊢ Eq (α := Comon.X (functorObjObj A X) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) (A.map f ≫ ε) ε

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
rw :
  Eq.{v₂ + 1} (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X) (NatTrans.app ε X)
        (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1))) :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y)
    (NatTrans.app ε X :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
⊢ Eq (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (A.map f ≫ NatTrans.app ε Y : A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (NatTrans.app ε X :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)

Tactic:
rw [ε[A].naturality, tensorUnit_map]

Premises used: CategoryTheory.Monoidal.tensorUnit_map, CategoryTheory.ComonObj.counit, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
dsimp :
  Eq.{v₂ + 1} (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
        (NatTrans.app ε X :
          A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
        (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1))) :
      A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (NatTrans.app ε X :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
⊢ Eq.{v₂ + 1} (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X) (NatTrans.app ε X)
        (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1))) :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) Y)
    (NatTrans.app ε X :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
rw rw₁ :
  Eq.{v₂ + 1} (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (NatTrans.app ε X :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
    (NatTrans.app ε X)
⊢ Eq.{v₂ + 1} (α := A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
        (NatTrans.app ε X :
          A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)
        (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_1))) :
      A.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1))
    (NatTrans.app ε X :
      A.obj X ⟶ Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) X)

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
dsimp :
  Eq (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (A.map f ≫ NatTrans.app Δ Y : A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
        (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f) :
      A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
⊢ Eq (α :=
    Comon.X (functorObjObj A X) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (Comon.X (functorObjObj A Y)) (Comon.X (functorObjObj A Y)))
    (A.map f ≫ Δ) (Δ ≫ (A.map f ⊗ₘ A.map f))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y : C
f : X ⟶ Y
rw :
  Eq (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (NatTrans.app Δ X ≫ (tensorObj (𝒞 := Functor.category) A A).map f)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
      (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f))
rw₁ rw₂ :
  Eq.{v₂ + 1} (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (CategoryStruct.comp (Y := (tensorObj (𝒞 := Functor.category) A A).obj X) (NatTrans.app Δ X) (A.map f ⊗ₘ A.map f))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
      (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f))
⊢ Eq (α := A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (A.map f ≫ NatTrans.app Δ Y : A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj X) (A.obj X))
        (NatTrans.app Δ X : A.obj X ⟶ (tensorObj (𝒞 := Functor.category) A A).obj X) (A.map f ⊗ₘ A.map f) :
      A.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (A.obj Y) (A.obj Y))

Tactic:
rw [Δ[A].naturality, tensorObj_map]

Premises used: CategoryTheory.ComonObj.comul, CategoryTheory.NatTrans.naturality, CategoryTheory.Monoidal.tensorObj_map
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X : C
w :
  Eq (α := Comon.X (functorObjObj A X) ⟶ Comon.X (functorObjObj A X))
    (Comon.Hom.hom { hom := A.map (𝟙 X), isComonHom_hom := ⋯ }) (Comon.Hom.hom (𝟙 (functorObjObj A X)))
⊢ Eq (α := Quiver.Hom (V := Comon.{v₂, u₂} D) (functorObjObj A X) (functorObjObj A X))
    { hom := A.map (𝟙 X), isComonHom_hom := ⋯ } (𝟙 (functorObjObj A X))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X : C
w : A.map (𝟙 X) = 𝟙 (A.obj X)
⊢ Eq (α := Comon.X (functorObjObj A X) ⟶ Comon.X (functorObjObj A X))
    (Comon.Hom.hom { hom := A.map (𝟙 X), isComonHom_hom := ⋯ }) (Comon.Hom.hom (𝟙 (functorObjObj A X)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X : C
w w₁ : Eq.{v₂ + 1} (α := A.obj X ⟶ A.obj X) (𝟙 (A.obj X)) (𝟙 (A.obj X))
⊢ A.map (𝟙 X) = 𝟙 (A.obj X)

Tactic:
rw [CategoryTheory.Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w :
  Eq.{v₂ + 1} (α := Comon.X (functorObjObj A X) ⟶ Comon.X (functorObjObj A Z))
    (Comon.Hom.hom { hom := A.map (f ≫ g), isComonHom_hom := ⋯ })
    (Comon.Hom.hom
      (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isComonHom_hom := ⋯ }
        { hom := A.map g, isComonHom_hom := ⋯ }))
⊢ Eq.{v₂ + 1} (α := Quiver.Hom (V := Comon.{v₂, u₂} D) (functorObjObj A X) (functorObjObj A Z))
    { hom := A.map (f ≫ g), isComonHom_hom := ⋯ }
    (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isComonHom_hom := ⋯ }
      { hom := A.map g, isComonHom_hom := ⋯ })

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w : A.map (f ≫ g) = A.map f ≫ A.map g
⊢ Eq.{v₂ + 1} (α := Comon.X (functorObjObj A X) ⟶ Comon.X (functorObjObj A Z))
    (Comon.Hom.hom { hom := A.map (f ≫ g), isComonHom_hom := ⋯ })
    (Comon.Hom.hom
      (CategoryStruct.comp (Y := functorObjObj A Y) { hom := A.map f, isComonHom_hom := ⋯ }
        { hom := A.map g, isComonHom_hom := ⋯ }))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
A : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ComonObj A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
w w₁ : A.map f ≫ A.map g = A.map f ≫ A.map g
⊢ A.map (f ≫ g) = A.map f ≫ A.map g

Tactic:
rw [Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
w :
  ∀ (x : C),
    Eq.{v₂ + 1} (α :=
      (inverseObj X).X.obj x ⟶
        Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) x)
      (NatTrans.app
        (CategoryStruct.comp (Y := (inverseObj Y).X) { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ε) x)
      (NatTrans.app ε x)
⊢ Eq (α := (inverseObj X).X ⟶ (𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category))
    (CategoryStruct.comp (Y := (inverseObj Y).X) { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ε) ε

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
x : C
w : Eq (α := (X.obj x).X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ((α.app x).hom ≫ ε) ε
⊢ Eq.{v₂ + 1} (α :=
    (inverseObj X).X.obj x ⟶
      Functor.obj.{v₁, v₂, u₁, u₂} ((𝟙_ (Functor.{v₁, v₂, u₁, u₂} C D)) (𝒞 := Functor.category)) x)
    (NatTrans.app
      (CategoryStruct.comp (Y := (inverseObj Y).X) { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ε) x)
    (NatTrans.app ε x)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
x : C
w w₁ : Eq.{v₂ + 1} (α := (X.obj x).X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ε ε
⊢ Eq (α := (X.obj x).X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_1)) ((α.app x).hom ≫ ε) ε

Tactic:
rw [IsComonHom.hom_counit (α.app x).hom]

Premises used: CategoryTheory.IsComonHom.hom_counit, CategoryTheory.NatTrans.app, CategoryTheory.Comon.Hom.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
w :
  ∀ (x : C),
    Eq.{v₂ + 1} (α :=
      (inverseObj X).X.obj x ⟶ (tensorObj (𝒞 := Functor.category) (inverseObj Y).X (inverseObj Y).X).obj x)
      (NatTrans.app ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ≫ Δ) x)
      (NatTrans.app
        (Δ ≫
          ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X } ⊗ₘ
            { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X }))
        x)
⊢ Eq (α := (inverseObj X).X ⟶ tensorObj (𝒞 := Functor.category) (inverseObj Y).X (inverseObj Y).X)
    ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ≫ Δ)
    (Δ ≫
      ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X } ⊗ₘ
        { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X }))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
x : C
w :
  Eq (α := (X.obj x).X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (Y.obj x).X (Y.obj x).X) ((α.app x).hom ≫ Δ)
    (Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom))
⊢ Eq.{v₂ + 1} (α :=
    (inverseObj X).X.obj x ⟶ (tensorObj (𝒞 := Functor.category) (inverseObj Y).X (inverseObj Y).X).obj x)
    (NatTrans.app ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ } ≫ Δ) x)
    (NatTrans.app
      (Δ ≫
        ({ app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X } ⊗ₘ
          { app := fun (X_1 : C) ↦ (α.app X_1).hom, naturality := ⋯ : NatTrans (inverseObj X).X (inverseObj Y).X }))
      x)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
X Y : C ⥤ Comon.{v₂, u₂} D
α : X ⟶ Y
x : C
w w₁ :
  Eq (α := (X.obj x).X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (Y.obj x).X (Y.obj x).X)
    (Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom)) (Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom))
⊢ Eq (α := (X.obj x).X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_1) (Y.obj x).X (Y.obj x).X) ((α.app x).hom ≫ Δ)
    (Δ ≫ ((α.app x).hom ⊗ₘ (α.app x).hom))

Tactic:
rw [IsComonHom.hom_comul (α.app x).hom]

Premises used: CategoryTheory.IsComonHom.hom_comul, CategoryTheory.NatTrans.app, CategoryTheory.Comon.Hom.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F : C ⥤ CommMon.{v₂, u₂} D
w :
  ∀ (X : C),
    Eq (α :=
      (tensorObj (𝒞 := Functor.category)
              (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
              (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X).obj
          X ⟶
        (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X.obj X)
      (NatTrans.app
        (Iso.hom
            (β_ (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
              (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X) ≫
          μ)
        X)
      (NatTrans.app μ X)
⊢ Eq (α :=
    tensorObj (𝒞 := Functor.category)
        (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
        (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X ⟶
      (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X)
    (Iso.hom
        (β_ (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
          (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X) ≫
      μ)
    μ

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F : C ⥤ CommMon.{v₂, u₂} D
X : C
⊢ Eq (α :=
    (tensorObj (𝒞 := Functor.category)
            (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
            (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X).obj
        X ⟶
      (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X.obj X)
    (NatTrans.app
      (Iso.hom
          (β_ (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
            (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X) ≫
        μ)
      X)
    (NatTrans.app μ X)

Tactic:
IsCommMonObj.mul_comm (F.obj X).X

Premises used: CategoryTheory.IsCommMonObj.mul_comm, CategoryTheory.CommMon.X, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : MonoidalCategory.{v₂, u₂} D
inst_3 : BraidedCategory.{v₂, u₂} D
F : C ⥤ CommMon.{v₂, u₂} D
X : C
⊢ Eq (α :=
    (tensorObj (𝒞 := Functor.category)
            (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
            (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X).obj
        X ⟶
      (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X.obj X)
    (NatTrans.app
      (Iso.hom
          (β_ (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X
            (Functor.obj (Equivalence.inverse (monFunctorCategoryEquivalence C D)) (F ⋙ CommMon.forget₂Mon D)).X) ≫
        μ)
      X)
    (NatTrans.app μ X)

Tactic:
exact IsCommMonObj.mul_comm (F.obj X).X

Premises used: CategoryTheory.IsCommMonObj.mul_comm, CategoryTheory.CommMon.X, CategoryTheory.Functor.obj