awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
x x_1 x_2 : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ⟶ F.obj x_1)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))
      ((CartesianMonoidalCategory.prodComparison F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2 ≫
          CartesianMonoidalCategory.prodComparison F x x_1 ▷ F.obj x_2 ≫
            Iso.hom (α_ (F.obj x) (F.obj x_1) (F.obj x_2))) ≫
        snd (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
      (fst (F.obj x_1) (F.obj x_2)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
        (F.map (Iso.hom (α_ x x_1 x_2)) ≫
          CartesianMonoidalCategory.prodComparison F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2) ≫
            F.obj x ◁ CartesianMonoidalCategory.prodComparison F x_1 x_2)
        (snd (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))
      (fst (F.obj x_1) (F.obj x_2)))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
x x_1 x_2 : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2) ⟶ F.obj x_2)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))
      ((CartesianMonoidalCategory.prodComparison F (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) x_2 ≫
          CartesianMonoidalCategory.prodComparison F x x_1 ▷ F.obj x_2 ≫
            Iso.hom (α_ (F.obj x) (F.obj x_1) (F.obj x_2))) ≫
        snd (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
      (snd (F.obj x_1) (F.obj x_2)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))
      (CategoryStruct.comp (Y :=
        tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2)))
        (F.map (Iso.hom (α_ x x_1 x_2)) ≫
          CartesianMonoidalCategory.prodComparison F x (tensorObj.{v₁, u₁} (𝒞 := inst) x_1 x_2) ≫
            F.obj x ◁ CartesianMonoidalCategory.prodComparison F x_1 x_2)
        (snd (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))
      (snd (F.obj x_1) (F.obj x_2)))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
x : C
h_snd :
  Iso.inv (λ_ (F.obj x)) ≫ snd (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x))
        (F.map (Iso.inv (λ_ x)))
        (CartesianMonoidalCategory.prodComparison F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x ≫
          CartesianMonoidalCategory.terminalComparison F ▷ F.obj x))
      (snd (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x))
⊢ Eq (α := F.obj x ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x))
    (Iso.inv (λ_ (F.obj x)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x))
      (F.map (Iso.inv (λ_ x)))
      (CartesianMonoidalCategory.prodComparison F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x ≫
        CartesianMonoidalCategory.terminalComparison F ▷ F.obj x))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
x : C
⊢ Iso.inv (λ_ (F.obj x)) ≫ snd (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x))
        (F.map (Iso.inv (λ_ x)))
        (CartesianMonoidalCategory.prodComparison F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) x ≫
          CartesianMonoidalCategory.terminalComparison F ▷ F.obj x))
      (snd (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (F.obj x))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
x : C
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (Iso.inv (ρ_ (F.obj x))) (fst (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.map (Iso.inv (ρ_ x)))
        (CartesianMonoidalCategory.prodComparison F x (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
          F.obj x ◁ CartesianMonoidalCategory.terminalComparison F))
      (fst (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
⊢ Eq (α := F.obj x ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
    (Iso.inv (ρ_ (F.obj x)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.map (Iso.inv (ρ_ x)))
      (CartesianMonoidalCategory.prodComparison F x (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
        F.obj x ◁ CartesianMonoidalCategory.terminalComparison F))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
x : C
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (Iso.inv (ρ_ (F.obj x))) (fst (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2))) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.map (Iso.inv (ρ_ x)))
        (CartesianMonoidalCategory.prodComparison F x (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫
          F.obj x ◁ CartesianMonoidalCategory.terminalComparison F))
      (fst (F.obj x) (tensorUnit.{v₂, u₂} D (𝒞 := inst_2)))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F.OplaxMonoidal
inst_7 : PreservesFiniteProducts F
a b : F.OplaxMonoidal
η :
  Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (OplaxMonoidal.η F)
    (OplaxMonoidal.η F)
δ :
  Eq (α :=
    (X Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (OplaxMonoidal.δ F) (OplaxMonoidal.δ F)
⊢ a = b

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F.OplaxMonoidal
inst_7 : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (η F)

Tactic:
toUnit_unique _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F.OplaxMonoidal
inst_7 : PreservesFiniteProducts F
a b : F.OplaxMonoidal
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (η F)

Tactic:
exact toUnit_unique _ _

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F.OplaxMonoidal
inst_7 : PreservesFiniteProducts F
a b : F.OplaxMonoidal
δ :
  ∀ (x : C),
    Eq (α :=
      (Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
      (OplaxMonoidal.δ F x) (OplaxMonoidal.δ F x)
⊢ Eq (α :=
    (X Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (OplaxMonoidal.δ F) (OplaxMonoidal.δ F)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F.OplaxMonoidal
inst_7 : PreservesFiniteProducts F
a b : F.OplaxMonoidal
x : C
δ :
  ∀ (x_1 : C),
    Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
      (OplaxMonoidal.δ F x x_1) (OplaxMonoidal.δ F x x_1)
⊢ Eq (α := (Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
    (OplaxMonoidal.δ F x) (OplaxMonoidal.δ F x)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
X Y Z : C
inst_6 : F.OplaxMonoidal
inst_7 : PreservesFiniteProducts F
a b : F.OplaxMonoidal
x x_1 : C
δ :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (CartesianMonoidalCategory.prodComparison F x x_1) (OplaxMonoidal.δ F x x_1)
δ₁ δ₂ :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (CartesianMonoidalCategory.prodComparison F x x_1) (CartesianMonoidalCategory.prodComparison F x x_1)
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x x_1) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj x_1))
    (OplaxMonoidal.δ F x x_1) (OplaxMonoidal.δ F x x_1)

Tactic:
rw [δ_of_cartesianMonoidalCategory, δ_of_cartesianMonoidalCategory]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X : C
rw :
  Eq (α := F.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (toUnit (F.obj X)) (ε F)) (Iso.inv (εIso F)))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map (toUnit X)) (Iso.inv (εIso F)))
⊢ Eq (α := F.obj X ⟶ F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (toUnit (F.obj X)) (ε F)) (F.map (toUnit X))

Tactic:
rw [← cancel_mono (εIso F).inv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.Monoidal.εIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X : C
⊢ Eq (α := F.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (toUnit (F.obj X)) (ε F)) (Iso.inv (εIso F)))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map (toUnit X)) (Iso.inv (εIso F)))

Tactic:
toUnit_unique ..

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X : C
⊢ Eq (α := F.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (CategoryStruct.comp (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (toUnit (F.obj X)) (ε F)) (Iso.inv (εIso F)))
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map (toUnit X)) (Iso.inv (εIso F)))

Tactic:
exact toUnit_unique ..

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
inst_4 : F.Monoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ Eq (α := F.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) (lift (F.map f) (F.map g))
        (μ F Y Z))
      (Iso.inv (μIso F Y Z)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) (F.map (lift f g)) (Iso.inv (μIso F Y Z)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (Iso.inv (μIso F X Y))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y) (F.map (fst X Y))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (Iso.inv (μIso F X Y))
      (fst (F.obj X) (F.obj Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (Iso.inv (μIso F X Y))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ F X Y) (F.map (snd X Y))))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (Iso.inv (μIso F X Y))
      (snd (F.obj X) (F.obj Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : G.Monoidal
inst_8 : (F ⋙ G).Monoidal
X Y : C
rw :
  Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
      (Iso.inv (μIso (F ⋙ G) X Y)))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X 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)))
      (Iso.inv (μIso (F ⋙ G) 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)
    (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 [← cancel_mono (μIso _ _ _).inv]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.Monoidal.μIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : G.Monoidal
inst_8 : (F ⋙ G).Monoidal
X Y : C
h_fst :
  Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶ (F ⋙ G).obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X 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)))
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
h_snd :
  Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶ (F ⋙ G).obj Y)
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X 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)))
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (snd ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶
      tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
      (Iso.inv (μIso (F ⋙ G) X Y)))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X 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)))
      (Iso.inv (μIso (F ⋙ G) X Y)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
E : Type u₃
inst_4 : Category.{v₃, u₃} E
inst_5 : CartesianMonoidalCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.Monoidal
inst_7 : G.Monoidal
inst_8 : (F ⋙ G).Monoidal
X Y : C
⊢ Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ⟶ (F ⋙ G).obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ (F ⋙ G) X Y)
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₃, u₃} (𝒞 := inst_4) ((F ⋙ G).obj X) ((F ⋙ G).obj Y))
      (CategoryStruct.comp (Y := (F ⋙ G).obj (tensorObj.{v₁, u₁} (𝒞 := inst) X 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)))
        (Iso.inv (μIso (F ⋙ G) X Y)))
      (fst ((F ⋙ G).obj X) ((F ⋙ G).obj Y)))

Tactic:
simp [← Functor.comp_obj, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.map_comp