awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
X Y : C
⊢ Eq (α :=
    tensorObj.{v₄, u₄} (𝒞 := inst_6) (((F ⋙ G) ⋙ H).obj X) (((F ⋙ G) ⋙ H).obj Y) ⟶
      (F ⋙ G ⋙ H).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ ((F ⋙ G) ⋙ H) X Y ≫ (F.associator G H).hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((F.associator G H).hom.app X ⊗ₘ (F.associator G H).hom.app Y) ≫ μ (F ⋙ G ⋙ H) X Y)

Tactic:
simp only [comp_obj, comp_μ, associator_hom_app, Functor.comp_map, map_comp,
      comp_id, tensorHom_id, id_whiskerRight, assoc, id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Functor.associator_hom_app, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.LaxMonoidal.comp_μ, CategoryTheory.Functor.comp_map, CategoryTheory.MonoidalCategory.tensorHom_id, CategoryTheory.Category.id_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
F G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₁ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 (ε (G.prod' K)).1
h₂ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 (ε (G.prod' K)).2
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ⟶ (G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (G.prod' K))

Tactic:
ext
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₁ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    ((ε (F.prod' H)).1 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
h₂ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε F ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε (G.prod' K)).1
h₃ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε F ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1) (ε G)
h₄ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε F ≫ α.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε G)
h₅ h₆ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε G) (ε G)
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).1 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).1 (ε (G.prod' K)).1

Tactic:
rw [prod_comp_fst, prod'_ε_fst, prod'_ε_fst, prod'_app_fst, IsMonoidal.unit]

Premises used: CategoryTheory.Functor.prod'_ε_fst, CategoryTheory.NatTrans.IsMonoidal.unit, CategoryTheory.NatTrans.prod'_app_fst, CategoryTheory.prod_comp_fst
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
h₂ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    ((ε (F.prod' H)).2 ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε (G.prod' K)).2
h₃ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε H ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε (G.prod' K)).2
h₄ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε H ≫ ((prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2) (ε K)
h₅ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε H ≫ β.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε K)
h₆ h₇ :
  Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε K) (ε K)
⊢ Eq (α :=
    (𝟙_ (D × E)) (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E).2 ⟶
      ((G.prod' K).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2)
    (ε (F.prod' H) ≫ (prod' α β).app (tensorUnit.{v₁, u₁} C (𝒞 := inst))).2 (ε (G.prod' K)).2

Tactic:
rw [prod_comp_snd, prod'_ε_snd, prod'_ε_snd, prod'_app_snd, IsMonoidal.unit]

Premises used: CategoryTheory.NatTrans.prod'_app_snd, CategoryTheory.NatTrans.IsMonoidal.unit, CategoryTheory.Functor.prod'_ε_snd, CategoryTheory.prod_comp_snd
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
X Y : C
h₁ :
  Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y)).1 ⟶
      ((G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1)
    (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1
    (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).1
h₂ :
  Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y)).2 ⟶
      ((G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2)
    (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2
    (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).2
⊢ Eq (α :=
    tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y) ⟶
      (G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y)

Tactic:
ext
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
X Y : C
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y)).1 ⟶
      ((G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1)
    (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).1
    (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).1

Tactic:
simp only [prod_comp_fst, prod'_μ_fst, prod'_app_fst,
        prodMonoidal_tensorHom, IsMonoidal.tensor]

Premises used: CategoryTheory.Functor.prod'_μ_fst, CategoryTheory.NatTrans.IsMonoidal.tensor, CategoryTheory.NatTrans.prod'_app_fst, CategoryTheory.prod_comp_fst, CategoryTheory.MonoidalCategory.prodMonoidal_tensorHom
-- 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 G : Functor.{v₁, v₂, u₁, u₂} C D
H K : Functor.{v₁, v₃, u₁, u₃} C E
α : F ⟶ G
β : H ⟶ K
inst_11 : F.LaxMonoidal
inst_12 : G.LaxMonoidal
inst_13 : IsMonoidal α
inst_14 : H.LaxMonoidal
inst_15 : K.LaxMonoidal
inst_16 : IsMonoidal β
X Y : C
⊢ Eq (α :=
    (tensorObj (𝒞 := CategoryTheory.prod'.{v₂, v₃, u₂, u₃} D E) ((F.prod' H).obj X) ((F.prod' H).obj Y)).2 ⟶
      ((G.prod' K).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2)
    (μ (F.prod' H) X Y ≫ (prod' α β).app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)).2
    (((prod' α β).app X ⊗ₘ (prod' α β).app Y) ≫ μ (G.prod' K) X Y).2

Tactic:
simp only [prod_comp_snd, prod'_μ_snd, prod'_app_snd,
        prodMonoidal_tensorHom, IsMonoidal.tensor]

Premises used: CategoryTheory.NatTrans.prod'_app_snd, CategoryTheory.NatTrans.IsMonoidal.tensor, CategoryTheory.Functor.prod'_μ_snd, CategoryTheory.MonoidalCategory.prodMonoidal_tensorHom, CategoryTheory.prod_comp_snd
-- 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
e : F₁ ≅ F₂
inst_11 : NatTrans.IsMonoidal e.hom
rw :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((LaxMonoidal.ε F₁ ≫ e.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁)
rw₁ :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁ ≫ e.hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁)
rw₂ :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₁ ≫ 𝟙 (F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (LaxMonoidal.ε F₁)
rw₃ rw₄ :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F₁)
    (LaxMonoidal.ε F₁)
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ F₁.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (LaxMonoidal.ε F₂ ≫ e.inv.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (LaxMonoidal.ε F₁)

Tactic:
rw [← NatTrans.IsMonoidal.unit (τ := e.hom), assoc, hom_inv_id_app, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.IsMonoidal.unit, CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Category.comp_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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
dsimp :
  𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    CategoryStruct.comp (Y := G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G) (G.map (ε F))
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ (F ⋙ G).obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (𝟭 C) ≫ adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε (F ⋙ G))

Tactic:
dsimp
-- 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 C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
rw :
  adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ 𝟙 (G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
⊢ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    CategoryStruct.comp (Y := G.obj (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε G) (G.map (ε F))

Tactic:
rw [id_comp, ← unit_app_unit_comp_map_η adj, assoc, Monoidal.map_η_ε]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.unit_app_unit_comp_map_η, CategoryTheory.Functor.Monoidal.map_η_ε, CategoryTheory.Category.id_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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
dsimp :
  adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ 𝟙 (G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
⊢ adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ 𝟙 (G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
dsimp
-- 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 C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
rw rw₁ :
  Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) =
    adj.unit.app (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ 𝟙 (G.obj (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : C
dsimp :
  𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    (adj.unit.app X ⊗ₘ adj.unit.app 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))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (obj.{v₁, v₁, u₁, u₁} (𝟭 C) X) (obj.{v₁, v₁, u₁, u₁} (𝟭 C) Y) ⟶
      (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ (𝟭 C) X Y ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ (F ⋙ G) X Y)

Tactic:
dsimp
-- 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 C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
X Y : C
rw :
  𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
        (G.map (μ F X Y))
rw₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))) (G.map (δ F X Y))
        (G.map (μ F X Y)))
rw₂ :
  adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ 𝟙 (G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
rw₃ rw₄ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) X Y ⟶ G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
    (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
⊢ 𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ≫ adj.unit.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) =
    (adj.unit.app X ⊗ₘ adj.unit.app 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))

Tactic:
rw [← unit_app_tensor_comp_map_δ_assoc, id_comp, Monoidal.map_δ_μ, comp_id]

Premises used: CategoryTheory.Adjunction.unit_app_tensor_comp_map_δ_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Functor.Monoidal.map_δ_μ, CategoryTheory.Category.id_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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
dsimp :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (F.map (ε G)) ≫
      adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
⊢ Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (ε (G ⋙ F) ≫ adj.counit.app (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (ε (𝟭 D))

Tactic:
dsimp