awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_3 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_4 : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
⊢ Eq (α := (tensorObj.{v, u} (𝒞 := ObjectProperty.FullSubcategory.category P) X Y).obj (P := P) ⟶ Y.obj (P := P))
    (InducedCategory.Hom.hom (ObjectProperty.homMk (P := P) (snd (X.obj (P := P)) (Y.obj (P := P)))))
    (InducedCategory.Hom.hom
      (IsTerminal.from
            (IsTerminal.ofUniqueHom
              (fun (X : P.FullSubcategory) ↦ ObjectProperty.homMk (P := P) (toUnit (X.obj (P := P)))) ⋯)
            X ▷
          Y ≫
        Iso.hom (λ_ Y)))

Tactic:
exact snd_def X.1 Y.1

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.SemiCartesianMonoidalCategory.snd_def
-- 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.OplaxMonoidal
⊢ Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F)
    (CartesianMonoidalCategory.terminalComparison 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.OplaxMonoidal
X Y : C
trans :
  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)) (δ F X Y)
      (fst (F.obj X) (F.obj Y)))
    (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))
trans₁ :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X) (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))
    (F.map (fst X Y))
⊢ 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)) (δ F X Y)
      (fst (F.obj X) (F.obj Y)))
    (F.map (fst X Y))

Tactic:
trans F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.Functor.map, CategoryTheory.Iso.hom, CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- 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.OplaxMonoidal
X Y : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.map (X ◁ toUnit Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (fst (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))))
    (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))
⊢ 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)) (δ F X Y)
      (fst (F.obj X) (F.obj Y)))
    (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))

Tactic:
rw [← whiskerLeft_fst _ (F.map (toUnit Y)), δ_natural_right_assoc]

Premises used: CategoryTheory.Functor.map, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, CategoryTheory.Functor.OplaxMonoidal.δ_natural_right_assoc
-- 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.OplaxMonoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.map (X ◁ toUnit Y))
      (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (fst (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))))
    (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))

Tactic:
simp [← OplaxMonoidal.right_unitality_hom, rightUnitor_hom (F.obj X)]

Premises used: CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom, CategoryTheory.Functor.obj, CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom
-- 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.OplaxMonoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X) (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))
    (F.map (fst X Y))

Tactic:
simp [← Functor.map_comp, rightUnitor_hom]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.CartesianMonoidalCategory.rightUnitor_hom
-- 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.OplaxMonoidal
X Y : C
trans :
  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)) (δ F X Y)
      (snd (F.obj X) (F.obj Y)))
    (F.map (toUnit X ▷ Y) ≫ F.map (Iso.hom (λ_ Y)))
trans₁ :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj Y) (F.map (toUnit X ▷ Y) ≫ F.map (Iso.hom (λ_ Y)))
    (F.map (snd X Y))
⊢ 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)) (δ F X Y)
      (snd (F.obj X) (F.obj Y)))
    (F.map (snd X Y))

Tactic:
trans F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.Functor.map, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.Iso.hom, CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- 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.OplaxMonoidal
X Y : C
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj Y)
    (F.map (toUnit X ▷ Y) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj Y))
        (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) (snd (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj Y)))
    (F.map (toUnit X ▷ Y) ≫ F.map (Iso.hom (λ_ Y)))
⊢ 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)) (δ F X Y)
      (snd (F.obj X) (F.obj Y)))
    (F.map (toUnit X ▷ Y) ≫ F.map (Iso.hom (λ_ Y)))

Tactic:
rw [← whiskerRight_snd (F.map (toUnit X)), δ_natural_left_assoc]

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_natural_left_assoc, CategoryTheory.Functor.map, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, CategoryTheory.CartesianMonoidalCategory.whiskerRight_snd
-- 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.OplaxMonoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj Y)
    (F.map (toUnit X ▷ Y) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj Y))
        (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) Y) (snd (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj Y)))
    (F.map (toUnit X ▷ Y) ≫ F.map (Iso.hom (λ_ Y)))

Tactic:
simp [← OplaxMonoidal.left_unitality_hom, leftUnitor_hom (F.obj Y)]

Premises used: CategoryTheory.Functor.OplaxMonoidal.left_unitality_hom, CategoryTheory.Functor.obj, CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom
-- 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.OplaxMonoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj Y) (F.map (toUnit X ▷ Y) ≫ F.map (Iso.hom (λ_ Y)))
    (F.map (snd X Y))

Tactic:
simp [← Functor.map_comp, leftUnitor_hom]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom
-- 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.OplaxMonoidal
f : X ⟶ Y
g : X ⟶ Z
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) (F.map (lift f g)) (δ F Y Z))
      (fst (F.obj Y) (F.obj Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) (lift (F.map f) (F.map g))
      (fst (F.obj Y) (F.obj Z))
h_snd :
  CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) (F.map (lift f g)) (δ F Y Z))
      (snd (F.obj Y) (F.obj Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) (lift (F.map f) (F.map g))
      (snd (F.obj Y) (F.obj 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)) (F.map (lift f g)) (δ F Y Z))
    (lift (F.map f) (F.map g))

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
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
inst_4 : F.OplaxMonoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) (F.map (lift f g)) (δ F Y Z))
      (fst (F.obj Y) (F.obj Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) (lift (F.map f) (F.map g))
      (fst (F.obj Y) (F.obj Z))

Tactic:
simp [← 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
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
inst_4 : F.OplaxMonoidal
f : X ⟶ Y
g : X ⟶ Z
⊢ CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z))
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) (F.map (lift f g)) (δ F Y Z))
      (snd (F.obj Y) (F.obj Z)) =
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y) (F.obj Z)) (lift (F.map f) (F.map g))
      (snd (F.obj Y) (F.obj Z))

Tactic:
simp [← 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
⊢ IsIso (X := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Y := tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F)

Tactic:
η_of_cartesianMonoidalCategory F ▸ terminalComparison_isIso_of_preservesLimits F

Premises used: CategoryTheory.Functor.OplaxMonoidal.η_of_cartesianMonoidalCategory, Eq.rec, CategoryTheory.CartesianMonoidalCategory.terminalComparison_isIso_of_preservesLimits, Eq.symm
-- 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_1 Y_1 Z : C
inst_6 : F.OplaxMonoidal
inst_7 : PreservesFiniteProducts F
X Y : C
⊢ IsIso (X := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
    (δ F X Y)

Tactic:
δ_of_cartesianMonoidalCategory F X Y ▸ isIso_prodComparison_of_preservesLimit_pair F X Y

Premises used: CategoryTheory.Functor.OplaxMonoidal.δ_of_cartesianMonoidalCategory, Eq.rec, Eq.symm, CategoryTheory.CartesianMonoidalCategory.isIso_prodComparison_of_preservesLimit_pair
-- 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_1 Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_1 : C
f : X_2 ⟶ Y_1
X : C
h_fst :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X_2 X) ⟶ F.obj Y_1)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y_1) (F.obj X))
      (CartesianMonoidalCategory.prodComparison F X_2 X ≫ F.map f ▷ F.obj X) (fst (F.obj Y_1) (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y_1) (F.obj X))
      (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y_1 X) (fst (F.obj Y_1) (F.obj X)))
h_snd :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X_2 X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y_1) (F.obj X))
      (CartesianMonoidalCategory.prodComparison F X_2 X ≫ F.map f ▷ F.obj X) (snd (F.obj Y_1) (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y_1) (F.obj X))
      (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y_1 X) (snd (F.obj Y_1) (F.obj X)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X_2 X) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y_1) (F.obj X))
    (CartesianMonoidalCategory.prodComparison F X_2 X ≫ F.map f ▷ F.obj X)
    (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y_1 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_1 Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_1 : C
f : X_2 ⟶ Y_1
X : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X_2 X) ⟶ F.obj Y_1)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y_1) (F.obj X))
      (CartesianMonoidalCategory.prodComparison F X_2 X ≫ F.map f ▷ F.obj X) (fst (F.obj Y_1) (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y_1) (F.obj X))
      (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y_1 X) (fst (F.obj Y_1) (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_1 Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_1 : C
f : X_2 ⟶ Y_1
X : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X_2 X) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y_1) (F.obj X))
      (CartesianMonoidalCategory.prodComparison F X_2 X ≫ F.map f ▷ F.obj X) (snd (F.obj Y_1) (F.obj X)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj Y_1) (F.obj X))
      (F.map (f ▷ X) ≫ CartesianMonoidalCategory.prodComparison F Y_1 X) (snd (F.obj Y_1) (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_1 Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_1 X : C
g : X_2 ⟶ Y_1
h_fst :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X_2) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y_1))
      (CartesianMonoidalCategory.prodComparison F X X_2 ≫ F.obj X ◁ F.map g) (fst (F.obj X) (F.obj Y_1)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y_1))
      (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y_1) (fst (F.obj X) (F.obj Y_1)))
h_snd :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X_2) ⟶ F.obj Y_1)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y_1))
      (CartesianMonoidalCategory.prodComparison F X X_2 ≫ F.obj X ◁ F.map g) (snd (F.obj X) (F.obj Y_1)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y_1))
      (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y_1) (snd (F.obj X) (F.obj Y_1)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X_2) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y_1))
    (CartesianMonoidalCategory.prodComparison F X X_2 ≫ F.obj X ◁ F.map g)
    (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y_1)

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_1 Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_1 X : C
g : X_2 ⟶ Y_1
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X_2) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y_1))
      (CartesianMonoidalCategory.prodComparison F X X_2 ≫ F.obj X ◁ F.map g) (fst (F.obj X) (F.obj Y_1)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y_1))
      (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y_1) (fst (F.obj X) (F.obj Y_1)))

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_1 Y Z : C
inst_6 : F_1.OplaxMonoidal
inst_7 : PreservesFiniteProducts F_1
F : Functor.{v₁, v₂, u₁, u₂} C D
X_2 Y_1 X : C
g : X_2 ⟶ Y_1
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X_2) ⟶ F.obj Y_1)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y_1))
      (CartesianMonoidalCategory.prodComparison F X X_2 ≫ F.obj X ◁ F.map g) (snd (F.obj X) (F.obj Y_1)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y_1))
      (F.map (X ◁ g) ≫ CartesianMonoidalCategory.prodComparison F X Y_1) (snd (F.obj X) (F.obj Y_1)))

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)
    (CategoryStruct.comp (Y :=
      tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (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)))
      (fst (F.obj x) (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)
      (fst (F.obj x) (tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x_1) (F.obj x_2))))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp