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 C
adj : F ⊣ G
inst_11 : F.Monoidal
inst_12 : G.LaxMonoidal
inst_13 : adj.IsMonoidal
rw :
  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))
rw₁ :
  CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε F) (η F) =
    𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
rw₂ rw₃ :
  Eq.{v₂ + 1} (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) (𝟙 (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
⊢ 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))

Tactic:
rw [assoc, map_ε_comp_counit_app_unit adj, ε_η]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.Monoidal.ε_η, CategoryTheory.Adjunction.map_ε_comp_counit_app_unit
-- 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 : D
dsimp :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
        (F.map (μ G X Y)) ≫
      adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_2) ((G ⋙ F).obj X) ((G ⋙ F).obj Y) ⟶
      obj.{v₂, v₂, u₂, u₂} (𝟭 D) (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    (μ (G ⋙ F) X Y ≫ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y))
    ((adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ μ (𝟭 D) 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 : D
rw :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
      (F.map (μ G X Y) ≫ adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
rw₁ :
  CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
      (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y)) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
rw₂ :
  adj.counit.app X ⊗ₘ adj.counit.app Y =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
rw₃ rw₄ :
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (G.obj X)) (F.obj (G.obj Y)) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)
    (adj.counit.app X ⊗ₘ adj.counit.app Y) (adj.counit.app X ⊗ₘ adj.counit.app Y)
⊢ CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (G.obj X) (G.obj Y))) (μ F (G.obj X) (G.obj Y))
        (F.map (μ G X Y)) ≫
      adj.counit.app (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y) =
    (adj.counit.app X ⊗ₘ adj.counit.app Y) ≫ 𝟙 (tensorObj.{v₂, u₂} (𝒞 := inst_2) X Y)

Tactic:
rw [assoc, map_μ_comp_counit_app_tensor, μ_δ_assoc, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Adjunction.map_μ_comp_counit_app_tensor, CategoryTheory.Functor.Monoidal.μ_δ_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
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_11 : e.functor.Monoidal
inst_12 : e.inverse.Monoidal
inst_13 : e.IsMonoidal
⊢ NatTrans.IsMonoidal e.unit

Tactic:
inferInstanceAs (NatTrans.IsMonoidal e.toAdjunction.unit)

Premises used: _private.0.CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit._proof_1
-- 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
e : Equivalence.{v₁, v₂, u₁, u₂} C D
inst_11 : e.functor.Monoidal
inst_12 : e.inverse.Monoidal
inst_13 : e.IsMonoidal
⊢ NatTrans.IsMonoidal e.counit

Tactic:
inferInstanceAs (NatTrans.IsMonoidal e.toAdjunction.counit)

Premises used: _private.0.CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit._proof_1
-- 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
X Y Z : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
α : X.Hom Y
β : Y.Hom Z
⊢ NatTrans.IsMonoidal α.hom

Tactic:
have := α.2
-- 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
X Y Z : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
α : X.Hom Y
β : Y.Hom Z
this : NatTrans.IsMonoidal α.hom
⊢ NatTrans.IsMonoidal β.hom

Tactic:
have := β.2
-- 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
X Y Z : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
α : X.Hom Y
β : Y.Hom Z
this_1 : NatTrans.IsMonoidal α.hom
this : NatTrans.IsMonoidal β.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)

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
F : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
⊢ Hom.hom (𝟙 F) = 𝟙 F.toFunctor

Tactic:
rfl

Premises used: rfl
-- 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
F G H : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ G
β : G ⟶ H
⊢ (α ≫ β).hom = α.hom ≫ β.hom

Tactic:
rfl

Premises used: rfl
-- 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
F G : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
α β : F ⟶ G
h : α.hom = β.hom
mk :
  ∀ (hom : F.toFunctor ⟶ G.toFunctor) (isMonoidal : NatTrans.IsMonoidal hom)
    (h : { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom = β.hom),
    { hom := hom, isMonoidal := isMonoidal : F.Hom G } = β
⊢ α = β

Tactic:
cases α
-- 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
F G : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
β : F ⟶ G
hom : F.toFunctor ⟶ G.toFunctor
isMonoidal : NatTrans.IsMonoidal hom
h : { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom = β.hom
mk :
  ∀ (hom_1 : F.toFunctor ⟶ G.toFunctor) (isMonoidal_1 : NatTrans.IsMonoidal hom_1)
    (h : { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom = { hom := hom_1, isMonoidal := isMonoidal_1 }.hom),
    { hom := hom, isMonoidal := isMonoidal : F.Hom G } = { hom := hom_1, isMonoidal := isMonoidal_1 }
⊢ { hom := hom, isMonoidal := isMonoidal : F.Hom G } = β

Tactic:
cases β
-- 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
F G : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
hom : F.toFunctor ⟶ G.toFunctor
isMonoidal : NatTrans.IsMonoidal hom
hom_1 : F.toFunctor ⟶ G.toFunctor
isMonoidal_1 : NatTrans.IsMonoidal hom_1
h : { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom = { hom := hom_1, isMonoidal := isMonoidal_1 }.hom
mk :
  ∀ (isMonoidal_2 : NatTrans.IsMonoidal { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom),
    { hom := hom, isMonoidal := isMonoidal : F.Hom G } =
      { hom := { hom := hom, isMonoidal := isMonoidal }.hom, isMonoidal := isMonoidal_2 }
⊢ { hom := hom, isMonoidal := isMonoidal : F.Hom G } = { hom := hom_1, isMonoidal := isMonoidal_1 }

Tactic:
subst h
-- 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
F G : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
hom : F.toFunctor ⟶ G.toFunctor
isMonoidal : NatTrans.IsMonoidal hom
isMonoidal_1 : NatTrans.IsMonoidal { hom := hom, isMonoidal := isMonoidal : F.Hom G }.hom
⊢ { hom := hom, isMonoidal := isMonoidal : F.Hom G } =
    { hom := { hom := hom, isMonoidal := isMonoidal }.hom, isMonoidal := isMonoidal_1 }

Tactic:
rfl
-- 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 : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε F.toFunctor ≫ Iso.hom (e (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (ε G.toFunctor)
tensor :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F.toFunctor X Y ≫ Iso.hom (e (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y)
unit₁ :
  autoParam
    (Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (ε F.toFunctor ≫ (NatIso.ofComponents e ⋯).hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε G.toFunctor))
    NatTrans.IsMonoidal.unit._autoParam
tensor₁ :
  autoParam
    (∀ (X Y : C),
      Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (μ F.toFunctor X Y ≫ (NatIso.ofComponents e ⋯).hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (((NatIso.ofComponents e ⋯).hom.app X ⊗ₘ (NatIso.ofComponents e ⋯).hom.app Y) ≫ μ G.toFunctor X Y))
    NatTrans.IsMonoidal.tensor._autoParam
⊢ NatTrans.IsMonoidal (NatIso.ofComponents e ⋯).hom

Tactic:
constructor
-- 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 : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε F.toFunctor ≫ Iso.hom (e (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (ε G.toFunctor)
tensor :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F.toFunctor X Y ≫ Iso.hom (e (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y)
⊢ autoParam
    (Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (ε F.toFunctor ≫ (NatIso.ofComponents e ⋯).hom.app (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (ε G.toFunctor))
    NatTrans.IsMonoidal.unit._autoParam

Tactic:
assumption
-- 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 : LaxMonoidalFunctor.{v₁, v₂, u₁, u₂} C D
e : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (e Y).hom = (e X).hom ≫ G.map f
unit :
  Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε F.toFunctor ≫ Iso.hom (e (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (ε G.toFunctor)
tensor :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ F.toFunctor X Y ≫ Iso.hom (e (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)))
      (((e X).hom ⊗ₘ (e Y).hom) ≫ μ G.toFunctor X Y)
⊢ autoParam
    (∀ (X Y : C),
      Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (μ F.toFunctor X Y ≫ (NatIso.ofComponents e ⋯).hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
        (((NatIso.ofComponents e ⋯).hom.app X ⊗ₘ (NatIso.ofComponents e ⋯).hom.app Y) ≫ μ G.toFunctor X Y))
    NatTrans.IsMonoidal.tensor._autoParam

Tactic:
assumption
-- 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
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
e : F ≅ G
this : G.Monoidal := transport e
⊢ NatTrans.IsMonoidal e.hom

Tactic:
⟨rfl, fun X Y ↦ ?_⟩

Premises used: CategoryTheory.NatTrans.IsMonoidal.mk, rfl
-- 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
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
e : F ≅ G
this : G.Monoidal := transport e
refine :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (LaxMonoidal.μ F X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      ((e.hom.app X ⊗ₘ e.hom.app Y) ≫ LaxMonoidal.μ G X Y)
⊢ NatTrans.IsMonoidal e.hom

Tactic:
refine ⟨rfl, fun X Y ↦ ?_⟩
-- 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
F G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
e : F ≅ G
this : G.Monoidal := transport e
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (LaxMonoidal.μ F X Y ≫ e.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    ((e.hom.app X ⊗ₘ e.hom.app Y) ≫ LaxMonoidal.μ G X Y)

Tactic:
simp [transport_μ, tensorHom_comp_tensorHom_assoc]

Premises used: CategoryTheory.Functor.Monoidal.transport_μ, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y : C
⊢ MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Y = coprod.{v, u} X Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) W Y ⟶ MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Z)
    (f ⊗ₘ g) (coprod.map f g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y Z : C
f : Y ⟶ Z
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Y ⟶ MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Z)
    (X ◁ f) (coprod.map (𝟙 X) f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α :=
    MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Z ⟶ MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) Y Z)
    (f ▷ Z) (coprod.map f (𝟙 Z))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X : C
⊢ Eq.{v + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (MonoidalCategoryStruct.tensorUnit.{v, u} C (𝒞 := inst)) X ⟶ X)
    (Iso.hom (λ_ X)) (coprod.desc (initial.to X) (𝟙 X))

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit.desc, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X : C
⊢ Eq.{v + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X (MonoidalCategoryStruct.tensorUnit.{v, u} C (𝒞 := inst)) ⟶ X)
    (Iso.hom (ρ_ X)) (coprod.desc (𝟙 X) (initial.to X))

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit.desc, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X : C
⊢ Eq.{v + 1} (α :=
    X ⟶ MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (MonoidalCategoryStruct.tensorUnit.{v, u} C (𝒞 := inst)) X)
    (Iso.inv (λ_ X)) coprod.inr

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X : C
⊢ Eq.{v + 1} (α :=
    X ⟶ MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X (MonoidalCategoryStruct.tensorUnit.{v, u} C (𝒞 := inst)))
    (Iso.inv (ρ_ X)) coprod.inl

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) Y Z))
    (Iso.hom (α_ X Y Z)) (coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr))

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit.desc, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Y) Z)
    (Iso.inv (α_ X Y Z)) (coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr))

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit.desc, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
inst_2 : HasBinaryCoproducts.{v, u} C
f g : C
⊢ ∀ {Z : C} (f_1 : g ⟶ Z),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) f g ⟶ tensorObj.{v, u} (𝒞 := inst) Z f)
      (f ◁ f_1 ≫ Iso.hom (coprod.braiding f Z))
      (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) g f)
        (Iso.hom (coprod.braiding f g) : tensorObj.{v, u} (𝒞 := inst) f g ⟶ tensorObj.{v, u} (𝒞 := inst) g f)
        (f_1 ▷ f : tensorObj.{v, u} (𝒞 := inst) g f ⟶ tensorObj.{v, u} (𝒞 := inst) Z f))

Tactic:
simp