awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
M : Mon.{v₂, u₂} D
N : C
e : F.obj N ≅ M.X
this_1 : MonObj (F.obj N) := MonObj.ofIso e.symm
this : MonObj N := (FullyFaithful.ofFullyFaithful F).monObj N
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2)
        (Mon.X (obj (C := Mon.{v₁, u₁} C) F.mapMon { X := N, mon := this : Mon.{v₁, u₁} C }))
        (Mon.X (obj (C := Mon.{v₁, u₁} C) F.mapMon { X := N, mon := this : Mon.{v₁, u₁} C })) ⟶
      M.X)
    (μ ≫ e.hom) ((e.hom ⊗ₘ e.hom) ≫ μ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M_1 N_1 O X : C
inst_2 : MonObj M_1
inst_3 : MonObj N_1
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : BraidedCategory.{v₁, u₁} C
inst_10 : BraidedCategory.{v₂, u₂} D
inst_11 : F.LaxBraided
M N : C
inst_12 : MonObj M
inst_13 : MonObj N
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_5) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) M N))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj M) (F.obj N)) η («μ» F M N)) η

Tactic:
simp [← Functor.map_comp, leftUnitor_inv_comp_tensorHom_assoc]

Premises used: CategoryTheory.MonoidalCategory.leftUnitor_inv_comp_tensorHom_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M_1 N_1 O X : C
inst_2 : MonObj M_1
inst_3 : MonObj N_1
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : BraidedCategory.{v₁, u₁} C
inst_10 : BraidedCategory.{v₂, u₂} D
inst_11 : F.Braided
M N : Mon.{v₁, u₁} C
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_5) ⟶ Mon.X (obj F.mapMon (tensorObj (𝒞 := Mon.instCategory) M N)))
    (CategoryStruct.comp (Y := Mon.X (tensorObj (𝒞 := Mon.instCategory) (obj F.mapMon M) (obj F.mapMon N))) η
      (Iso.hom (Monoidal.μIso F M.X N.X)))
    η

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M_1 N_1 O X : C
inst_2 : MonObj M_1
inst_3 : MonObj N_1
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : SymmetricCategory.{v₁, u₁} C
inst_10 : SymmetricCategory.{v₂, u₂} D
inst_11 : F.LaxBraided
M N : Mon.{v₁, u₁} C
w :
  Eq (α :=
    Mon.X (tensorObj (𝒞 := Mon.instCategory) (obj F.mapMon M) (obj F.mapMon N)) ⟶
      Mon.X (obj F.mapMon (tensorObj (𝒞 := Mon.instCategory) N M)))
    (Mon.Hom.hom («μ» F.mapMon M N ≫ map F.mapMon (Iso.hom (β_ M N))))
    (Mon.Hom.hom (Iso.hom (β_ (obj F.mapMon M) (obj F.mapMon N)) ≫ «μ» F.mapMon N M))
⊢ Eq (α :=
    Quiver.Hom (V := Mon.{v₂, u₂} D) (tensorObj (𝒞 := Mon.instCategory) (obj F.mapMon M) (obj F.mapMon N))
      (obj F.mapMon (tensorObj (𝒞 := Mon.instCategory) N M)))
    («μ» F.mapMon M N ≫ map F.mapMon (Iso.hom (β_ M N)))
    (Iso.hom (β_ (obj F.mapMon M) (obj F.mapMon N)) ≫ «μ» F.mapMon N M)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M_1 N_1 O X : C
inst_2 : MonObj M_1
inst_3 : MonObj N_1
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : SymmetricCategory.{v₁, u₁} C
inst_10 : SymmetricCategory.{v₂, u₂} D
inst_11 : F.LaxBraided
M N : Mon.{v₁, u₁} C
⊢ Eq (α :=
    Mon.X (tensorObj (𝒞 := Mon.instCategory) (obj F.mapMon M) (obj F.mapMon N)) ⟶
      Mon.X (obj F.mapMon (tensorObj (𝒞 := Mon.instCategory) N M)))
    (Mon.Hom.hom («μ» F.mapMon M N ≫ map F.mapMon (Iso.hom (β_ M N))))
    (Mon.Hom.hom (Iso.hom (β_ (obj F.mapMon M) (obj F.mapMon N)) ≫ «μ» F.mapMon N M))

Tactic:
Functor.LaxBraided.braided ..

Premises used: CategoryTheory.Functor.LaxBraided.braided
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M_1 N_1 O X : C
inst_2 : MonObj M_1
inst_3 : MonObj N_1
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : SymmetricCategory.{v₁, u₁} C
inst_10 : SymmetricCategory.{v₂, u₂} D
inst_11 : F.LaxBraided
M N : Mon.{v₁, u₁} C
⊢ Eq (α :=
    Mon.X (tensorObj (𝒞 := Mon.instCategory) (obj F.mapMon M) (obj F.mapMon N)) ⟶
      Mon.X (obj F.mapMon (tensorObj (𝒞 := Mon.instCategory) N M)))
    (Mon.Hom.hom («μ» F.mapMon M N ≫ map F.mapMon (Iso.hom (β_ M N))))
    (Mon.Hom.hom (Iso.hom (β_ (obj F.mapMon M) (obj F.mapMon N)) ≫ «μ» F.mapMon N M))

Tactic:
exact Functor.LaxBraided.braided ..

Premises used: CategoryTheory.Functor.LaxBraided.braided
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A : Mon.{v₁, u₁} C
⊢ Eq (α :=
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶
      (monToLaxMonoidalObj A).obj ((𝟙_ (Discrete PUnit.{u_1 + 1})) (𝒞 := discreteCategory PUnit.{u_1 + 1})))
    (ε (monToLaxMonoidalObj A)) η

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
A : Mon.{v₁, u₁} C
X Y : Discrete PUnit.{u_1 + 1}
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) ((monToLaxMonoidalObj A).obj X) ((monToLaxMonoidalObj A).obj Y) ⟶
      (monToLaxMonoidalObj A).obj (tensorObj (𝒞 := discreteCategory PUnit.{u_1 + 1}) X Y))
    («μ» (monToLaxMonoidalObj A) X Y) μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F_1 F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
F : LaxMonoidalFunctor.{w, v₁, w, u₁} (Discrete PUnit.{w + 1}) C
x : Discrete PUnit.{w + 1}
⊢ x = Mon.X (trivial (Discrete PUnit.{w + 1}))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
F : Mon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (obj (monToLaxMonoidal C ⋙ laxMonoidalToMon C) F).X) η
    (η ≫ 𝟙 F.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
F : Mon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (obj (monToLaxMonoidal C ⋙ laxMonoidalToMon C) F).X
        (obj (monToLaxMonoidal C ⋙ laxMonoidalToMon C) F).X ⟶
      (obj (monToLaxMonoidal C ⋙ laxMonoidalToMon C) F).X)
    μ (μ ≫ 𝟙 F.X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : IsCommMonObj.{v₁, u₁} M
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) M M ⟶ M) (Iso.inv (β_ M M) ≫ μ) μ

Tactic:
simp [← cancel_epi (β_ M M).hom]

Premises used: CategoryTheory.BraidedCategory.braiding, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : BraidedCategory.{v₁, u₁} C
dsimp :
  Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ μ) μ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O X : C
inst_2 : MonObj M
inst_3 : MonObj N
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : BraidedCategory.{v₁, u₁} C
rw : Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) = Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
rw₁ rw₂ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (Iso.hom (ρ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
⊢ Iso.hom (β_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rw [braiding_leftUnitor, unitors_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_equal, CategoryTheory.braiding_leftUnitor
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : IsCommMonObj.{v₁, u₁} M
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⟶ M)
    (tensorμ M M M M ≫ (μ ⊗ₘ μ) ≫ μ) ((μ ⊗ₘ μ) ≫ μ)

Tactic:
simp only [mon_tauto]
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : C
inst_2 : MonObj M
inst_3 : BraidedCategory.{v₁, u₁} C
inst_4 : IsCommMonObj.{v₁, u₁} M
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M M) (tensorObj.{v₁, u₁} (𝒞 := inst) M M) ⟶ M)
    (tensorδ M M M M ≫ (μ ⊗ₘ μ) ≫ μ) ((μ ⊗ₘ μ) ≫ μ)

Tactic:
simp only [mon_tauto]
-- Module: Mathlib.CategoryTheory.Monoidal.Mon
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M_1 N_1 O X_1 : C
inst_2 : MonObj M_1
inst_3 : MonObj N_1
inst_4 : MonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_7 : Category.{v₃, u₃} E
inst_8 : MonoidalCategory.{v₃, u₃} E
F F' : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : SymmetricCategory.{v₁, u₁} C
M N W X Y Z : C
inst_10 : MonObj M
inst_11 : MonObj N
inst_12 : IsCommMonObj.{v₁, u₁} M
inst_13 : IsCommMonObj.{v₁, u₁} N
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M N) (tensorObj.{v₁, u₁} (𝒞 := inst) M N) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) M N)
    (Iso.hom (β_ (tensorObj.{v₁, u₁} (𝒞 := inst) M N) (tensorObj.{v₁, u₁} (𝒞 := inst) M N)) ≫ μ) μ

Tactic:
simp [← IsIso.inv_comp_eq, tensorμ, ← associator_inv_naturality_left_assoc,
      ← associator_naturality_right_assoc, SymmetricCategory.braiding_swap_eq_inv_braiding M N,
      ← tensorHom_def_assoc, -whiskerRight_tensor, -tensor_whiskerLeft, MonObj.tensorObj.mul_def,
      ← MonoidalCategory.whiskerLeft_comp_assoc, -MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.MonoidalCategory.whiskerRight_tensor, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.MonoidalCategory.associator_inv_naturality_left_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonObj.tensorObj.mul_def, CategoryTheory.MonoidalCategory.tensorμ, CategoryTheory.SymmetricCategory.braiding_swap_eq_inv_braiding, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.MonoidalCategory.tensor_whiskerLeft, CategoryTheory.MonoidalCategory.tensorHom_def_assoc, CategoryTheory.MonoidalCategory.associator_naturality_right_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Multifunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalCategory.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
f : F₁ ⟶ F₂
X₁ : C
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ((curriedTensorPre F₁).obj X₁).map f_1 ≫ (f.app X₁ ⊗ₘ f.app Y) =
      (f.app X₁ ⊗ₘ f.app X) ≫ ((curriedTensorPre F₂).obj X₁).map f_1

Tactic:
simp [← id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Multifunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalCategory.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
f : F₁ ⟶ F₂
x x_1 : C
x_2 : x ⟶ x_1
w :
  ∀ (x_3 : C),
    NatTrans.app ((curriedTensorPre F₁).map x_2 ≫ { app := fun (X₂ : C) ↦ f.app x_1 ⊗ₘ f.app X₂, naturality := ⋯ })
        x_3 =
      NatTrans.app
        ({ app := fun (X₂ : C) ↦ f.app x ⊗ₘ f.app X₂, naturality := ⋯ :
            NatTrans ((curriedTensorPre F₁).obj x) ((curriedTensorPre F₂).obj x) } ≫
          (curriedTensorPre F₂).map x_2)
        x_3
⊢ (curriedTensorPre F₁).map x_2 ≫ { app := fun (X₂ : C) ↦ f.app x_1 ⊗ₘ f.app X₂, naturality := ⋯ } =
    { app := fun (X₂ : C) ↦ f.app x ⊗ₘ f.app X₂, naturality := ⋯ :
        NatTrans ((curriedTensorPre F₁).obj x) ((curriedTensorPre F₂).obj x) } ≫
      (curriedTensorPre F₂).map x_2

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Multifunctor
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalCategory.{v_2, u_2} D
F₁ F₂ : Functor.{v_1, v_2, u_1, u_2} C D
f : F₁ ⟶ F₂
x x_1 : C
x_2 : x ⟶ x_1
x_3 : C
⊢ NatTrans.app ((curriedTensorPre F₁).map x_2 ≫ { app := fun (X₂ : C) ↦ f.app x_1 ⊗ₘ f.app X₂, naturality := ⋯ }) x_3 =
    NatTrans.app
      ({ app := fun (X₂ : C) ↦ f.app x ⊗ₘ f.app X₂, naturality := ⋯ :
          NatTrans ((curriedTensorPre F₁).obj x) ((curriedTensorPre F₂).obj x) } ≫
        (curriedTensorPre F₂).map x_2)
      x_3

Tactic:
simp [← tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ G₂ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst_13 : IsMonoidal τ
inst_14 : IsMonoidal τ'
⊢ Eq (α := tensorUnit.{v₃, u₃} E (𝒞 := inst_4) ⟶ (F₂ ⋙ G₂).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (F₁ ⋙ G₁) ≫ (τ ◫ τ').app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F₂ ⋙ G₂))

Tactic:
simp only [comp_obj, comp_ε, hcomp_app, assoc, naturality_assoc, unit_assoc, ← map_comp, unit]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.NatTrans.hcomp_app, CategoryTheory.NatTrans.IsMonoidal.unit, CategoryTheory.Functor.LaxMonoidal.comp_ε, CategoryTheory.NatTrans.IsMonoidal.unit_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ G₂ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst_13 : IsMonoidal τ
inst_14 : IsMonoidal τ'
X Y : C
simp :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G₁.obj (F₁.obj X)) (G₁.obj (F₁.obj Y)) ⟶
      G₂.obj (F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
    ((τ'.app (F₁.obj X) ⊗ₘ τ'.app (F₁.obj Y)) ≫
      CategoryStruct.comp (Y := G₂.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₁.obj X) (F₁.obj Y)))
        (μ G₂ (F₁.obj X) (F₁.obj Y)) (G₂.map (μ F₁ X Y) ≫ G₂.map (τ.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))))
    ((τ'.app (F₁.obj X) ⊗ₘ τ'.app (F₁.obj Y)) ≫
      CategoryStruct.comp (Y := G₂.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₁.obj X) (F₁.obj Y)))
        (μ G₂ (F₁.obj X) (F₁.obj Y)) (G₂.map (τ.app X ⊗ₘ τ.app Y) ≫ G₂.map (μ F₂ X Y)))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F₁ ⋙ G₁).obj X) ((F₁ ⋙ G₁).obj Y) ⟶
      (F₂ ⋙ G₂).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ (F₁ ⋙ G₁) X Y ≫ (τ ◫ τ').app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((τ ◫ τ').app X ⊗ₘ (τ ◫ τ').app Y) ≫ μ (F₂ ⋙ G₂) X Y)

Tactic:
simp only [comp_obj, comp_μ, hcomp_app, assoc, naturality_assoc,
      tensor_assoc, ← tensorHom_comp_tensorHom, μ_natural_assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.NatTrans.hcomp_app, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Functor.LaxMonoidal.comp_μ, CategoryTheory.NatTrans.IsMonoidal.tensor_assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ G₂ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst_13 : IsMonoidal τ
inst_14 : IsMonoidal τ'
X Y : C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) (G₁.obj (F₁.obj X)) (G₁.obj (F₁.obj Y)) ⟶
      G₂.obj (F₂.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
    ((τ'.app (F₁.obj X) ⊗ₘ τ'.app (F₁.obj Y)) ≫
      CategoryStruct.comp (Y := G₂.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₁.obj X) (F₁.obj Y)))
        (μ G₂ (F₁.obj X) (F₁.obj Y)) (G₂.map (μ F₁ X Y) ≫ G₂.map (τ.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))))
    ((τ'.app (F₁.obj X) ⊗ₘ τ'.app (F₁.obj Y)) ≫
      CategoryStruct.comp (Y := G₂.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F₁.obj X) (F₁.obj Y)))
        (μ G₂ (F₁.obj X) (F₁.obj Y)) (G₂.map (τ.app X ⊗ₘ τ.app Y) ≫ G₂.map (μ F₂ X Y)))

Tactic:
simp only [← map_comp, tensor]

Premises used: CategoryTheory.NatTrans.IsMonoidal.tensor, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : IsMonoidal τ
rw : IsMonoidal (τ ◫ 𝟙 G₁)
⊢ IsMonoidal (Functor.whiskerRight τ G₁)

Tactic:
rw [← Functor.hcomp_id]

Premises used: CategoryTheory.Functor.hcomp_id
-- Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : IsMonoidal τ
⊢ IsMonoidal (τ ◫ 𝟙 G₁)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ G₂ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst_13 : IsMonoidal τ'
rw : IsMonoidal (𝟙 F₁ ◫ τ')
⊢ IsMonoidal (F₁.whiskerLeft τ')

Tactic:
rw [← Functor.id_hcomp]

Premises used: CategoryTheory.Functor.id_hcomp
-- Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
G₁ G₂ : Functor.{v₂, v₃, u₂, u₃} D E
inst_11 : G₁.LaxMonoidal
inst_12 : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst_13 : IsMonoidal τ'
⊢ IsMonoidal (𝟙 F₁ ◫ τ')

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation
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
E' : Type u₄
inst_6 : Category.{v₄, u₄} E'
inst_7 : MonoidalCategory.{v₄, u₄} E'
F₁ F₂ F₃ : Functor.{v₁, v₂, u₁, u₂} C D
τ : F₁ ⟶ F₂
inst_8 : F₁.LaxMonoidal
inst_9 : F₂.LaxMonoidal
inst_10 : F₃.LaxMonoidal
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
H : Functor.{v₃, v₄, u₃, u₄} E E'
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : H.LaxMonoidal
⊢ Eq (α := tensorUnit.{v₄, u₄} E' (𝒞 := inst_6) ⟶ (F ⋙ G ⋙ H).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε ((F ⋙ G) ⋙ H) ≫ (F.associator G H).hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F ⋙ G ⋙ H))

Tactic:
simp only [comp_obj, comp_ε, assoc, Functor.map_comp, associator_hom_app, comp_id,
      Functor.comp_map]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Category.comp_id, CategoryTheory.Functor.LaxMonoidal.comp_ε, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map