awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Discrete
Goal:
M : Type u
inst : Monoid M
N : Type u'
inst_1 : Monoid N
K : Type u
inst_2 : Monoid K
F : M →* N
G : N →* K
dsimp :
  (Discrete.eqToHom ⋯ ≫ (monoidalFunctor G).map (Discrete.eqToHom ⋯)) ≫
      NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) ((𝟙_ (Discrete M)) (𝒞 := discreteCategory M)) =
    Discrete.eqToHom ⋯
⊢ Eq (α :=
    (𝟙_ (Discrete K)) (𝒞 := discreteCategory K) ⟶
      (monoidalFunctor (G.comp F)).obj ((𝟙_ (Discrete M)) (𝒞 := discreteCategory M)))
    (ε (monoidalFunctor F ⋙ monoidalFunctor G) ≫
      (monoidalFunctorComp F G).hom.app ((𝟙_ (Discrete M)) (𝒞 := discreteCategory M)))
    (ε (monoidalFunctor (G.comp F)))

Tactic:
dsimp only [comp_ε, monoidalFunctorComp, Iso.refl, Discrete.monoidalFunctor_ε]

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Discrete.monoidalFunctor_ε, CategoryTheory.Discrete.monoidalFunctorComp, CategoryTheory.Functor.LaxMonoidal.comp_ε
-- Module: Mathlib.CategoryTheory.Monoidal.Discrete
Goal:
M : Type u
inst : Monoid M
N : Type u'
inst_1 : Monoid N
K : Type u
inst_2 : Monoid K
F : M →* N
G : N →* K
⊢ (Discrete.eqToHom ⋯ ≫ (monoidalFunctor G).map (Discrete.eqToHom ⋯)) ≫
      NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) ((𝟙_ (Discrete M)) (𝒞 := discreteCategory M)) =
    Discrete.eqToHom ⋯

Tactic:
simp [eqToHom_map]

Premises used: CategoryTheory.eqToHom_map
-- Module: Mathlib.CategoryTheory.Monoidal.Discrete
Goal:
M : Type u
inst : Monoid M
N : Type u'
inst_1 : Monoid N
K : Type u
inst_2 : Monoid K
F : M →* N
G : N →* K
x x_1 : Discrete M
dsimp :
  Eq (α :=
    tensorObj (𝒞 := discreteCategory K) ((monoidalFunctor F ⋙ monoidalFunctor G).obj x)
        ((monoidalFunctor F ⋙ monoidalFunctor G).obj x_1) ⟶
      (monoidalFunctor (G.comp F)).obj (tensorObj (𝒞 := discreteCategory M) x x_1))
    ((Discrete.eqToHom ⋯ ≫ (monoidalFunctor G).map (Discrete.eqToHom ⋯)) ≫
      NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) (tensorObj (𝒞 := discreteCategory M) x x_1))
    ((NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) x ⊗ₘ
        NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) x_1) ≫
      Discrete.eqToHom ⋯)
⊢ Eq (α :=
    tensorObj (𝒞 := discreteCategory K) ((monoidalFunctor F ⋙ monoidalFunctor G).obj x)
        ((monoidalFunctor F ⋙ monoidalFunctor G).obj x_1) ⟶
      (monoidalFunctor (G.comp F)).obj (tensorObj (𝒞 := discreteCategory M) x x_1))
    (μ (monoidalFunctor F ⋙ monoidalFunctor G) x x_1 ≫
      (monoidalFunctorComp F G).hom.app (tensorObj (𝒞 := discreteCategory M) x x_1))
    (((monoidalFunctorComp F G).hom.app x ⊗ₘ (monoidalFunctorComp F G).hom.app x_1) ≫
      μ (monoidalFunctor (G.comp F)) x x_1)

Tactic:
dsimp only [comp_μ, monoidalFunctorComp, Iso.refl, Discrete.monoidalFunctor_μ]

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Discrete.monoidalFunctorComp, CategoryTheory.Discrete.monoidalFunctor_μ, CategoryTheory.Functor.LaxMonoidal.comp_μ
-- Module: Mathlib.CategoryTheory.Monoidal.Discrete
Goal:
M : Type u
inst : Monoid M
N : Type u'
inst_1 : Monoid N
K : Type u
inst_2 : Monoid K
F : M →* N
G : N →* K
x x_1 : Discrete M
⊢ Eq (α :=
    tensorObj (𝒞 := discreteCategory K) ((monoidalFunctor F ⋙ monoidalFunctor G).obj x)
        ((monoidalFunctor F ⋙ monoidalFunctor G).obj x_1) ⟶
      (monoidalFunctor (G.comp F)).obj (tensorObj (𝒞 := discreteCategory M) x x_1))
    ((Discrete.eqToHom ⋯ ≫ (monoidalFunctor G).map (Discrete.eqToHom ⋯)) ≫
      NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) (tensorObj (𝒞 := discreteCategory M) x x_1))
    ((NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) x ⊗ₘ
        NatTrans.app (𝟙 (monoidalFunctor F ⋙ monoidalFunctor G)) x_1) ≫
      Discrete.eqToHom ⋯)

Tactic:
simp [eqToHom_map]

Premises used: CategoryTheory.eqToHom_map
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
X : C
⊢ Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) X = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Functor.map ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
X : C
⊢ (tensorObj (𝒞 := Functor.category) F G).obj X = G.obj (F.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, v, u, u} C C
X Y : C
f : X ⟶ Y
⊢ (tensorObj (𝒞 := Functor.category) F G).map f = G.map (F.map f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F G H K : Functor.{v, v, u, u} C C
α : F ⟶ G
β : H ⟶ K
X : C
⊢ NatTrans.app (α ⊗ₘ β) X = β.app (F.obj X) ≫ K.map (α.app X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F H K : Functor.{v, v, u, u} C C
β : H ⟶ K
X : C
⊢ NatTrans.app (F ◁ β) X = β.app (F.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F G H : Functor.{v, v, u, u} C C
α : F ⟶ G
X : C
⊢ NatTrans.app (α ▷ H) X = H.map (α.app X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F G H : Functor.{v, v, u, u} C C
X : C
⊢ NatTrans.app (Iso.hom (α_ F G H)) X =
    𝟙 ((tensorObj (𝒞 := Functor.category) (tensorObj (𝒞 := Functor.category) F G) H).obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F G H : Functor.{v, v, u, u} C C
X : C
⊢ NatTrans.app (Iso.inv (α_ F G H)) X =
    𝟙 ((tensorObj (𝒞 := Functor.category) F (tensorObj (𝒞 := Functor.category) G H)).obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
X : C
⊢ NatTrans.app (Iso.hom (λ_ F)) X =
    𝟙 ((tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) F).obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
X : C
⊢ NatTrans.app (Iso.inv (λ_ F)) X = 𝟙 (F.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
X : C
⊢ NatTrans.app (Iso.hom (ρ_ F)) X =
    𝟙 ((tensorObj (𝒞 := Functor.category) F ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category))).obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, v, u, u} C C
X : C
⊢ NatTrans.app (Iso.inv (ρ_ F)) X = 𝟙 (F.obj X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category))
      (Functor.obj (tensoringRight C) (tensorUnit.{v, u} C (𝒞 := inst))))
    (ε (tensoringRight C)) (Iso.inv (rightUnitorNatIso C))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (Functor.obj (tensoringRight C) (tensorUnit.{v, u} C (𝒞 := inst)))
      ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)))
    (η (tensoringRight C)) (Iso.hom (rightUnitorNatIso C))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u}
        (tensorObj (𝒞 := Functor.category) (Functor.obj (tensoringRight C) X) (Functor.obj (tensoringRight C) Y)) Z ⟶
      Functor.obj.{v, v, u, u} (Functor.obj (tensoringRight C) (tensorObj.{v, u} (𝒞 := inst) X Y)) Z)
    (NatTrans.app (μ (tensoringRight C) X Y) Z) (Iso.hom (α_ Z X Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.End
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (Functor.obj (tensoringRight C) (tensorObj.{v, u} (𝒞 := inst) X Y)) Z ⟶
      Functor.obj.{v, v, u, u}
        (tensorObj (𝒞 := Functor.category) (Functor.obj (tensoringRight C) X) (Functor.obj (tensoringRight C) Y)) Z)
    (NatTrans.app (δ (tensoringRight C) X Y) Z) (Iso.inv (α_ Z X Y))

Tactic:
rfl

Premises used: rfl
-- 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
i j : M
X : C
inst_3 : F.Monoidal
⊢ CategoryStruct.comp (Y := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) i j)).obj X) (NatTrans.app (μ F i j) X)
      (NatTrans.app (δ F i j) X) =
    𝟙 ((tensorObj (𝒞 := Functor.category) (F.obj i) (F.obj j)).obj X)

Tactic:
(μIso F i j).hom_inv_id_app X

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.Monoidal.μIso
-- 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
i j : M
X : C
inst_3 : F.Monoidal
⊢ NatTrans.app (δ F i j) X ≫ NatTrans.app (μ F i j) X = 𝟙 ((F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) i j)).obj X)

Tactic:
(μIso F i j).inv_hom_id_app X

Premises used: CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.Iso.inv_hom_id_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
X : C
inst_3 : F.Monoidal
⊢ CategoryStruct.comp (Y := (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X) (NatTrans.app (ε F) X)
      (NatTrans.app (η F) X) =
    𝟙 (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) X)

Tactic:
(εIso F).hom_inv_id_app X

Premises used: CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Functor.Monoidal.εIso
-- 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
X : C
inst_3 : F.Monoidal
⊢ NatTrans.app (η F) X ≫ NatTrans.app (ε F) X = 𝟙 ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X)

Tactic:
(εIso F).inv_hom_id_app X

Premises used: CategoryTheory.Functor.Monoidal.εIso, CategoryTheory.Iso.inv_hom_id_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
X Y : C
f : X ⟶ Y
inst_3 : F.LaxMonoidal
⊢ NatTrans.app (ε F) X ≫ (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).map f = f ≫ NatTrans.app (ε F) Y

Tactic:
((ε F).naturality f).symm

Premises used: CategoryTheory.Functor.LaxMonoidal.ε, CategoryTheory.NatTrans.naturality, Eq.symm
-- 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
X Y : C
f : X ⟶ Y
inst_3 : F.OplaxMonoidal
⊢ Eq (α :=
    (F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X ⟶
      Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) Y)
    (NatTrans.app (η F) X ≫ Functor.map ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) f)
    (NatTrans.app (η F) X ≫ f)

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 n : M
X Y : C
f : X ⟶ Y
inst_3 : F.LaxMonoidal
⊢ (F.obj n).map ((F.obj m).map f) ≫ NatTrans.app (μ F m n) Y =
    NatTrans.app (μ F m n) X ≫ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m n)).map f

Tactic:
(μ F m n).naturality f

Premises used: CategoryTheory.Functor.LaxMonoidal.μ, CategoryTheory.NatTrans.naturality
-- 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 n : M
X Y : C
f : X ⟶ Y
inst_3 : F.OplaxMonoidal
⊢ NatTrans.app (δ F m n) X ≫ (F.obj n).map ((F.obj m).map f) =
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m n)).map f ≫ NatTrans.app (δ F m n) 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 n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst_3 : F.LaxMonoidal
⊢ Eq (α :=
    (tensorObj (𝒞 := Functor.category) (F.obj m) (F.obj n)).obj X ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n')).obj X)
    (NatTrans.app ((F.map f ⊗ₘ F.map g) ≫ μ F m' n') X) (NatTrans.app (μ F m n ≫ F.map (f ⊗ₘ g)) X)

Tactic:
have := congr_app (μ_natural F f g) 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 n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst_3 : F.LaxMonoidal
this :
  Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n')).obj X)
    (((F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X)) ≫ NatTrans.app (μ F m' n') X)
    (NatTrans.app (μ F m n) X ≫ NatTrans.app (F.map (f ⊗ₘ g)) X)
⊢ Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n')).obj X)
    ((F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ NatTrans.app (μ F m' n') X)
    (NatTrans.app (μ F m n) X ≫ NatTrans.app (F.map (f ⊗ₘ g)) 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 n m' : M
f : m ⟶ m'
X : C
inst_3 : F.LaxMonoidal
rw :
  Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n)).obj X)
    ((F.obj n).map ((F.map f).app X) ≫ NatTrans.app (μ F m' n) X)
    ((F.map (𝟙 n)).app ((F.obj m).obj X) ≫ (F.obj n).map ((F.map f).app X) ≫ NatTrans.app (μ F m' n) X)
⊢ Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n)).obj X)
    ((F.obj n).map ((F.map f).app X) ≫ NatTrans.app (μ F m' n) X)
    (NatTrans.app (μ F m n) X ≫ NatTrans.app (F.map (f ▷ n)) X)

Tactic:
rw [← tensorHom_id, ← μ_naturality₂ F f (𝟙 n) X]

Premises used: CategoryTheory.μ_naturality₂, CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategory.tensorHom_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 n m' : M
f : m ⟶ m'
X : C
inst_3 : F.LaxMonoidal
⊢ Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m' n)).obj X)
    ((F.obj n).map ((F.map f).app X) ≫ NatTrans.app (μ F m' n) X)
    ((F.map (𝟙 n)).app ((F.obj m).obj X) ≫ (F.obj n).map ((F.map f).app X) ≫ NatTrans.app (μ F m' n) 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 n n' : M
g : n ⟶ n'
X : C
inst_3 : F.LaxMonoidal
rw :
  Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m n')).obj X)
    ((F.map g).app ((F.obj m).obj X) ≫ NatTrans.app (μ F m n') X)
    ((F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map (𝟙 m)).app X) ≫ NatTrans.app (μ F m n') X)
⊢ Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m n')).obj X)
    ((F.map g).app ((F.obj m).obj X) ≫ NatTrans.app (μ F m n') X)
    (NatTrans.app (μ F m n) X ≫ NatTrans.app (F.map (m ◁ g)) X)

Tactic:
rw [← id_tensorHom, ← μ_naturality₂ F (𝟙 m) g X]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.μ_naturality₂, CategoryTheory.CategoryStruct.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 n n' : M
g : n ⟶ n'
X : C
inst_3 : F.LaxMonoidal
⊢ Eq (α := (F.obj n).obj ((F.obj m).obj X) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m n')).obj X)
    ((F.map g).app ((F.obj m).obj X) ≫ NatTrans.app (μ F m n') X)
    ((F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map (𝟙 m)).app X) ≫ NatTrans.app (μ F m n') 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 n m' : M
f : m ⟶ m'
X : C
inst_3 : F.OplaxMonoidal
⊢ Eq (α := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m n)).obj X ⟶ (F.obj n).obj ((F.obj m').obj X))
    (NatTrans.app (δ F m n) X ≫ (F.obj n).map ((F.map f).app X))
    (NatTrans.app (F.map (f ▷ n)) X ≫ NatTrans.app (δ F m' n) X)

Tactic:
congr_app (δ_natural_left F f n) X

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_natural_left, 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
m n n' : M
g : n ⟶ n'
X : C
inst_3 : F.OplaxMonoidal
⊢ Eq (α := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) m n)).obj X ⟶ (F.obj n').obj ((F.obj m).obj X))
    (NatTrans.app (δ F m n) X ≫ (F.map g).app ((F.obj m).obj X))
    (NatTrans.app (F.map (m ◁ g)) X ≫ NatTrans.app (δ F m n') X)

Tactic:
congr_app (δ_natural_right F m g) X

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_natural_right, 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.LaxMonoidal
⊢ CategoryStruct.comp (Y := (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 (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X ≫ NatTrans.app (F.map (Iso.hom (λ_ n))) X) =
    𝟙 ((F.obj n).obj (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) X))

Tactic:
congr_app (left_unitality F n).symm X

Premises used: CategoryTheory.Functor.LaxMonoidal.left_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 (α :=
    (F.obj n).obj (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) 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))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n)).obj X)
      (NatTrans.app (Iso.inv (λ_ (F.obj n)) ≫ ε F ▷ F.obj n ≫ μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X)
      (NatTrans.app (δ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X))
⊢ Eq (α :=
    (F.obj n).obj (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) 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.map (Iso.inv (λ_ n))) X ≫ NatTrans.app (δ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X)

Tactic:
rw [map_leftUnitor_inv]

Premises used: CategoryTheory.Functor.Monoidal.map_leftUnitor_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 n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X))
    ((F.obj n).map (NatTrans.app (ε F) X))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n)).obj X)
      (𝟙 ((F.obj n).obj X) ≫
        (F.obj n).map (NatTrans.app (ε F) X) ≫ NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X)
      (NatTrans.app (δ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X))
⊢ Eq (α :=
    (F.obj n).obj (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) 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))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n)).obj X)
      (NatTrans.app (Iso.inv (λ_ (F.obj n)) ≫ ε F ▷ F.obj n ≫ μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X)
      (NatTrans.app (δ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) 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 n).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))
    (CategoryStruct.comp (Y :=
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n)).obj X)
      (𝟙 ((F.obj n).obj X) ≫
        (F.obj n).map (NatTrans.app (ε F) X) ≫ NatTrans.app (μ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) X)
      (NatTrans.app (δ F (tensorUnit.{v_1, u_1} M (𝒞 := inst_1)) n) 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 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))
⊢ Eq (α :=
    (F.obj n).obj ((F.obj (tensorUnit.{v_1, u_1} M (𝒞 := inst_1))).obj X) ⟶
      (F.obj n).obj (Functor.obj.{v, v, u, u} ((𝟙_ (Functor.{v, v, u, u} C C)) (𝒞 := Functor.category)) X))
    ((F.obj n).map (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)

Tactic:
rw [← cancel_mono ((F.obj n).map ((ε F).app X)), ← Functor.map_comp]

Premises used: CategoryTheory.Functor.LaxMonoidal.ε, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app