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 : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
X Y : D
⊢ Eq (α :=
    e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) ⟶
      obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (e.functor.map (μ e.inverse X Y) ≫ e.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (δ e.functor (e.inverse.obj X) (e.inverse.obj Y) ≫ (e.counit.app X ⊗ₘ e.counit.app Y))

Tactic:
e.toAdjunction.map_μ_comp_counit_app_tensor X Y

Premises used: CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor, CategoryTheory.Equivalence.toAdjunction
-- 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 : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
rw :
  Eq (α := e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor)
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)))
    (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor) (ε e.functor))
rw₁ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η e.functor)
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₂ :
  CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
      (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₃ :
  CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
      (e.functor.map (ε e.inverse))
      (e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫
        e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₄ :
  CategoryStruct.comp (Y := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
      (e.functor.map (ε e.inverse)) (e.functor.map (η e.inverse)) =
    𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₅ rw₆ :
  Eq.{v₂ + 1} (α :=
    e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (𝟙 (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
⊢ Eq (α :=
    obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⟶
      e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (e.counitInv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse)) (ε e.functor)

Tactic:
rw [← cancel_epi (η e.functor), Monoidal.η_ε, ← functor_map_ε_inverse_comp_counitIso_hom_app,
    Category.assoc, Iso.hom_inv_id_app_assoc, Monoidal.map_ε_η]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Equivalence.functor, CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.Monoidal.map_ε_η, CategoryTheory.cancel_epi, CategoryTheory.Functor.OplaxMonoidal.η, 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
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
X Y : C
⊢ Eq (α :=
    obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y)) ⟶
      e.functor.obj
        (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))))
    (e.counitInv.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y)) ≫
      e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y)))
    (μ e.functor X Y ≫ e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y))

Tactic:
counitIso_inv_app_tensor_comp_functor_map_δ_inverse e X Y

Premises used: CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse
-- 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 : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ e.inverse.obj (e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (CategoryStruct.comp (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε e.inverse)
      (e.inverse.map (ε e.functor)))
    (e.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
e.toAdjunction.ε_comp_map_ε

Premises used: CategoryTheory.Adjunction.ε_comp_map_ε, CategoryTheory.Equivalence.toAdjunction
-- 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 : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
⊢ Eq (α := e.functor.obj (e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (e.functor.map (η e.inverse))
      (η e.functor))
    (e.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))

Tactic:
e.toAdjunction.map_η_comp_η

Premises used: CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.map_η_comp_η
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
⊢ IsMonoidal.{v₁, v₁, u₁, u₁} (C := C) refl

Tactic:
inferInstanceAs (Adjunction.id (C := C)).IsMonoidal

Premises used: _private.0.CategoryTheory.Equivalence.isMonoidal_refl._proof_1
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
simp :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.symm.inverse.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε e.symm.inverse) (e.symm.unit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.symm.inverse.map (η e.symm.functor))
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.symm.inverse.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε e.symm.inverse)
    (e.symm.toAdjunction.unit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.symm.inverse.map (η e.symm.functor))

Tactic:
simp only [toAdjunction]

Premises used: CategoryTheory.Equivalence.toAdjunction
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
dsimp :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε e.functor)
    (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse))
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.symm.inverse.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε e.symm.inverse) (e.symm.unit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.symm.inverse.map (η e.symm.functor))

Tactic:
dsimp [symm]

Premises used: CategoryTheory.Equivalence.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
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
rw rw₁ :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε e.functor)
    (ε e.functor)
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ e.functor.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε e.functor)
    (e.counitIso.inv.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ≫ e.functor.map (η e.inverse))

Tactic:
rw [counitIso_inv_app_comp_functor_map_η_inverse]

Premises used: CategoryTheory.Equivalence.counitIso_inv_app_comp_functor_map_η_inverse
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
X Y : C
simp :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ⟶
      e.symm.inverse.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.symm.inverse X Y)
    (e.symm.unit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y)) ≫
      e.symm.inverse.map
        (δ e.symm.functor (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ≫ (e.symm.counit.app X ⊗ₘ e.symm.counit.app Y)))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ⟶
      e.symm.inverse.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.symm.inverse X Y)
    (e.symm.toAdjunction.unit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y)) ≫
      e.symm.inverse.map
        (δ e.symm.functor (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ≫
          (e.symm.toAdjunction.counit.app X ⊗ₘ e.symm.toAdjunction.counit.app Y)))

Tactic:
simp only [toAdjunction]

Premises used: CategoryTheory.Equivalence.toAdjunction
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
X Y : C
dsimp :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y) ⟶
      e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.functor X Y)
    (e.counitIso.inv.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y)) ≫
      e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y) ≫ (e.unitIso.inv.app X ⊗ₘ e.unitIso.inv.app Y)))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ⟶
      e.symm.inverse.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.symm.inverse X Y)
    (e.symm.unit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.symm.inverse.obj X) (e.symm.inverse.obj Y)) ≫
      e.symm.inverse.map
        (δ e.symm.functor (e.symm.inverse.obj X) (e.symm.inverse.obj Y) ≫ (e.symm.counit.app X ⊗ₘ e.symm.counit.app Y)))

Tactic:
dsimp [symm]

Premises used: CategoryTheory.Equivalence.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
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
X Y : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y) ⟶
      e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.functor X Y)
    (μ e.functor X Y ≫
      e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y) ≫
        e.functor.map (e.unitIso.inv.app X ⊗ₘ e.unitIso.inv.app Y))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y) ⟶
      e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.functor X Y)
    (e.counitIso.inv.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y)) ≫
      e.functor.map (δ e.inverse (e.functor.obj X) (e.functor.obj Y) ≫ (e.unitIso.inv.app X ⊗ₘ e.unitIso.inv.app Y)))

Tactic:
rw [map_comp, counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc]

Premises used: CategoryTheory.Equivalence.counitIso_inv_app_tensor_comp_functor_map_δ_inverse_assoc, CategoryTheory.Functor.map_comp
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
X Y : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y) ⟶
      e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ e.functor X Y)
    (μ e.functor X Y ≫
      e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y) ≫
        e.functor.map (e.unitIso.inv.app X ⊗ₘ e.unitIso.inv.app Y))

Tactic:
simp [← map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
e' : Equivalence.{v₂, v₃, u₂, u₃} D E
inst_10 : e'.functor.Monoidal
inst_11 : e'.inverse.Monoidal
inst_12 : e'.IsMonoidal
rw : (e.toAdjunction.comp e'.toAdjunction).IsMonoidal
⊢ (e.trans e').toAdjunction.IsMonoidal

Tactic:
rw [trans_toAdjunction]

Premises used: CategoryTheory.Equivalence.trans_toAdjunction
-- 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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
inst_8 : e.inverse.Monoidal
inst_9 : e.IsMonoidal
e' : Equivalence.{v₂, v₃, u₂, u₃} D E
inst_10 : e'.functor.Monoidal
inst_11 : e'.inverse.Monoidal
inst_12 : e'.IsMonoidal
⊢ (e.toAdjunction.comp e'.toAdjunction).IsMonoidal

Tactic:
infer_instance
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y : C
x : X ⟶ Y
x_1 : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj x_1) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1))
    (G.map x ▷ G.obj x_1 ≫
      Iso.hom ((i.symm.app Y ⊗ᵢ i.symm.app x_1) ≪≫ μIso F Y x_1 ≪≫ i.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y x_1)))
    (Iso.hom ((i.symm.app X ⊗ᵢ i.symm.app x_1) ≪≫ μIso F X x_1 ≪≫ i.app (tensorObj.{v₁, u₁} (𝒞 := inst) X x_1)) ≫
      G.map (x ▷ x_1))

Tactic:
simp [NatTrans.whiskerRight_app_tensor_app_assoc]

Premises used: CategoryTheory.NatTrans.whiskerRight_app_tensor_app_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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y x : C
x_1 : X ⟶ Y
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj x) (G.obj X) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y))
    (G.obj x ◁ G.map x_1 ≫
      Iso.hom ((i.symm.app x ⊗ᵢ i.symm.app Y) ≪≫ μIso F x Y ≪≫ i.app (tensorObj.{v₁, u₁} (𝒞 := inst) x Y)))
    (Iso.hom ((i.symm.app x ⊗ᵢ i.symm.app X) ≪≫ μIso F x X ≪≫ i.app (tensorObj.{v₁, u₁} (𝒞 := inst) x X)) ≫
      G.map (x ◁ x_1))

Tactic:
simp [NatTrans.whiskerLeft_app_tensor_app_assoc]

Premises used: CategoryTheory.NatTrans.whiskerLeft_app_tensor_app_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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
simp :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z ≫
          (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
              i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
                G.map (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
              LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
                i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (Iso.hom ((i.symm.app X ⊗ᵢ i.symm.app Y) ≪≫ μIso F X Y ≪≫ i.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ▷ G.obj Z ≫
      Iso.hom
          ((i.symm.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ᵢ i.symm.app Z) ≪≫
            μIso F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≪≫
              i.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z)) ≫
        G.map (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ Iso.hom ((i.symm.app Y ⊗ᵢ i.symm.app Z) ≪≫ μIso F Y Z ≪≫ i.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
        Iso.hom
          ((i.symm.app X ⊗ᵢ i.symm.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≪≫
            μIso F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≪≫
              i.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))))

Tactic:
simp only [Iso.trans_hom, tensorIso_hom, Iso.app_hom, Iso.symm_hom, μIso_hom, comp_whiskerRight,
      Category.assoc, MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.tensorIso_hom, CategoryTheory.Iso.symm_hom, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Iso.app_hom, CategoryTheory.Functor.Monoidal.μIso_hom, CategoryTheory.Iso.trans_hom
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z ≫
          (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
              F.map (Iso.hom (α_ X Y Z)) ≫
                i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
              LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
                i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      LaxMonoidal.μ F X Y ▷ G.obj Z ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ▷ G.obj Z ≫
          (i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ i.inv.app Z) ≫
            LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫
              i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z) ≫
                G.map (Iso.hom (α_ X Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
            (i.inv.app X ⊗ₘ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
              LaxMonoidal.μ F X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
                i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))

Tactic:
rw [← i.hom.naturality, map_associator_assoc, Functor.OplaxMonoidal.associativity_assoc,
      whiskerLeft_δ_μ_assoc, δ_μ_assoc]

Premises used: CategoryTheory.Functor.OplaxMonoidal.associativity_assoc, CategoryTheory.Functor.Monoidal.map_associator_assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.Functor.Monoidal.δ_μ_assoc, CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ_assoc