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 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
nth_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 ▷ F.obj (G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) Y Z)) ≫
                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 (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)))

Tactic:
nth_rw 4 [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- 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
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
leftAdjoint_ε :
  autoParam
    (Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G)
      (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ G.map (η F)))
    IsMonoidal.leftAdjoint_ε._autoParam
leftAdjoint_μ :
  autoParam
    (∀ (X Y : D),
      Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
        (μ G X Y)
        (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ≫
          G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y))))
    IsMonoidal.leftAdjoint_μ._autoParam
⊢ adj.IsMonoidal

Tactic:
constructor
-- 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
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
⊢ autoParam
    (Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G)
      (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ G.map (η F)))
    IsMonoidal.leftAdjoint_ε._autoParam

Tactic:
rfl
-- 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
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
X : D
leftAdjoint_μ :
  ∀ (Y : D),
    Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
      (μ G X Y)
      (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ≫
        G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)))
⊢ ∀ (Y : D),
    Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
      (μ G X Y)
      (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ≫
        G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)))

Tactic:
_
-- 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
this : G.LaxMonoidal := adj.rightAdjointLaxMonoidal
X Y : D
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (μ G X Y)
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ≫
      G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)))

Tactic:
rfl
-- 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
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.OplaxMonoidal
inst_5 : G.LaxMonoidal
inst_6 : adj.IsMonoidal
⊢ Eq (α := obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ G.map (η F)) (ε G)

Tactic:
Adjunction.IsMonoidal.leftAdjoint_ε.symm

Premises used: CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_ε, Eq.symm
-- 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
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.OplaxMonoidal
inst_5 : G.LaxMonoidal
inst_6 : adj.IsMonoidal
X Y : C
⊢ Eq (α :=
    obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ G.map (δ F X Y))
    ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y))

Tactic:
simp [IsMonoidal.leftAdjoint_μ (adj := adj), ← adj.unit_naturality_assoc,
    ← Functor.map_comp, ← δ_natural_assoc]

Premises used: CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_μ, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.OplaxMonoidal.δ_natural_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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.OplaxMonoidal
inst_5 : G.LaxMonoidal
inst_6 : adj.IsMonoidal
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (F.map (ε G) ≫ adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (η F)

Tactic:
simp [IsMonoidal.leftAdjoint_ε (adj := adj)]

Premises used: CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_ε
-- 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
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_4 : F.OplaxMonoidal
inst_5 : G.LaxMonoidal
inst_6 : adj.IsMonoidal
X Y : D
⊢ Eq (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y)) ⟶
      obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (F.map (μ G X Y) ≫ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y))

Tactic:
simp [IsMonoidal.leftAdjoint_μ (adj := adj)]

Premises used: CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_μ
-- 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
inst_8 : G.LaxMonoidal
inst_9 : adj.IsMonoidal
F' : Functor.{v₂, v₃, u₂, u₃} D E
G' : Functor.{v₃, v₂, u₃, u₂} E D
adj' : F' ⊣ G'
inst_10 : F'.OplaxMonoidal
inst_11 : G'.LaxMonoidal
inst_12 : adj'.IsMonoidal
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (G' ⋙ G).obj (tensorUnit.{v₃, u₃} E (𝒞 := inst_4))) (ε (G' ⋙ G))
    ((adj.comp adj').unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ (G' ⋙ G).map (η (F ⋙ F')))

Tactic:
simp [IsMonoidal.leftAdjoint_ε (adj := adj'), IsMonoidal.leftAdjoint_ε (adj := adj),
      ← map_comp, ← adj'.unit_naturality_assoc]

Premises used: CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_ε, 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
inst_8 : G.LaxMonoidal
inst_9 : adj.IsMonoidal
F' : Functor.{v₂, v₃, u₂, u₃} D E
G' : Functor.{v₃, v₂, u₃, u₂} E D
adj' : F' ⊣ G'
inst_10 : F'.OplaxMonoidal
inst_11 : G'.LaxMonoidal
inst_12 : adj'.IsMonoidal
X Y : E
simp :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y)) ⟶
      G.obj (G'.obj (tensorObj.{v₃, u₃} (𝒞 := inst_4) X Y)))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y))) ≫
      G.map
        (CategoryStruct.comp (Y :=
          tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj (G'.obj X))) (F.obj (G.obj (G'.obj Y))))
          (δ F (G.obj (G'.obj X)) (G.obj (G'.obj Y)))
          ((adj.counit.app (G'.obj X) ⊗ₘ adj.counit.app (G'.obj Y)) ≫
            adj'.unit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G'.obj X) (G'.obj Y)) ≫
              G'.map (δ F' (G'.obj X) (G'.obj Y) ≫ (adj'.counit.app X ⊗ₘ adj'.counit.app Y)))))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y))) ≫
      G.map
        (adj'.unit.app (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y)))) ≫
          G'.map
            (CategoryStruct.comp (Y :=
              F'.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj (G'.obj X))) (F.obj (G.obj (G'.obj Y)))))
              (F'.map (δ F (G.obj (G'.obj X)) (G.obj (G'.obj Y))))
              (F'.map (adj.counit.app (G'.obj X) ⊗ₘ adj.counit.app (G'.obj Y)) ≫
                δ F' (G'.obj X) (G'.obj Y) ≫ (adj'.counit.app X ⊗ₘ adj'.counit.app Y)))))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) ((G' ⋙ G).obj X) ((G' ⋙ G).obj Y) ⟶
      (G' ⋙ G).obj (tensorObj.{v₃, u₃} (𝒞 := inst_4) X Y))
    (μ (G' ⋙ G) X Y)
    ((adj.comp adj').unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) ((G' ⋙ G).obj X) ((G' ⋙ G).obj Y)) ≫
      (G' ⋙ G).map
        (δ (F ⋙ F') ((G' ⋙ G).obj X) ((G' ⋙ G).obj Y) ≫ ((adj.comp adj').counit.app X ⊗ₘ (adj.comp adj').counit.app Y)))

Tactic:
simp only [comp_obj, comp_μ, IsMonoidal.leftAdjoint_μ (adj := adj), id_obj,
      IsMonoidal.leftAdjoint_μ (adj := adj'), assoc, ← map_comp, comp_unit_app, comp_δ,
      comp_counit_app, ← tensorHom_comp_tensorHom, δ_natural_assoc, Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_μ, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Adjunction.comp_counit_app, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.OplaxMonoidal.δ_natural_assoc, CategoryTheory.Functor.LaxMonoidal.comp_μ, CategoryTheory.Functor.OplaxMonoidal.comp_δ, CategoryTheory.Functor.comp_map, CategoryTheory.Adjunction.comp_unit_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
inst_8 : G.LaxMonoidal
inst_9 : adj.IsMonoidal
F' : Functor.{v₂, v₃, u₂, u₃} D E
G' : Functor.{v₃, v₂, u₃, u₂} E D
adj' : F' ⊣ G'
inst_10 : F'.OplaxMonoidal
inst_11 : G'.LaxMonoidal
inst_12 : adj'.IsMonoidal
X Y : E
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y)) ⟶
      G.obj (G'.obj (tensorObj.{v₃, u₃} (𝒞 := inst_4) X Y)))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y))) ≫
      G.map
        (CategoryStruct.comp (Y :=
          tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj (G'.obj X))) (F.obj (G.obj (G'.obj Y))))
          (δ F (G.obj (G'.obj X)) (G.obj (G'.obj Y)))
          ((adj.counit.app (G'.obj X) ⊗ₘ adj.counit.app (G'.obj Y)) ≫
            adj'.unit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G'.obj X) (G'.obj Y)) ≫
              G'.map (δ F' (G'.obj X) (G'.obj Y) ≫ (adj'.counit.app X ⊗ₘ adj'.counit.app Y)))))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y))) ≫
      G.map
        (adj'.unit.app (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj (G'.obj X)) (G.obj (G'.obj Y)))) ≫
          G'.map
            (CategoryStruct.comp (Y :=
              F'.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj (G'.obj X))) (F.obj (G.obj (G'.obj Y)))))
              (F'.map (δ F (G.obj (G'.obj X)) (G.obj (G'.obj Y))))
              (F'.map (adj.counit.app (G'.obj X) ⊗ₘ adj.counit.app (G'.obj Y)) ≫
                δ F' (G'.obj X) (G'.obj Y) ≫ (adj'.counit.app X ⊗ₘ adj'.counit.app 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
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 : G.LaxMonoidal
X Y : C
x : X ⟶ Y
x_1 : C
⊢ Eq.{v₂ + 1} (α :=
    F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))
    (((Equiv.symm
              (adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1)
                (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))) :
            Equiv.{v₁ + 1, v₂ + 1}
              (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1 ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))) :
          (a : X ⊗ x_1 ⟶ G.obj (F.obj Y ⊗ F.obj x_1)) → F.obj (X ⊗ x_1) ⟶ F.obj Y ⊗ F.obj x_1)
        ((adj.unit.app X ⊗ₘ adj.unit.app x_1) ≫ G.map (F.map x) ▷ G.obj (F.obj x_1) ≫ μ G (F.obj Y) (F.obj x_1)) :
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))
    (((Equiv.symm
              (adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1)
                (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))) :
            Equiv.{v₁ + 1, v₂ + 1}
              (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1 ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1)))
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))) :
          (a : X ⊗ x_1 ⟶ G.obj (F.obj Y ⊗ F.obj x_1)) → F.obj (X ⊗ x_1) ⟶ F.obj Y ⊗ F.obj x_1)
        (x ▷ x_1 ≫ (adj.unit.app Y ⊗ₘ adj.unit.app x_1) ≫ μ G (F.obj Y) (F.obj x_1)) :
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj x_1))

Tactic:
simp [← tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_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
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 : G.LaxMonoidal
X Y x : C
x_1 : X ⟶ Y
⊢ Eq.{v₂ + 1} (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
    (((Equiv.symm
              (adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) x X)
                (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) :
            Equiv.{v₁ + 1, v₂ + 1}
              (tensorObj.{v₁, u₁} (𝒞 := inst) x X ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y)))
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) :
          (a : x ⊗ X ⟶ G.obj (F.obj x ⊗ F.obj Y)) → F.obj (x ⊗ X) ⟶ F.obj x ⊗ F.obj Y)
        ((adj.unit.app x ⊗ₘ adj.unit.app X) ≫ G.obj (F.obj x) ◁ G.map (F.map x_1) ≫ μ G (F.obj x) (F.obj Y)) :
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
    (((Equiv.symm
              (adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) x X)
                (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) :
            Equiv.{v₁ + 1, v₂ + 1}
              (tensorObj.{v₁, u₁} (𝒞 := inst) x X ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y)))
              (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))) :
          (a : x ⊗ X ⟶ G.obj (F.obj x ⊗ F.obj Y)) → F.obj (x ⊗ X) ⟶ F.obj x ⊗ F.obj Y)
        (x ◁ x_1 ≫ (adj.unit.app x ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj x) (F.obj Y)) :
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x X) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))

Tactic:
simp [← id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom
-- 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 : G.LaxMonoidal
X Y Z : C
rw :
  tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ (F ⋙ G).obj Z ≫
      (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫
              G.map (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))) ▷
          G.obj (F.obj Z) ≫
        μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ≫
          G.map (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
| (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ adj.unit.app Z) ≫
    CategoryStruct.comp (Y :=
      G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z)))
      (μ G (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (F.obj Z))
      (G.map
        (((Equiv.symm
                    (adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)
                      (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) :
                  Equiv.{v₁ + 1, v₂ + 1}
                    (tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))
                    (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
                      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) :
                (a : X ⊗ Y ⟶ G.obj (F.obj X ⊗ F.obj Y)) → F.obj (X ⊗ Y) ⟶ F.obj X ⊗ F.obj Y)
              ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
            F.obj Z ≫
          Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z))))

Tactic:
rw [homEquiv_counit, map_comp_assoc, map_comp,
        ← μ_natural_left_assoc, map_comp, map_comp, tensorHom_def'_assoc]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def'_assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.homEquiv_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 : G.LaxMonoidal
X Y Z : C
dsimp :
  tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj (F.obj Z) ≫
      (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫
              G.map (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))) ▷
          G.obj (F.obj Z) ≫
        μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ≫
          G.map (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))
| tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ (F ⋙ G).obj Z ≫
      (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
            G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫
              G.map (adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)))) ▷
          G.obj (F.obj Z) ≫
        μ G (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (F.obj Z) ≫
          G.map (Iso.hom (α_ (F.obj X) (F.obj Y) (F.obj Z)))

Tactic:
dsimp