awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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)))
⊢ 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))
have 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))
Tactic: trans F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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)
    (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)))
have 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)))
Tactic: rw [← whiskerRight_snd (F.map (toUnit X)), δ_natural_left_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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
⊢ 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))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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) ⟶ 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)
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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)))
⊢ 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)
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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) ⟶ 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)
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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)))
⊢ 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)
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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) ⟶
      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)))
    (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)
have h_fst : 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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
⊢ 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))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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
⊢ 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))
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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
⊢ a = b
have η : Eq (α := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) (η F) (η F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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)
⊢ a = b
have δ : Eq (α := (X Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y))
  (δ F) (δ F)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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 (α :=
    (X Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F)
    (δ F)
have δ : ∀ (x : C),
  Eq (α := (Y : C) → F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x Y) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj x) (F.obj Y))
    (δ F x) (δ F x)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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))
    (δ F x) (δ F x)
have δ : ∀ (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))
    (δ F x x_1) (δ F x x_1)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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))
    (δ F x x_1) (δ F x x_1)
have δ : 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) (δ F x x_1)
Tactic: rw [δ_of_cartesianMonoidalCategory, δ_of_cartesianMonoidalCategory]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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))
    (OplaxMonoidal.δ F x x_1) (OplaxMonoidal.δ F x x_1)
have δ₁ : 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)
Tactic: rw [δ_of_cartesianMonoidalCategory, δ_of_cartesianMonoidalCategory]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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 ⟶ 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))
have 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)))
Tactic: rw [← cancel_mono (εIso F).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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 (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)))
have 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)))
Tactic: rw [← cancel_mono (μIso _ _ _).inv]