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
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)
⊢ 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'))
have 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)
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerLeft]
-- 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
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)
⊢ 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'))
have 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)
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerLeft]
-- 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
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)
⊢ 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))
have 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)
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerRight]
-- 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
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)
⊢ 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))
have 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)
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerRight]
-- 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
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)
⊢ 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))
have 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)
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerRight]
-- 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
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)
⊢ 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))
have 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)
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerRight]
-- 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
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) ⟶ 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)))
have 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)))))
Tactic: unfold prodComparison
-- 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
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) ⟶ 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)))))
have 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)))
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
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)))
⊢ 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)))))
have 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)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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
⊢ (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
have 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)
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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)
⊢ (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
have 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)
Tactic: apply hom_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
A : C
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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
⊢ (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
have 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
Tactic: ext z
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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
⊢ 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
have 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)
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
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)
⊢ 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
have 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)
Tactic: apply hom_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
E : Type u₂
inst_4 : Category.{v₂, u₂} E
inst_5 : CartesianMonoidalCategory.{v₂, u₂} E
G : Functor.{v₁, v₂, u₁, u₂} D E
⊢ 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))))
have 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)
Tactic: ext