awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_7 : F.OplaxMonoidal
inst_8 : G.OplaxMonoidal
X Y Z : C
dsimp :
  Eq (α :=
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj X))
        (tensorObj.{v₃, u₃} (𝒞 := inst_4) (G.obj (F.obj Y)) (G.obj (F.obj Z))))
    (CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)))
        (G.map (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
        (δ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
            (δ G (F.obj X) (F.obj Y)) ▷
          G.obj (F.obj Z) ≫
        Iso.hom (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))))
    (G.map (F.map (Iso.hom (α_ X Y Z))) ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))))
          (G.map (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
          (δ G (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
        G.obj (F.obj X) ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) (G.map (δ F Y Z))
            (δ G (F.obj Y) (F.obj Z)))
⊢ Eq (α :=
    (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X)
        (tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj Y) ((F ⋙ G).obj Z)))
    (CategoryStruct.comp (Y :=
        G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)))
        (G.map (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z))
        (δ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
            (δ G (F.obj X) (F.obj Y)) ▷
          (F ⋙ G).obj Z ≫
        Iso.hom (α_ ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ((F ⋙ G).obj Z)))
    ((F ⋙ G).map (Iso.hom (α_ X Y Z)) ≫
      CategoryStruct.comp (Y :=
          G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))))
          (G.map (δ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
          (δ G (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))) ≫
        (F ⋙ G).obj X ◁
          CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) (G.map (δ F Y Z))
            (δ G (F.obj Y) (F.obj Z)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
⊢ IsIso (X := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F)

Tactic:
(εIso F).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Functor.Monoidal.εIso
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
⊢ IsIso (X := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F)

Tactic:
(εIso F).isIso_inv

Premises used: CategoryTheory.Iso.isIso_inv, CategoryTheory.Functor.Monoidal.εIso
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
X Y : C
⊢ IsIso (X := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ F X Y)

Tactic:
(μIso F X Y).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Functor.Monoidal.μIso
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
X Y : C
⊢ IsIso (X := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (δ F X Y)

Tactic:
(μIso F X Y).isIso_inv

Premises used: CategoryTheory.Iso.isIso_inv, CategoryTheory.Functor.Monoidal.μIso
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
C' : Type u₁'
inst_4 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : F.Monoidal
G : Functor.{v₂, v₁', u₂, u₁'} D C'
⊢ CategoryStruct.comp (Y := G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (G.map (ε F)) (G.map (η F)) =
    𝟙 (G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))

Tactic:
(εIso F).map_hom_inv_id G

Premises used: CategoryTheory.Iso.map_hom_inv_id, CategoryTheory.Functor.Monoidal.εIso
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
C' : Type u₁'
inst_4 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : F.Monoidal
G : Functor.{v₂, v₁', u₂, u₁'} D C'
⊢ CategoryStruct.comp (Y := G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (G.map (η F)) (G.map (ε F)) =
    𝟙 (G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
(εIso F).map_inv_hom_id G

Premises used: CategoryTheory.Iso.map_inv_hom_id, CategoryTheory.Functor.Monoidal.εIso
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
C' : Type u₁'
inst_4 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : F.Monoidal
G : Functor.{v₂, v₁', u₂, u₁'} D C'
X Y : C
⊢ CategoryStruct.comp (Y := G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))) (G.map (μ F X Y)) (G.map (δ F X Y)) =
    𝟙 (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))

Tactic:
(μIso F X Y).map_hom_inv_id G

Premises used: CategoryTheory.Iso.map_hom_inv_id, CategoryTheory.Functor.Monoidal.μIso
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
C' : Type u₁'
inst_4 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : F.Monoidal
G : Functor.{v₂, v₁', u₂, u₁'} D C'
X Y : C
⊢ CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
      (G.map (μ F X Y)) =
    𝟙 (G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))

Tactic:
(μIso F X Y).map_inv_hom_id G

Premises used: CategoryTheory.Iso.map_inv_hom_id, CategoryTheory.Functor.Monoidal.μIso
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
rw :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
rw₁ :
  𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
rw₂ rw₃ :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T) (ε F ▷ T)
      (η F ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T)

Tactic:
rw [← MonoidalCategory.comp_whiskerRight, ε_η, id_whiskerRight]

Premises used: CategoryTheory.Functor.Monoidal.ε_η, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.id_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
rw :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (ε F) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
rw₁ :
  𝟙 (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
rw₂ rw₃ :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) T) (η F ▷ T)
      (ε F ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) T)

Tactic:
rw [← MonoidalCategory.comp_whiskerRight, η_ε, id_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.Functor.Monoidal.η_ε
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y) (δ F X Y) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
rw₁ :
  𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
rw₂ rw₃ :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
      (μ F X Y ▷ T) (δ F X Y ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)

Tactic:
rw [← MonoidalCategory.comp_whiskerRight, μ_δ, id_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.Functor.Monoidal.μ_δ
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (μ F X Y) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
rw₁ :
  𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ▷ T =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
rw₂ rw₃ :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) T)
      (δ F X Y ▷ T) (μ F X Y ▷ T) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) T)

Tactic:
rw [← MonoidalCategory.comp_whiskerRight, δ_μ, id_whiskerRight]

Premises used: CategoryTheory.Functor.Monoidal.δ_μ, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.id_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
rw :
  T ◁ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
rw₁ :
  T ◁ 𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
rw₂ rw₃ :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (T ◁ ε F)
      (T ◁ η F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, ε_η, MonoidalCategory.whiskerLeft_id]

Premises used: CategoryTheory.Functor.Monoidal.ε_η, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.whiskerLeft_id
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
T : D
rw :
  T ◁ CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (ε F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
rw₁ :
  T ◁ 𝟙 (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
rw₂ rw₃ :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (T ◁ η F)
      (T ◁ ε F) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, η_ε, MonoidalCategory.whiskerLeft_id]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.Functor.Monoidal.η_ε
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  T ◁ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y) (δ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
rw₁ :
  T ◁ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
rw₂ rw₃ :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (T ◁ μ F X Y) (T ◁ δ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, μ_δ, MonoidalCategory.whiskerLeft_id]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.Functor.Monoidal.μ_δ
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
T : D
rw :
  T ◁ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (μ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
rw₁ :
  T ◁ 𝟙 (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
rw₂ rw₃ :
  Eq.{v₂ + 1} (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))))
    (𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))))
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) T (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
      (T ◁ δ F X Y) (T ◁ μ F X Y) =
    𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) T (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, δ_μ, MonoidalCategory.whiskerLeft_id]

Premises used: CategoryTheory.Functor.Monoidal.δ_μ, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.whiskerLeft_id
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X') ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Y')) (F.map (f ⊗ₘ g))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj X')) (δ F X X')
      ((F.map f ⊗ₘ F.map g) ≫ μ F Y Y'))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
f : Y ⟶ Z
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)) (F.map (X ◁ f))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y)
      (F.obj X ◁ F.map f ≫ μ F X Z))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Z) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) (F.map (f ▷ Z))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Z)) (δ F X Z)
      (F.map f ▷ F.obj Z ≫ μ F Y Z))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y Z : C
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z))
        (δ F X Y ▷ F.obj Z)
        (μ F X Y ▷ F.obj Z ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z)))))
rw₁ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.map (Iso.hom (α_ X Y Z))))
rw₂ rw₃ :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z))) (F.map (Iso.hom (α_ X Y Z)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (F.map (Iso.hom (α_ X Y Z)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)
      (δ F X Y ▷ F.obj Z ≫
        Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫ F.obj X ◁ μ F Y Z ≫ μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))

Tactic:
rw [← LaxMonoidal.associativity F, whiskerRight_δ_μ_assoc, δ_μ_assoc]

Premises used: CategoryTheory.Functor.LaxMonoidal.associativity, CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc, CategoryTheory.Functor.Monoidal.δ_μ_assoc