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
x : G.LaxMonoidal
x_1 x_2 : D
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj x_1) (G.obj x_2) ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) x_1 x_2))
    (μ G x_1 x_2) (μ G x_1 x_2)

Tactic:
simp [homEquiv_counit, homEquiv_unit, ← μ_natural]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.Functor.LaxMonoidal.μ_natural
-- 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
x : F.OplaxMonoidal
η :
  Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (OplaxMonoidal.η F)
    (OplaxMonoidal.η F)
δ :
  ∀ (x_1 x_2 : C),
    Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))
      (OplaxMonoidal.δ F x_1 x_2) (OplaxMonoidal.δ F x_1 x_2)
⊢ (fun (x : G.LaxMonoidal) ↦ (adj.leftAdjointOplaxMonoidal : F.OplaxMonoidal))
      ((fun (x : F.OplaxMonoidal) ↦ (adj.rightAdjointLaxMonoidal : G.LaxMonoidal)) x) =
    x

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 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
x : F.OplaxMonoidal
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (η F)

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
x : F.OplaxMonoidal
x_1 x_2 : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))
    (δ F x_1 x_2) (δ F x_1 x_2)

Tactic:
simp [homEquiv_counit, homEquiv_unit, ← δ_natural_assoc]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.Functor.OplaxMonoidal.δ_natural_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.Monoidal
inst_5 : G.Monoidal
inst_6 : adj.IsMonoidal
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (CategoryStruct.comp (Y := G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G) (G.map (ε F)))
    (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
simp [← adj.unit_app_unit_comp_map_η]

Premises used: CategoryTheory.Adjunction.unit_app_unit_comp_map_η
-- 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.Monoidal
inst_5 : G.Monoidal
inst_6 : adj.IsMonoidal
⊢ Eq (α := F.obj (G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map (η G)) (η F))
    (adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))

Tactic:
simp [← adj.map_ε_comp_counit_app_unit]

Premises used: CategoryTheory.Adjunction.map_ε_comp_counit_app_unit
-- 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
this : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
simp :
  IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (e.toAdjunction.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ e.inverse.map (OplaxMonoidal.η e.functor))
⊢ IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (LaxMonoidal.ε e.inverse)

Tactic:
simp only [this, Adjunction.rightAdjointLaxMonoidal_ε, Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.Adjunction.rightAdjointLaxMonoidal_ε
-- 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
this : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
⊢ IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (e.toAdjunction.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ e.inverse.map (OplaxMonoidal.η e.functor))

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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
this : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
⊢ IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (LaxMonoidal.ε e.inverse)

Tactic:
have : IsIso (LaxMonoidal.ε e.inverse) := by
    simp only [this, Adjunction.rightAdjointLaxMonoidal_ε, Adjunction.homEquiv_unit]
    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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
this_1 : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this :
  IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (LaxMonoidal.ε e.inverse)
X Y : D
simp :
  IsIso (X := tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) (Y :=
    e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (e.toAdjunction.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) ≫
      e.inverse.map
        (OplaxMonoidal.δ e.functor (e.inverse.obj X) (e.inverse.obj Y) ≫
          (e.toAdjunction.counit.app X ⊗ₘ e.toAdjunction.counit.app Y)))
⊢ IsIso (X := tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) (Y :=
    e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (LaxMonoidal.μ e.inverse X Y)

Tactic:
simp only [Adjunction.rightAdjointLaxMonoidal_μ, Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.rightAdjointLaxMonoidal_μ, CategoryTheory.Adjunction.homEquiv_unit
-- 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
this_1 : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this :
  IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (LaxMonoidal.ε e.inverse)
⊢ ∀ (X Y : D),
    IsIso (X := tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) (Y :=
      e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (LaxMonoidal.μ e.inverse X Y)

Tactic:
have : ∀ (X Y : D), IsIso (LaxMonoidal.μ e.inverse X Y) := fun X Y ↦ by
    simp only [Adjunction.rightAdjointLaxMonoidal_μ, Adjunction.homEquiv_unit]
    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'
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_7 : e.functor.Monoidal
this_1 : e.inverse.LaxMonoidal := e.toAdjunction.rightAdjointLaxMonoidal
this_2 :
  IsIso (X := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Y := e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (LaxMonoidal.ε e.inverse)
this :
  ∀ (X Y : D),
    IsIso (X := tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj X) (e.inverse.obj Y)) (Y :=
      e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) (LaxMonoidal.μ e.inverse X Y)
⊢ e.inverse.Monoidal

Tactic:
apply Monoidal.ofLaxMonoidal

Premises used: CategoryTheory.Functor.Monoidal.ofLaxMonoidal
-- 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
⊢ e.IsMonoidal

Tactic:
inferInstance

Premises used: inferInstance
-- 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 (α :=
    obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (e.unitIso.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ e.inverse.map (η e.functor)) (ε e.inverse)

Tactic:
e.toAdjunction.unit_app_unit_comp_map_η

Premises used: CategoryTheory.Adjunction.unit_app_unit_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
X Y : C
⊢ Eq (α :=
    obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y)))
    (e.unitIso.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.inverse.map (δ e.functor X Y))
    ((e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y) ≫ μ e.inverse (e.functor.obj X) (e.functor.obj Y))

Tactic:
e.toAdjunction.unit_app_tensor_comp_map_δ X Y

Premises used: CategoryTheory.Adjunction.unit_app_tensor_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 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (e.functor.map (ε e.inverse) ≫ e.counitIso.hom.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (η e.functor)

Tactic:
e.toAdjunction.map_ε_comp_counit_app_unit

Premises used: CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.map_ε_comp_counit_app_unit
-- 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.counitIso.hom.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (δ e.functor (e.inverse.obj X) (e.inverse.obj Y) ≫ (e.counitIso.hom.app X ⊗ₘ e.counitIso.hom.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.counitIso.inv.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.counitIso.inv.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.counitIso.inv.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.counitIso.inv.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.counitIso.inv.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
rw :
  Eq (α :=
    e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      e.functor.obj
        (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj 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.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y))
⊢ 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.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.functor X Y ≫ e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y))

Tactic:
rw [← cancel_epi (δ e.functor _ _), Monoidal.δ_μ_assoc]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ, CategoryTheory.Equivalence.functor, CategoryTheory.cancel_epi, CategoryTheory.Functor.Monoidal.δ_μ_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 : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
X Y : C
a :
  Eq (α :=
    e.inverse.obj (e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ⟶
      e.inverse.obj
        (e.functor.obj
          (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y)))))
    (e.inverse.map
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj 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.inverse.map (e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y)))
⊢ Eq (α :=
    e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      e.functor.obj
        (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj 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.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y))

Tactic:
apply e.inverse.map_injective

Premises used: CategoryTheory.Functor.map_injective, CategoryTheory.Equivalence.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
X Y : C
⊢ Eq (α :=
    e.inverse.obj (e.functor.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ⟶
      e.inverse.obj
        (e.functor.obj
          (tensorObj.{v₁, u₁} (𝒞 := inst) (e.inverse.obj (e.functor.obj X)) (e.inverse.obj (e.functor.obj Y)))))
    (e.inverse.map
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj 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.inverse.map (e.functor.map (e.unitIso.hom.app X ⊗ₘ e.unitIso.hom.app Y)))

Tactic:
simp [← cancel_epi (e.unitIso.hom.app (X ⊗ Y)), Functor.map_comp,
    unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc]

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor_assoc, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.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 : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_4 : e.functor.Monoidal
inst_5 : e.inverse.Monoidal
inst_6 : e.IsMonoidal
⊢ Eq (α :=
    obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      e.inverse.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (e.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ e.inverse.map (η e.functor)) (ε e.inverse)

Tactic:
e.toAdjunction.unit_app_unit_comp_map_η

Premises used: CategoryTheory.Adjunction.unit_app_unit_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
X Y : C
⊢ Eq (α :=
    obj.{v₁, v₁, u₁, u₁} (𝟭 C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      e.inverse.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (e.functor.obj X) (e.functor.obj Y)))
    (e.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ e.inverse.map (δ e.functor X Y))
    ((e.unit.app X ⊗ₘ e.unitIso.hom.app Y) ≫ μ e.inverse (e.functor.obj X) (e.functor.obj Y))

Tactic:
e.toAdjunction.unit_app_tensor_comp_map_δ X Y

Premises used: CategoryTheory.Adjunction.unit_app_tensor_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 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (e.functor.map (ε e.inverse) ≫ e.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (η e.functor)

Tactic:
e.toAdjunction.map_ε_comp_counit_app_unit

Premises used: CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.map_ε_comp_counit_app_unit