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
F : Functor.{v, v₁, u, u₁} C D
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A x : C
⊢ Eq (α :=
    (Functor.obj (curriedTensor C) A ⋙ F ⋙ G).obj x ⟶ ((F ⋙ G) ⋙ Functor.obj (curriedTensor E) ((F ⋙ G).obj A)).obj x)
    (NatTrans.app (prodComparisonNatTrans (F ⋙ G) A) x)
    (NatTrans.app
      (CategoryStruct.comp (Y := (F ⋙ Functor.obj (curriedTensor D) (F.obj A)) ⋙ G)
        (Functor.whiskerRight (prodComparisonNatTrans F A) G) (F.whiskerLeft (prodComparisonNatTrans G (F.obj A))))
      x)

Tactic:
simp [prodComparison_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A : C
w :
  ∀ (x : C),
    Eq.{v + 1} (α :=
      Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) A ⋙ 𝟭 C) x ⟶
        Functor.obj.{v, v, u, u} (𝟭 C ⋙ Functor.obj (curriedTensor C) (Functor.obj.{v, v, u, u} (𝟭 C) A)) x)
      (NatTrans.app (prodComparisonNatTrans (𝟭 C) A) x) (NatTrans.app (𝟙 (Functor.obj (curriedTensor C) A ⋙ 𝟭 C)) x)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (Functor.obj (curriedTensor C) A ⋙ 𝟭 C)
      (𝟭 C ⋙ Functor.obj (curriedTensor C) (Functor.obj.{v, v, u, u} (𝟭 C) A)))
    (prodComparisonNatTrans (𝟭 C) A) (𝟙 (Functor.obj (curriedTensor C) A ⋙ 𝟭 C))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A x : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) A ⋙ 𝟭 C) x ⟶
      Functor.obj.{v, v, u, u} (𝟭 C ⋙ Functor.obj (curriedTensor C) (Functor.obj.{v, v, u, u} (𝟭 C) A)) x)
    (NatTrans.app (prodComparisonNatTrans (𝟭 C) A) x) (NatTrans.app (𝟙 (Functor.obj (curriedTensor C) A ⋙ 𝟭 C)) x)

Tactic:
simp
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E : Type u₂
inst_5 : Category.{v₂, u₂} E
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A B A' B' x y : C
f : x ⟶ y
w :
  ∀ (z : C),
    NatTrans.app ((curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) F).map f ≫ prodComparisonNatTrans F y)
        z =
      NatTrans.app
        (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F).map f) z
⊢ (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) F).map f ≫ prodComparisonNatTrans F y =
    prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F).map f

Tactic:
ext z
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E : Type u₂
inst_5 : Category.{v₂, u₂} E
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A B A' B' x y : C
f : x ⟶ y
z : C
w :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj y) (F.obj z))
      (NatTrans.app
        ((curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) F).map f ≫ prodComparisonNatTrans F y) z)
      (fst (F.obj y) (F.obj z)) =
    NatTrans.app
        (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F).map f) z ≫
      fst (F.obj y) (F.obj z)
w₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj y) (F.obj z))
      (NatTrans.app
        ((curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) F).map f ≫ prodComparisonNatTrans F y) z)
      (snd (F.obj y) (F.obj z)) =
    NatTrans.app
        (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F).map f) z ≫
      snd (F.obj y) (F.obj z)
⊢ NatTrans.app ((curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) F).map f ≫ prodComparisonNatTrans F y)
      z =
    NatTrans.app
      (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F).map f) z

Tactic:
apply hom_ext

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E : Type u₂
inst_5 : Category.{v₂, u₂} E
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj y) (F.obj z))
      (NatTrans.app
        ((curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) F).map f ≫ prodComparisonNatTrans F y) z)
      (fst (F.obj y) (F.obj z)) =
    NatTrans.app
        (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F).map f) z ≫
      fst (F.obj y) (F.obj z)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E : Type u₂
inst_5 : Category.{v₂, u₂} E
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A B A' B' x y : C
f : x ⟶ y
z : C
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj y) (F.obj z))
      (NatTrans.app
        ((curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) F).map f ≫ prodComparisonNatTrans F y) z)
      (snd (F.obj y) (F.obj z)) =
    NatTrans.app
        (prodComparisonNatTrans F x ≫ (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F).map f) z ≫
      snd (F.obj y) (F.obj z)

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
F : Functor.{v, v₁, u, u₁} C D
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
w :
  ∀ (x x_1 : C),
    Eq (α :=
      ((curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C E) (F ⋙ G)).obj x).obj x_1 ⟶
        (((F ⋙ G) ⋙ curriedTensor E ⋙ Functor.obj (Functor.whiskeringLeft C E E) (F ⋙ G)).obj x).obj x_1)
      (NatTrans.app (NatTrans.app (prodComparisonBifunctorNatTrans (F ⋙ G)) x) x_1)
      (NatTrans.app
        (NatTrans.app
          (CategoryStruct.comp (Y :=
            (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F) ⋙
              Functor.obj (Functor.whiskeringRight C D E) G)
            (Functor.whiskerRight (prodComparisonBifunctorNatTrans F) (Functor.obj (Functor.whiskeringRight C D E) G))
            (F.whiskerLeft
              (Functor.whiskerRight (prodComparisonBifunctorNatTrans G)
                (Functor.obj (Functor.whiskeringLeft C D E) F))))
          x)
        x_1)
⊢ Eq (α :=
    curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C E) (F ⋙ G) ⟶
      (F ⋙ G) ⋙ curriedTensor E ⋙ Functor.obj (Functor.whiskeringLeft C E E) (F ⋙ G))
    (prodComparisonBifunctorNatTrans (F ⋙ G))
    (CategoryStruct.comp (Y :=
      (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F) ⋙
        Functor.obj (Functor.whiskeringRight C D E) G)
      (Functor.whiskerRight (prodComparisonBifunctorNatTrans F) (Functor.obj (Functor.whiskeringRight C D E) G))
      (F.whiskerLeft
        (Functor.whiskerRight (prodComparisonBifunctorNatTrans G) (Functor.obj (Functor.whiskeringLeft C D E) 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
F : Functor.{v, v₁, u, u₁} C D
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
x x_1 : C
⊢ Eq (α :=
    ((curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C E) (F ⋙ G)).obj x).obj x_1 ⟶
      (((F ⋙ G) ⋙ curriedTensor E ⋙ Functor.obj (Functor.whiskeringLeft C E E) (F ⋙ G)).obj x).obj x_1)
    (NatTrans.app (NatTrans.app (prodComparisonBifunctorNatTrans (F ⋙ G)) x) x_1)
    (NatTrans.app
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F) ⋙
            Functor.obj (Functor.whiskeringRight C D E) G)
          (Functor.whiskerRight (prodComparisonBifunctorNatTrans F) (Functor.obj (Functor.whiskeringRight C D E) G))
          (F.whiskerLeft
            (Functor.whiskerRight (prodComparisonBifunctorNatTrans G) (Functor.obj (Functor.whiskeringLeft C D E) F))))
        x)
      x_1)

Tactic:
simp [prodComparison_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_comp
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E_1 : Type u₂
inst_5 : Category.{v₂, u₂} E_1
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E_1
G_1 : Functor.{v₁, v₂, u₁, u₂} D E_1
A_1 B A' B' : C
E : Type u₂
inst_7 : Category.{v₂, u₂} E
inst_8 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A : C
inst_9 :
  ∀ (B : C),
    IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst_1) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj B))
      (prodComparison F A B)
⊢ ∀ (X : C),
    IsIso (X := (Functor.obj (curriedTensor C) A ⋙ F).obj X) (Y := (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).obj X)
      (NatTrans.app (prodComparisonNatTrans F A) X)

Tactic:
assumption
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E_1 : Type u₂
inst_5 : Category.{v₂, u₂} E_1
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E_1
G_1 : Functor.{v₁, v₂, u₁, u₂} D E_1
A_1 B A' B' : C
E : Type u₂
inst_7 : Category.{v₂, u₂} E
inst_8 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A : C
inst_9 :
  ∀ (B : C),
    IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst_1) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj B))
      (prodComparison F A B)
this : ∀ (X : C),
  IsIso (X := (Functor.obj (curriedTensor C) A ⋙ F).obj X) (Y := (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).obj X)
    (NatTrans.app (prodComparisonNatTrans F A) X) :=
  inst_9
⊢ IsIso (X := Functor.obj (curriedTensor C) A ⋙ F) (Y := F ⋙ Functor.obj (curriedTensor D) (F.obj A))
    (prodComparisonNatTrans F A)

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E_1 : Type u₂
inst_5 : Category.{v₂, u₂} E_1
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E_1
G_1 : Functor.{v₁, v₂, u₁, u₂} D E_1
A B A' B' : C
E : Type u₂
inst_7 : Category.{v₂, u₂} E
inst_8 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
inst_9 :
  ∀ (A B : C),
    IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst_1) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj B))
      (prodComparison F A B)
x : C
⊢ IsIso (X := Functor.obj (curriedTensor C) x ⋙ F) (Y := F ⋙ Functor.obj (curriedTensor D) (F.obj x))
    (prodComparisonNatTrans F x)

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E_1 : Type u₂
inst_5 : Category.{v₂, u₂} E_1
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E_1
G_1 : Functor.{v₁, v₂, u₁, u₂} D E_1
A B A' B' : C
E : Type u₂
inst_7 : Category.{v₂, u₂} E
inst_8 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
inst_9 :
  ∀ (A B : C),
    IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst_1) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj B))
      (prodComparison F A B)
this : ∀ (X : C),
  IsIso (X := (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) F).obj X) (Y :=
    (F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F).obj X)
    (NatTrans.app (prodComparisonBifunctorNatTrans F) X) :=
  ⋯
⊢ IsIso (X := curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) F) (Y :=
    F ⋙ curriedTensor D ⋙ Functor.obj (Functor.whiskeringLeft C D D) F) (prodComparisonBifunctorNatTrans F)

Tactic:
apply NatIso.isIso_of_isIso_app

Premises used: CategoryTheory.NatIso.isIso_of_isIso_app
-- 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
A B : C
inst_4 : PreservesLimit (pair A B) F
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B))
    (Iso.hom (prodComparisonIso F A B)) (prodComparison F A B)

Tactic:
rfl

Premises used: CategoryTheory.CartesianMonoidalCategory.lift, CategoryTheory.CartesianMonoidalCategory.prodComparison, rfl
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E_1 : Type u₂
inst_5 : Category.{v₂, u₂} E_1
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E_1
G_1 : Functor.{v₁, v₂, u₁, u₂} D E_1
A B A' B' : C
E : Type u₂
inst_7 : Category.{v₂, u₂} E
inst_8 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
inst_9 : PreservesLimit (pair A B) F
rw :
  IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst_1) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj B))
    (Iso.hom (prodComparisonIso F A B))
⊢ IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst_1) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj B))
    (prodComparison F A B)

Tactic:
rw [← prodComparisonIso_hom]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparisonIso_hom
-- 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
D : Type u₁
inst_3 : Category.{v₁, u₁} D
inst_4 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
E_1 : Type u₂
inst_5 : Category.{v₂, u₂} E_1
inst_6 : CartesianMonoidalCategory.{v₂, u₂} E_1
G_1 : Functor.{v₁, v₂, u₁, u₂} D E_1
A B A' B' : C
E : Type u₂
inst_7 : Category.{v₂, u₂} E
inst_8 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
inst_9 : PreservesLimit (pair A B) F
⊢ IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst_1) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj B))
    (Iso.hom (prodComparisonIso F A B))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A B : C
w :
  CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B))
      (Iso.hom (prodComparisonIso (𝟭 C) A B))
      (fst (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B)) =
    Iso.hom (Iso.refl (Functor.obj.{v, v, u, u} (𝟭 C) (tensorObj.{v, u} (𝒞 := inst) A B))) ≫
      fst (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B)
w₁ :
  CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B))
      (Iso.hom (prodComparisonIso (𝟭 C) A B))
      (snd (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B)) =
    Iso.hom (Iso.refl (Functor.obj.{v, v, u, u} (𝟭 C) (tensorObj.{v, u} (𝒞 := inst) A B))) ≫
      snd (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B)
⊢ prodComparisonIso (𝟭 C) A B = Iso.refl (Functor.obj.{v, v, u, u} (𝟭 C) (tensorObj.{v, u} (𝒞 := inst) A B))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A B : C
⊢ CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B))
      (Iso.hom (prodComparisonIso (𝟭 C) A B))
      (fst (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B)) =
    Iso.hom (Iso.refl (Functor.obj.{v, v, u, u} (𝟭 C) (tensorObj.{v, u} (𝒞 := inst) A B))) ≫
      fst (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
A B : C
⊢ CategoryStruct.comp (Y :=
      tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B))
      (Iso.hom (prodComparisonIso (𝟭 C) A B))
      (snd (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B)) =
    Iso.hom (Iso.refl (Functor.obj.{v, v, u, u} (𝟭 C) (tensorObj.{v, u} (𝒞 := inst) A B))) ≫
      snd (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B)

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
A B : C
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
inst_6 : PreservesLimit (pair A B) F
inst_7 : PreservesLimit (pair A B) (F ⋙ G)
inst_8 : PreservesLimit (pair (F.obj A) (F.obj B)) G
w :
  Eq (α := (F ⋙ G).obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ (F ⋙ G).obj A)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (Iso.hom (prodComparisonIso (F ⋙ G) A B)) (fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (Iso.hom
        (Iso.trans (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
          (G.mapIso (prodComparisonIso F A B)) (prodComparisonIso G (F.obj A) (F.obj B))))
      (fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)))
w₁ :
  Eq (α := (F ⋙ G).obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ (F ⋙ G).obj B)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (Iso.hom (prodComparisonIso (F ⋙ G) A B)) (snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (Iso.hom
        (Iso.trans (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
          (G.mapIso (prodComparisonIso F A B)) (prodComparisonIso G (F.obj A) (F.obj B))))
      (snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)))
⊢ Eq (α :=
    (F ⋙ G).obj (tensorObj.{v, u} (𝒞 := inst) A B) ≅ tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
    (prodComparisonIso (F ⋙ G) A B)
    (Iso.trans (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B))) (G.mapIso (prodComparisonIso F A B))
      (prodComparisonIso G (F.obj A) (F.obj B)))

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
A B : C
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
inst_6 : PreservesLimit (pair A B) F
inst_7 : PreservesLimit (pair A B) (F ⋙ G)
inst_8 : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ Eq (α := (F ⋙ G).obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ (F ⋙ G).obj A)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (Iso.hom (prodComparisonIso (F ⋙ G) A B)) (fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (Iso.hom
        (Iso.trans (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
          (G.mapIso (prodComparisonIso F A B)) (prodComparisonIso G (F.obj A) (F.obj B))))
      (fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)))

Tactic:
simp [CartesianMonoidalCategory.prodComparison, ← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.CartesianMonoidalCategory.prodComparison
-- 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
A B : C
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
inst_6 : PreservesLimit (pair A B) F
inst_7 : PreservesLimit (pair A B) (F ⋙ G)
inst_8 : PreservesLimit (pair (F.obj A) (F.obj B)) G
⊢ Eq (α := (F ⋙ G).obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ (F ⋙ G).obj B)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (Iso.hom (prodComparisonIso (F ⋙ G) A B)) (snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
      (Iso.hom
        (Iso.trans (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
          (G.mapIso (prodComparisonIso F A B)) (prodComparisonIso G (F.obj A) (F.obj B))))
      (snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)))

Tactic:
simp [CartesianMonoidalCategory.prodComparison, ← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.CartesianMonoidalCategory.prodComparison