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 : 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) ≫
          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) ▷ 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)))

Tactic:
rw [← comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight_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 : 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) ≫
          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]
      dsimp
      rw [← comp_whiskerRight_assoc]

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

Tactic:
rw [← μ_natural_right, homEquiv_counit, map_comp_assoc,
        map_comp, tensorHom_def_assoc, ← associator_naturality_left_assoc]

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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : MonoidalCategory.{v₃, u₃} E
C' : Type u₁'
inst_6 : Category.{v₁', u₁'} C'
F : Functor.{v₁, v₂, u₁, u₂} C D
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 X ⊗ₘ adj.unit.app Y) ≫ μ G (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 X ▷ Y ▷ Z ≫
    Iso.hom (α_ (G.obj (F.obj X)) Y Z) ≫
      G.obj (F.obj X) ◁ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
        G.obj (F.obj X) ◁
            (G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
              G.map
                (F.map (μ G (F.obj Y) (F.obj Z)) ≫
                  adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))) ≫
          μ G (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp_assoc, map_comp,
        unit_naturality_assoc, MonoidalCategory.whiskerLeft_comp,
        unit_naturality_assoc, right_triangle_components, comp_id, assoc,
        tensorHom_def, MonoidalCategory.whiskerLeft_comp_assoc,
        ← associator_naturality_middle_assoc, ← associator_naturality_right_assoc,
        ← associativity G, ← comp_whiskerRight_assoc, ← tensorHom_def,
        ← whisker_exchange_assoc, ← comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc, CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Functor.LaxMonoidal.associativity, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.MonoidalCategory.associator_naturality_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 : G.LaxMonoidal
X Y Z : C
rw :
  tensorObj.{v₁, u₁} (𝒞 := inst) X Y ◁ adj.unit.app Z ≫
    ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (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)))
| Iso.hom (α_ X Y Z) ≫
    (adj.unit.app X ⊗ₘ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
      μ G (F.obj X) (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
        G.map
          (F.obj X ◁
            ((Equiv.symm
                    (adj.homEquiv (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)
                      (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) :
                  Equiv.{v₁ + 1, v₂ + 1}
                    (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)))
                    (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ⟶
                      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))) :
                (a : Y ⊗ Z ⟶ G.obj (F.obj Y ⊗ F.obj Z)) → F.obj (Y ⊗ Z) ⟶ F.obj Y ⊗ F.obj Z)
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))

Tactic:
rw [← μ_natural_right, homEquiv_counit, map_comp_assoc,
        map_comp, tensorHom_def_assoc, ← associator_naturality_left_assoc]
      dsimp
      rw [← MonoidalCategory.whiskerLeft_comp_assoc, map_comp,
        unit_naturality_assoc, MonoidalCategory.whiskerLeft_comp,
        unit_naturality_assoc, right_triangle_components, comp_id, assoc,
        tensorHom_def, MonoidalCategory.whiskerLeft_comp_assoc,
        ← associator_naturality_middle_assoc, ← associator_naturality_right_assoc,
        ← associativity G, ← comp_whiskerRight_assoc, ← tensorHom_def,
        ← whisker_exchange_assoc, ← comp_whiskerRight_assoc]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc, CategoryTheory.Category.assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_right, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Functor.LaxMonoidal.associativity, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.MonoidalCategory.tensorHom_def_assoc, CategoryTheory.MonoidalCategory.associator_naturality_left_assoc, CategoryTheory.MonoidalCategory.associator_naturality_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 : G.LaxMonoidal
X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ⟶
      G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (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) ≫
            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 X ⊗ₘ adj.unit.app Y) ≫ μ G (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:
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 : C
⊢ Eq.{v₁ + 1} (α := x ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)))
    (((adj.homEquiv x (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj x ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x))
              (x ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)))) :
          (a : F.obj x ⟶ 𝟙_ D ⊗ F.obj x) → x ⟶ G.obj (𝟙_ D ⊗ F.obj x))
        (Iso.inv (λ_ (F.obj x))) :
      x ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x) (Iso.inv (λ_ x))
        ((adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
              G.map
                (((Equiv.symm (adj.homEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) :
                      Equiv.{v₁ + 1, v₂ + 1}
                        (tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
                        (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) :
                    (a : 𝟙_ C ⟶ G.obj (𝟙_ D)) → F.obj (𝟙_ C) ⟶ 𝟙_ D)
                  (ε G)) ⊗ₘ
            adj.unit.app x ≫ 𝟙 (G.obj (F.obj x))) ≫
          μ G (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)) :
      x ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x)))

Tactic:
simp [tensorHom_def', homEquiv_unit, homEquiv_counit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.MonoidalCategory.tensorHom_def', 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 : C
⊢ Eq.{v₁ + 1} (α := x ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
    (((adj.homEquiv x (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) :
            Equiv.{v₂ + 1, v₁ + 1}
              (F.obj x ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
              (x ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))) :
          (a : F.obj x ⟶ F.obj x ⊗ 𝟙_ D) → x ⟶ G.obj (F.obj x ⊗ 𝟙_ D))
        (Iso.inv (ρ_ (F.obj x))) :
      x ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Iso.inv (ρ_ x))
        ((adj.unit.app x ≫ 𝟙 (G.obj (F.obj x)) ⊗ₘ
            adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
              G.map
                (((Equiv.symm (adj.homEquiv (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) :
                      Equiv.{v₁ + 1, v₂ + 1}
                        (tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
                        (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) :
                    (a : 𝟙_ C ⟶ G.obj (𝟙_ D)) → F.obj (𝟙_ C) ⟶ 𝟙_ D)
                  (ε G))) ≫
          μ G (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) :
      x ⟶ G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))))

Tactic:
simp [tensorHom_def, homEquiv_unit, homEquiv_counit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.MonoidalCategory.tensorHom_def, 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
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
⊢ adj.IsMonoidal

Tactic:
⟨?_, fun X Y ↦ ?_⟩

Premises used: CategoryTheory.Adjunction.IsMonoidal.mk
-- 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
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
refine_1 :
  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))
refine_2 :
  ∀ (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)))
⊢ adj.IsMonoidal

Tactic:
refine ⟨?_, fun X Y ↦ ?_⟩
-- 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
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
⊢ 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))

Tactic:
simp [homEquiv_counit, leftAdjointOplaxMonoidal_η]

Premises used: CategoryTheory.Adjunction.leftAdjointOplaxMonoidal_η, 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
this : F.OplaxMonoidal := adj.leftAdjointOplaxMonoidal
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:
simp [homEquiv_counit, ← μ_natural, leftAdjointOplaxMonoidal_δ]

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

Tactic:
simp