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
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj B')
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
      (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') (snd (F.obj A') (F.obj B')))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
      (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) (snd (F.obj A') (F.obj B')))

Tactic:
simp only [Category.assoc, prodComparison_fst, tensorHom_fst, prodComparison_fst_assoc,
    prodComparison_snd, tensorHom_snd, prodComparison_snd_assoc, ← F.map_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_snd, CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst, CategoryTheory.CartesianMonoidalCategory.tensorHom_fst, CategoryTheory.CartesianMonoidalCategory.prodComparison_snd_assoc, CategoryTheory.CartesianMonoidalCategory.tensorHom_snd, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst_assoc, 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
A B B' : C
g : B ⟶ B'
h_fst :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
      (F.map (A ◁ g) ≫ prodComparison F A B') (fst (F.obj A) (F.obj B')))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
      (prodComparison F A B ≫ F.obj A ◁ F.map g) (fst (F.obj A) (F.obj B')))
h_snd :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj B')
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
      (F.map (A ◁ g) ≫ prodComparison F A B') (snd (F.obj A) (F.obj B')))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
      (prodComparison F A B ≫ F.obj A ◁ F.map g) (snd (F.obj A) (F.obj B')))
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
    (F.map (A ◁ g) ≫ prodComparison F A B') (prodComparison F A B ≫ F.obj A ◁ 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
A B B' : C
g : B ⟶ B'
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj A)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
      (F.map (A ◁ g) ≫ prodComparison F A B') (fst (F.obj A) (F.obj B')))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
      (prodComparison F A B ≫ F.obj A ◁ F.map g) (fst (F.obj A) (F.obj B')))

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
A B B' : C
g : B ⟶ B'
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj B')
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
      (F.map (A ◁ g) ≫ prodComparison F A B') (snd (F.obj A) (F.obj B')))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
      (prodComparison F A B ≫ F.obj A ◁ F.map g) (snd (F.obj A) (F.obj B')))

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
A B A' : C
f : A ⟶ A'
h_fst :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj A')
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
      (F.map (f ▷ B) ≫ prodComparison F A' B) (fst (F.obj A') (F.obj B)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
      (prodComparison F A B ≫ F.map f ▷ F.obj B) (fst (F.obj A') (F.obj B)))
h_snd :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
      (F.map (f ▷ B) ≫ prodComparison F A' B) (snd (F.obj A') (F.obj B)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
      (prodComparison F A B ≫ F.map f ▷ F.obj B) (snd (F.obj A') (F.obj B)))
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
    (F.map (f ▷ B) ≫ prodComparison F A' B) (prodComparison F A B ≫ F.map f ▷ 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 A' : C
f : A ⟶ A'
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj A')
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
      (F.map (f ▷ B) ≫ prodComparison F A' B) (fst (F.obj A') (F.obj B)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
      (prodComparison F A B ≫ F.map f ▷ F.obj B) (fst (F.obj A') (F.obj B)))

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
A B A' : C
f : A ⟶ A'
⊢ Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ F.obj B)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
      (F.map (f ▷ B) ≫ prodComparison F A' B) (snd (F.obj A') (F.obj B)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
      (prodComparison F A B ≫ F.map f ▷ F.obj B) (snd (F.obj A') (F.obj B)))

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
A B A' B' : C
inst_4 :
  IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B))
    (prodComparison F A B)
f : A ⟶ A'
g : B ⟶ B'
inst_5 :
  IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A' B')) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
    (prodComparison F A' B')
rw :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A' B')) (inv (prodComparison F A B) ≫ F.map (f ⊗ₘ g))
      (prodComparison F A' B'))
    (F.map f ⊗ₘ F.map g)
rw₁ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (inv (prodComparison F A B))
      (F.map (f ⊗ₘ g) ≫ prodComparison F A' B'))
    (F.map f ⊗ₘ F.map g)
rw₂ :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
    (F.map (f ⊗ₘ g) ≫ prodComparison F A' B') (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g))
rw₃ rw₄ :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B'))
    (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)) (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g))
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A' B'))
    (inv (prodComparison F A B) ≫ F.map (f ⊗ₘ g)) ((F.map f ⊗ₘ F.map g) ≫ inv (prodComparison F A' B'))

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural, CategoryTheory.IsIso.eq_comp_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
A B B' : C
inst_4 :
  IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B))
    (prodComparison F A B)
g : B ⟶ B'
inst_5 :
  IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B')) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
    (prodComparison F A B')
rw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A B')) (inv (prodComparison F A B) ≫ F.map (A ◁ g))
      (prodComparison F A B'))
    (F.obj A ◁ F.map g)
rw₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (inv (prodComparison F A B))
      (F.map (A ◁ g) ≫ prodComparison F A B'))
    (F.obj A ◁ F.map g)
rw₂ :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
    (F.map (A ◁ g) ≫ prodComparison F A B') (prodComparison F A B ≫ F.obj A ◁ F.map g)
rw₃ rw₄ :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B'))
    (prodComparison F A B ≫ F.obj A ◁ F.map g) (prodComparison F A B ≫ F.obj A ◁ F.map g)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A B'))
    (inv (prodComparison F A B) ≫ F.map (A ◁ g)) (F.obj A ◁ F.map g ≫ inv (prodComparison F A B'))

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerLeft]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft
-- 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 A' : C
inst_4 :
  IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B))
    (prodComparison F A B)
f : A ⟶ A'
inst_5 :
  IsIso (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A' B)) (Y := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
    (prodComparison F A' B)
rw :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A' B)) (inv (prodComparison F A B) ≫ F.map (f ▷ B))
      (prodComparison F A' B))
    (F.map f ▷ F.obj B)
rw₁ :
  Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (inv (prodComparison F A B))
      (F.map (f ▷ B) ≫ prodComparison F A' B))
    (F.map f ▷ F.obj B)
rw₂ :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
    (F.map (f ▷ B) ≫ prodComparison F A' B) (prodComparison F A B ≫ F.map f ▷ F.obj B)
rw₃ rw₄ :
  Eq (α := F.obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A') (F.obj B))
    (prodComparison F A B ≫ F.map f ▷ F.obj B) (prodComparison F A B ≫ F.map f ▷ F.obj B)
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B) ⟶ F.obj (tensorObj.{v, u} (𝒞 := inst) A' B))
    (inv (prodComparison F A B) ≫ F.map (f ▷ B)) (F.map f ▷ F.obj B ≫ inv (prodComparison F A' B))

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerRight]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerRight, CategoryTheory.IsIso.eq_comp_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
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A B : C
unfold :
  Eq (α :=
    (F ⋙ G).obj (tensorObj.{v, u} (𝒞 := inst) A B) ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_4) ((F ⋙ G).obj A) ((F ⋙ G).obj B))
    (lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
      (G.map (lift (F.map (fst A B)) (F.map (snd A B))))
      (lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.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))
    (prodComparison (F ⋙ G) A B)
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
      (G.map (prodComparison F A B)) (prodComparison G (F.obj A) (F.obj B)))

Tactic:
unfold prodComparison

Premises used: 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
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A B : C
h_fst :
  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))
      (lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd 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))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
        (G.map (lift (F.map (fst A B)) (F.map (snd A B))))
        (lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))))
      (fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)))
h_snd :
  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))
      (lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd 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))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
        (G.map (lift (F.map (fst A B)) (F.map (snd A B))))
        (lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (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))
    (lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd A B)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
      (G.map (lift (F.map (fst A B)) (F.map (snd A B))))
      (lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (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
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
A B : C
⊢ 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))
      (lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd 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))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
        (G.map (lift (F.map (fst A B)) (F.map (snd A B))))
        (lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))))
      (fst ((F ⋙ G).obj A) ((F ⋙ G).obj B)))

Tactic:
simp [← G.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
A B : C
⊢ 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))
      (lift ((F ⋙ G).map (fst A B)) ((F ⋙ G).map (snd 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))
      (CategoryStruct.comp (Y := G.obj (tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)))
        (G.map (lift (F.map (fst A B)) (F.map (snd A B))))
        (lift (G.map (fst (F.obj A) (F.obj B))) (G.map (snd (F.obj A) (F.obj B)))))
      (snd ((F ⋙ G).obj A) ((F ⋙ G).obj B)))

Tactic:
simp [← G.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
A B : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (𝟭 C) (tensorObj.{v, u} (𝒞 := inst) A B) ⟶
      tensorObj.{v, u} (𝒞 := inst) (Functor.obj.{v, v, u, u} (𝟭 C) A) (Functor.obj.{v, v, u, u} (𝟭 C) B))
    (prodComparison (𝟭 C) A B) (𝟙 (tensorObj.{v, u} (𝒞 := inst) A B))

Tactic:
lift_fst_snd

Premises used: CategoryTheory.CartesianMonoidalCategory.lift_fst_snd, CategoryTheory.CartesianMonoidalCategory.prodComparison
-- 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_1 B A' B' A x y : C
f : x ⟶ y
h_fst :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj y))
      ((Functor.obj (curriedTensor C) A ⋙ F).map f ≫ prodComparison F A y) (fst (F.obj A) (F.obj y)) =
    (prodComparison F A x ≫ (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).map f) ≫ fst (F.obj A) (F.obj y)
h_snd :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj y))
      ((Functor.obj (curriedTensor C) A ⋙ F).map f ≫ prodComparison F A y) (snd (F.obj A) (F.obj y)) =
    (prodComparison F A x ≫ (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).map f) ≫ snd (F.obj A) (F.obj y)
⊢ (Functor.obj (curriedTensor C) A ⋙ F).map f ≫ prodComparison F A y =
    prodComparison F A x ≫ (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).map f

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_1 B A' B' A x y : C
f : x ⟶ y
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj y))
      ((Functor.obj (curriedTensor C) A ⋙ F).map f ≫ prodComparison F A y) (fst (F.obj A) (F.obj y)) =
    (prodComparison F A x ≫ (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).map f) ≫ fst (F.obj A) (F.obj y)

Tactic:
simp only [Functor.comp_obj, curriedTensor_obj_obj,
      Functor.comp_map, curriedTensor_obj_map, Category.assoc, prodComparison_fst, whiskerLeft_fst,
      prodComparison_snd, prodComparison_snd_assoc, whiskerLeft_snd, ← F.map_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_snd, CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst, CategoryTheory.CartesianMonoidalCategory.prodComparison_snd_assoc, CategoryTheory.MonoidalCategory.curriedTensor_obj_map, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd, CategoryTheory.MonoidalCategory.curriedTensor_obj_obj, CategoryTheory.Functor.map_comp, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst, CategoryTheory.Functor.comp_map
-- 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_1 B A' B' A x y : C
f : x ⟶ y
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst_3) (F.obj A) (F.obj y))
      ((Functor.obj (curriedTensor C) A ⋙ F).map f ≫ prodComparison F A y) (snd (F.obj A) (F.obj y)) =
    (prodComparison F A x ≫ (F ⋙ Functor.obj (curriedTensor D) (F.obj A)).map f) ≫ snd (F.obj A) (F.obj y)

Tactic:
simp only [Functor.comp_obj, curriedTensor_obj_obj,
      Functor.comp_map, curriedTensor_obj_map, Category.assoc, prodComparison_fst, whiskerLeft_fst,
      prodComparison_snd, prodComparison_snd_assoc, whiskerLeft_snd, ← F.map_comp]

Premises used: CategoryTheory.CartesianMonoidalCategory.prodComparison_snd, CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.CartesianMonoidalCategory.prodComparison_fst, CategoryTheory.CartesianMonoidalCategory.prodComparison_snd_assoc, CategoryTheory.MonoidalCategory.curriedTensor_obj_map, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_snd, CategoryTheory.MonoidalCategory.curriedTensor_obj_obj, CategoryTheory.Functor.map_comp, CategoryTheory.CartesianMonoidalCategory.whiskerLeft_fst, CategoryTheory.Functor.comp_map