awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X) ⟶
      (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X))
    ((F.obj n).map (NatTrans.app (η F) X ≫ NatTrans.app (ε F) X))
    ((NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X ≫ NatTrans.app (F.map (Iso.hom (λ_ n))) X) ≫
      (F.obj n).map (NatTrans.app (ε F) X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ CategoryStruct.comp (Y := (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
      (NatTrans.app (ε F) ((F.obj n).obj X))
      (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X ≫ NatTrans.app (F.map (Iso.hom (ρ_ n))) X) =
    𝟙 (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X))

Tactic:
congr_app (Functor.LaxMonoidal.right_unitality F n).symm X

Premises used: CategoryTheory.Functor.LaxMonoidal.right_unitality, Eq.symm, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
rw :
  Eq (α :=
    Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X) ⟶
      (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
    (NatTrans.app (ε F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (NatTrans.app (Iso.inv (ρ_ (F.obj n)) ≫ F.obj n ◁ ε F ≫ μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X))
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X) ⟶
      (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
    (NatTrans.app (ε F) ((F.obj n).obj X))
    (NatTrans.app (F.map (Iso.inv (ρ_ n))) X ≫ NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)

Tactic:
rw [map_rightUnitor_inv]

Premises used: CategoryTheory.Functor.Monoidal.map_rightUnitor_inv
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
dsimp :
  Eq (α := (F.obj n).obj X ⟶ (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
    (NatTrans.app (ε F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (𝟙 ((F.obj n).obj X) ≫
        NatTrans.app (ε F) ((F.obj n).obj X) ≫ NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X))
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X) ⟶
      (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
    (NatTrans.app (ε F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (NatTrans.app (Iso.inv (ρ_ (F.obj n)) ≫ F.obj n ◁ ε F ≫ μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α := (F.obj n).obj X ⟶ (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X))
    (NatTrans.app (ε F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (𝟙 ((F.obj n).obj X) ≫
        NatTrans.app (ε F) ((F.obj n).obj X) ≫ NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X))

Tactic:
simp only [Category.id_comp, Category.assoc, μ_δ_app,
    endofunctorMonoidalCategory_tensorObj_obj, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.endofunctorMonoidalCategory_tensorObj_obj, CategoryTheory.Category.comp_id, CategoryTheory.μ_δ_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
rw :
  Eq (α :=
    (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X) ⟶
      Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X))
    (NatTrans.app (η F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) ≫ F.obj n ◁ η F ≫ Iso.hom (ρ_ (F.obj n))) X))
⊢ Eq (α :=
    (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X) ⟶
      Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X))
    (NatTrans.app (η F) ((F.obj n).obj X))
    (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X ≫ NatTrans.app (F.map (Iso.hom (ρ_ n))) X)

Tactic:
rw [map_rightUnitor]

Premises used: CategoryTheory.Functor.Monoidal.map_rightUnitor
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
dsimp :
  Eq (α := (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X) ⟶ (F.obj n).obj X)
    (NatTrans.app (η F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X ≫
        NatTrans.app (η F) ((F.obj n).obj X) ≫ 𝟙 ((F.obj n).obj X)))
⊢ Eq (α :=
    (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X) ⟶
      Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) ((F.obj n).obj X))
    (NatTrans.app (η F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) ≫ F.obj n ◁ η F ≫ Iso.hom (ρ_ (F.obj n))) X))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
n : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α := (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj ((F.obj n).obj X) ⟶ (F.obj n).obj X)
    (NatTrans.app (η F) ((F.obj n).obj X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj X)
      (NatTrans.app (μ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X)
      (NatTrans.app (δ F n (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) X ≫
        NatTrans.app (η F) ((F.obj n).obj X) ≫ 𝟙 ((F.obj n).obj X)))

Tactic:
simp only [Category.comp_id, μ_δ_app_assoc]

Premises used: CategoryTheory.μ_δ_app_assoc, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ m₃ : M
X : C
inst_3 : F.LaxMonoidal
⊢ Eq (α :=
    (tensorObj (𝒞 := Functor.category) (tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)) (F.obj m₃)).obj X ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
    (NatTrans.app
      (μ F m₁ m₂ ▷ F.obj m₃ ≫ μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃ ≫ F.map (Iso.hom (α_ m₁ m₂ m₃))) X)
    (NatTrans.app
      (Iso.hom (α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)) ≫
        F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))
      X)

Tactic:
have := congr_app (associativity F m₁ m₂ m₃) X
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ m₃ : M
X : C
inst_3 : F.LaxMonoidal
this :
  Eq (α :=
    (F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X)) ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
    ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X) ≫
      NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
        NatTrans.app (F.map (Iso.hom (α_ m₁ m₂ m₃))) X)
    (𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
      NatTrans.app (μ F m₂ m₃) ((F.obj m₁).obj X) ≫ NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X)
⊢ Eq (α :=
    (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X) ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
    ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X) ≫
      NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
        NatTrans.app (F.map (Iso.hom (α_ m₁ m₂ m₃))) X)
    (NatTrans.app (μ F m₂ m₃) ((F.obj m₁).obj X) ≫ NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X)

Tactic:
simpa using this
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ m₃ : M
X : C
inst_3 : F.Monoidal
rw :
  Eq (α :=
    (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X) ⟶
      (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X))
    ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X))
    ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X) ≫
      NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
        NatTrans.app (F.map (Iso.hom (α_ m₁ m₂ m₃))) X ≫
          NatTrans.app (F.map (Iso.inv (α_ m₁ m₂ m₃))) X ≫
            NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
⊢ Eq (α :=
    (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X) ⟶
      (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X))
    ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X))
    (NatTrans.app (μ F m₂ m₃) ((F.obj m₁).obj X) ≫
      NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
        NatTrans.app (F.map (Iso.inv (α_ m₁ m₂ m₃))) X ≫
          NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)

Tactic:
rw [← associativity_app_assoc]

Premises used: CategoryTheory.associativity_app_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ m₃ : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X) ⟶
      (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X))
    ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X))
    ((F.obj m₃).map (NatTrans.app (μ F m₁ m₂) X) ≫
      NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
        NatTrans.app (F.map (Iso.hom (α_ m₁ m₂ m₃))) X ≫
          NatTrans.app (F.map (Iso.inv (α_ m₁ m₂ m₃))) X ≫
            NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ m₃ : M
X : C
inst_3 : F.Monoidal
rw :
  Eq (α :=
    (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X) ⟶
      (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X))
    ((F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃)).obj X)
      (NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
      (CategoryStruct.comp (Y :=
        (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
        (NatTrans.app
          (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃ ≫
            δ F m₁ m₂ ▷ F.obj m₃ ≫
              Iso.hom (α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)) ≫
                F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))
          X)
        (NatTrans.app (δ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
          NatTrans.app (δ F m₂ m₃) ((F.obj m₁).obj X))))
⊢ Eq (α :=
    (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X) ⟶
      (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X))
    ((F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X))
    (NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
      NatTrans.app (F.map (Iso.hom (α_ m₁ m₂ m₃))) X ≫
        NatTrans.app (δ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
          NatTrans.app (δ F m₂ m₃) ((F.obj m₁).obj X))

Tactic:
rw [map_associator]

Premises used: CategoryTheory.Functor.Monoidal.map_associator
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ m₃ : M
X : C
inst_3 : F.Monoidal
dsimp :
  Eq (α :=
    (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X) ⟶
      (F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X)))
    ((F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃)).obj X)
      (NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
      (CategoryStruct.comp (Y :=
        (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
        (NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
          (F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X) ≫
            𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
              NatTrans.app (μ F m₂ m₃) ((F.obj m₁).obj X) ≫
                NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X)
        (NatTrans.app (δ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
          NatTrans.app (δ F m₂ m₃) ((F.obj m₁).obj X))))
⊢ Eq (α :=
    (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X) ⟶
      (F.obj m₃).obj ((tensorObj (𝒞 := Functor.category) (F.obj m₁) (F.obj m₂)).obj X))
    ((F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃)).obj X)
      (NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
      (CategoryStruct.comp (Y :=
        (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
        (NatTrans.app
          (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃ ≫
            δ F m₁ m₂ ▷ F.obj m₃ ≫
              Iso.hom (α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)) ≫
                F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))
          X)
        (NatTrans.app (δ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
          NatTrans.app (δ F m₂ m₃) ((F.obj m₁).obj X))))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ m₃ : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (F.obj m₃).obj ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂)).obj X) ⟶
      (F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X)))
    ((F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃)).obj X)
      (NatTrans.app (μ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X)
      (CategoryStruct.comp (Y :=
        (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃))).obj X)
        (NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ m₂) m₃) X ≫
          (F.obj m₃).map (NatTrans.app (δ F m₁ m₂) X) ≫
            𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
              NatTrans.app (μ F m₂ m₃) ((F.obj m₁).obj X) ≫
                NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X)
        (NatTrans.app (δ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₂ m₃)) X ≫
          NatTrans.app (δ F m₂ m₃) ((F.obj m₁).obj X))))

Tactic:
simp only [Category.id_comp, Category.assoc, μ_δ_app_assoc, μ_δ_app,
    endofunctorMonoidalCategory_tensorObj_obj, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.endofunctorMonoidalCategory_tensorObj_obj, CategoryTheory.μ_δ_app_assoc, CategoryTheory.Category.comp_id, CategoryTheory.μ_δ_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst_3 : F.Monoidal
rw :
  CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj Y)
      (NatTrans.app (ε F) X ≫
        (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).map f ≫
          NatTrans.app (μ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y)
      (NatTrans.app (δ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y) =
    CategoryStruct.comp (Y := (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X) (NatTrans.app (ε F) X)
        (NatTrans.app (η F) X ≫ f ≫ NatTrans.app (F.map (Iso.inv (ρ_ m))) Y) ≫
      NatTrans.app (δ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y
⊢ (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).map f ≫
      NatTrans.app (μ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y =
    NatTrans.app (η F) X ≫ f ≫ NatTrans.app (F.map (Iso.inv (ρ_ m))) Y

Tactic:
rw [← cancel_epi ((ε F).app _), ← cancel_mono ((δ F _ _).app _)]

Premises used: CategoryTheory.Functor.LaxMonoidal.ε, CategoryTheory.Functor.OplaxMonoidal.δ, CategoryTheory.cancel_mono, CategoryTheory.cancel_epi, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst_3 : F.Monoidal
⊢ CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))).obj Y)
      (NatTrans.app (ε F) X ≫
        (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).map f ≫
          NatTrans.app (μ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y)
      (NatTrans.app (δ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y) =
    CategoryStruct.comp (Y := (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X) (NatTrans.app (ε F) X)
        (NatTrans.app (η F) X ≫ f ≫ NatTrans.app (F.map (Iso.inv (ρ_ m))) Y) ≫
      NatTrans.app (δ F m (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ : M
X : C
inst_3 : F.Monoidal
rw :
  Eq (α :=
    (tensorObj (𝒞 := Functor.category) (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) (F.obj m₂)).obj
        ((F.obj m₁).obj X) ⟶
      (tensorObj (𝒞 := Functor.category)
            (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))) (F.obj m₂)).obj
        X)
    (NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂)) X ≫
        NatTrans.app (F.map (Iso.inv (α_ m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂))) X ≫
          NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) m₂) X)
    ((F.obj m₂).map (NatTrans.app (η F) ((F.obj m₁).obj X) ≫ NatTrans.app (F.map (Iso.inv (ρ_ m₁))) X))
⊢ Eq (α :=
    (tensorObj (𝒞 := Functor.category) (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) (F.obj m₂)).obj
        ((F.obj m₁).obj X) ⟶
      (tensorObj (𝒞 := Functor.category)
            (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))) (F.obj m₂)).obj
        X)
    (NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂)) X ≫
        NatTrans.app (F.map (Iso.inv (α_ m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂))) X ≫
          NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) m₂) X)
    (NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (F.map (Iso.hom (λ_ m₂))) ((F.obj m₁).obj X) ≫
        (F.obj m₂).map (NatTrans.app (F.map (Iso.inv (ρ_ m₁))) X))

Tactic:
rw [← obj_η_app_assoc, ← Functor.map_comp]

Premises used: CategoryTheory.obj_η_app_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
M : Type u_1
inst_1 : Category.{v_1, u_1} M
inst_2 : MonoidalCategory.{v_1, u_1} M
F : M ⥤ Functor.{v, v, u, u} C C
m₁ m₂ : M
X : C
inst_3 : F.Monoidal
⊢ Eq (α :=
    (tensorObj (𝒞 := Functor.category) (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) (F.obj m₂)).obj
        ((F.obj m₁).obj X) ⟶
      (tensorObj (𝒞 := Functor.category)
            (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)))) (F.obj m₂)).obj
        X)
    (NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂) ((F.obj m₁).obj X) ≫
      NatTrans.app (μ F m₁ (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂)) X ≫
        NatTrans.app (F.map (Iso.inv (α_ m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) m₂))) X ≫
          NatTrans.app (δ F (tensorObj.{v_1, u_1} (𝒞 := inst_1) m₁ (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))) m₂) X)
    ((F.obj m₂).map (NatTrans.app (η F) ((F.obj m₁).obj X) ≫ NatTrans.app (F.map (Iso.inv (ρ_ m₁))) X))

Tactic:
simp