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

Tactic:
simp only [← Category.assoc]

Premises used: CategoryTheory.Category.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
e_a :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.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)))
    (((((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))
⊢ 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)))

Tactic:
congr 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'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
a :
  i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ
    𝟙 (G.obj Z) ≫ i.inv.app 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)

Tactic:
rw [← tensorHom_id, tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, 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 G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
a : F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ◁ i.inv.app Z
| i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ i.inv.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⊗ₘ
    𝟙 (G.obj Z) ≫ i.inv.app Z

Tactic:
simp only [Iso.hom_inv_id_app, Category.id_comp, id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.id_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'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
a : F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ◁ i.inv.app 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)

Tactic:
rw [← tensorHom_id, tensorHom_comp_tensorHom]
      simp only [Iso.hom_inv_id_app, Category.id_comp, id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_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'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
e_a :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.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 ≫
        (F.obj (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)))
    (((((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))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.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)))
    (((((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))

Tactic:
slice_lhs 3 4 =>
      rw [← tensorHom_id, tensorHom_comp_tensorHom]
      simp only [Iso.hom_inv_id_app, Category.id_comp, id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_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'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X Y Z : C
e_a :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.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 ≫
        F.obj (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)))
    (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))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.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 ≫
        (F.obj (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)))
    (((((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))

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.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
e_a :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ◁ i.inv.app Z ≫
        LaxMonoidal.μ F X Y ▷ F.obj Z ≫
          LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.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))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.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 ≫
        F.obj (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)))
    (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))

Tactic:
rw [← whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_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
e_a :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      Iso.hom (α_ (F.obj X) (F.obj Y) (G.obj Z)) ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫
          F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F 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))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ◁ i.inv.app Z ≫
        LaxMonoidal.μ F X Y ▷ F.obj Z ≫
          LaxMonoidal.μ F (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) Z ≫ F.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))

Tactic:
simp only [tensor_whiskerLeft, Functor.LaxMonoidal.associativity, Category.assoc,
      Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.LaxMonoidal.associativity, CategoryTheory.MonoidalCategory.tensor_whiskerLeft
-- 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
e_a :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (Iso.hom (α_ (G.obj X) (G.obj Y) (G.obj Z)) ≫
      (i.inv.app X ⊗ₘ i.inv.app Y ⊗ₘ 𝟙 (G.obj Z)) ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫
          F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F 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))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (G.obj X) (G.obj Y)) (G.obj Z) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    ((i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      Iso.hom (α_ (F.obj X) (F.obj Y) (G.obj Z)) ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫
          F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F 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))

Tactic:
rw [← tensorHom_id, associator_naturality_assoc]

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

Tactic:
simp [← id_tensorHom, -tensorHom_id]

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

Tactic:
simp only [Iso.trans_hom, εIso_hom, Iso.app_hom, ← tensorHom_id, tensorIso_hom, Iso.symm_hom,
      μIso_hom, Category.assoc, tensorHom_comp_tensorHom_assoc, Iso.hom_inv_id_app,
      Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.Monoidal.εIso_hom, CategoryTheory.MonoidalCategory.tensorIso_hom, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Iso.app_hom, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.Monoidal.μIso_hom, CategoryTheory.Iso.trans_hom, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_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'
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.Monoidal
i : F ≅ G
X : C
rw :
  Iso.hom (λ_ (G.obj X)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      ((𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ⊗ₘ i.inv.app X) ≫ (LaxMonoidal.ε F ⊗ₘ 𝟙 (F.obj X)))
      (LaxMonoidal.μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫ F.map (Iso.hom (λ_ X)) ≫ i.hom.app X)
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (G.obj X) ⟶ G.obj X)
    (Iso.hom (λ_ (G.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj X))
      (LaxMonoidal.ε F ⊗ₘ i.inv.app X)
      (LaxMonoidal.μ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ≫
        i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫ G.map (Iso.hom (λ_ X))))

Tactic:
rw [← i.hom.naturality, ← Category.comp_id (i.inv.app X),
      ← Category.id_comp (Functor.LaxMonoidal.ε F), ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.Functor.LaxMonoidal.ε, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.Category.id_comp