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_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
h₁ :
  Eq (α :=
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).1 ⟶
      ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).1)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))
        (δ (F.prod' G) x x_1) (μ (F.prod' G) x x_1)).1
    (𝟙 ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1))).1
h₂ :
  Eq (α :=
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).2 ⟶
      ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).2)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))
        (δ (F.prod' G) x x_1) (μ (F.prod' G) x x_1)).2
    (𝟙 ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1))).2
⊢ CategoryStruct.comp (Y :=
      tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))
      (δ (F.prod' G) x x_1) (μ (F.prod' G) x x_1) =
    𝟙 ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1))

Tactic:
ext
-- 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_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
⊢ Eq (α :=
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).1 ⟶
      ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).1)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))
        (δ (F.prod' G) x x_1) (μ (F.prod' G) x x_1)).1
    (𝟙 ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1))).1

Tactic:
simp only [CategoryTheory.prod_comp_fst, prod'_μ_fst, prod'_δ_fst, δ_μ,
        prod'_obj, prod_id]

Premises used: CategoryTheory.Functor.prod'_μ_fst, CategoryTheory.Functor.Monoidal.δ_μ, CategoryTheory.prod_id, CategoryTheory.Functor.prod'_obj, CategoryTheory.Functor.prod'_δ_fst, CategoryTheory.prod_comp_fst
-- 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_1 F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₁, v₃, u₁, u₃} C E
inst_7 : F.Monoidal
inst_8 : G.Monoidal
x x_1 : C
⊢ Eq (α :=
    ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).2 ⟶
      ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1)).2)
    (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' G).obj x) ((F.prod' G).obj x_1))
        (δ (F.prod' G) x x_1) (μ (F.prod' G) x x_1)).2
    (𝟙 ((F.prod' G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1))).2

Tactic:
simp only [CategoryTheory.prod_comp_snd, prod'_μ_snd, prod'_δ_snd, δ_μ,
        prod'_obj, prod_id]

Premises used: CategoryTheory.Functor.prod'_δ_snd, CategoryTheory.Functor.Monoidal.δ_μ, CategoryTheory.prod_id, CategoryTheory.Functor.prod'_obj, CategoryTheory.Functor.prod'_μ_snd, CategoryTheory.prod_comp_snd
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
simp :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
    (G.map f ▷ G.obj X' ≫
      ((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj X')) (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X') :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X')
              (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))) :
          (a : F.obj (G.obj Y ⊗ G.obj X') ⟶ Y ⊗ X') → G.obj Y ⊗ G.obj X' ⟶ G.obj (Y ⊗ X'))
        (δ F (G.obj Y) (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')))
    (((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X X') :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X X')
              (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X X'))) :
          (a : F.obj (G.obj X ⊗ G.obj X') ⟶ X ⊗ X') → G.obj X ⊗ G.obj X' ⟶ G.obj (X ⊗ X'))
        (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X')) ≫
      G.map (f ▷ X'))

Tactic:
simp only [Adjunction.homEquiv_apply, ← adj.unit_naturality_assoc, ← G.map_comp, assoc,
      ← δ_natural_left_assoc F]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc, CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_apply, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.unit_naturality_assoc
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X')
    (F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X'))
    ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')
rw rw₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))

Tactic:
rw [this]
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
suffices :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X')
    (F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X'))
    ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'))

Tactic:
suffices F.map (G.map f) ▷ F.obj (G.obj X') ≫ _ =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X')
    (F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X'))
    ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')

Tactic:
simpa using NatTrans.whiskerRight_app_tensor_app adj.counit adj.counit (f := f) X'

Premises used: CategoryTheory.NatTrans.whiskerRight_app_tensor_app, CategoryTheory.Adjunction.counit
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
simp :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
    (G.obj X ◁ G.map g ≫
      ((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y')) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y') :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y')
              (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))) :
          (a : F.obj (G.obj X ⊗ G.obj Y') ⟶ X ⊗ Y') → G.obj X ⊗ G.obj Y' ⟶ G.obj (X ⊗ Y'))
        (δ F (G.obj X) (G.obj Y') ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')))
    (((adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X X') :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X X')
              (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X X'))) :
          (a : F.obj (G.obj X ⊗ G.obj X') ⟶ X ⊗ X') → G.obj X ⊗ G.obj X' ⟶ G.obj (X ⊗ X'))
        (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X')) ≫
      G.map (X ◁ g))

Tactic:
simp only [Adjunction.homEquiv_apply, ← adj.unit_naturality_assoc, ← G.map_comp,
      assoc, ← δ_natural_right_assoc F]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_apply, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc, CategoryTheory.Adjunction.unit_naturality_assoc
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
this :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y')
    (F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y'))
    ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)
rw rw₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))

Tactic:
rw [this]
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
suffices :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y')
    (F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y'))
    ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X') ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y'))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y')))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj X')) ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g))

Tactic:
suffices F.obj (G.obj X) ◁ F.map (G.map g) ≫ _ =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj X')) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y')
    (F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y'))
    ((adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g)

Tactic:
simpa using NatTrans.whiskerLeft_app_tensor_app adj.counit adj.counit (f := g) _

Premises used: CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.whiskerLeft_app_tensor_app
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y Z : D
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (δ F (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z) ≫
      F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
        F.map (G.map (δ F (G.obj X) (G.obj Y))) ▷ F.obj (G.obj Z) ≫
          F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y)) ▷ F.obj (G.obj Z) ≫
            (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) ⊗ₘ adj.counit.app Z) ≫ Iso.hom (α_ X Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
      F.map (G.map (δ F (G.obj X) (G.obj Y)) ▷ G.obj Z) ≫
        F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app Y) ▷ G.obj Z) ≫
          δ F (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (G.obj Z) ≫
            (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) ⊗ₘ adj.counit.app Z) ≫ Iso.hom (α_ X Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))

Tactic:
rw [← δ_natural_left_assoc, ← δ_natural_left_assoc, ← δ_natural_left_assoc]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y Z : D
⊢ ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D}
    (h : tensorObj.{v₂, u₂} (𝒞 := inst_2) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X') ⟶ Z),
    (G ⋙ F).map f ▷ (G ⋙ F).obj X' ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ map (𝟭 D) f ▷ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X' ≫ h

Tactic:
haveI := @NatTrans.whiskerRight_app_tensor_app_assoc _ _ _ _ _ _ _ _ _ adj.counit adj.counit
-- 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 C
adj : F ⊣ G
inst_7 : F.OplaxMonoidal
X Y Z : D
this :
  ∀ {X Y : D} (f : X ⟶ Y) (X' : D) {Z : D} (h : tensorObj.{v₂, u₂} (𝒞 := inst_2) Y X' ⟶ Z),
    F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') ≫ h =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X' ≫ h
rw :
  Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
        F.obj (G.obj X) ◁ F.map (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
          F.obj (G.obj X) ◁ F.map (G.map (δ F (G.obj Y) (G.obj Z))) ≫
            F.obj (G.obj X) ◁ F.map (G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) (G.obj Z)) ⟶
      tensorObj.{v₂, u₂} (𝒞 := inst_2) X (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      δ F (G.obj X) (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z)) ≫
        F.obj (G.obj X) ◁ δ F (G.obj Y) (G.obj Z) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y ⊗ₘ adj.counit.app Z))
    (F.map (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z))) ≫
      F.map (G.obj X ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj Y) (G.obj Z))) ≫
        F.map (G.obj X ◁ G.map (δ F (G.obj Y) (G.obj Z))) ≫
          F.map (G.obj X ◁ G.map (adj.counit.app Y ⊗ₘ adj.counit.app Z)) ≫
            δ F (G.obj X) (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
              (adj.counit.app X ⊗ₘ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)))

Tactic:
rw [← δ_natural_right_assoc, ← δ_natural_right_assoc, ← δ_natural_right_assoc]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc