awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : BraidedCategory.{v, u} C
e₁ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₁ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₁ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₁ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₁ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₂ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₂ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₂ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₂ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₂ X Z).hom ▷ Y
⊢ { braiding := e₁, braiding_naturality_right := a₁, braiding_naturality_left := @b₁, hexagon_forward := c₁,
      hexagon_reverse := d₁ : BraidedCategory.{v, u} C } =
    { braiding := e₂, braiding_naturality_right := a₂, braiding_naturality_left := @b₂, hexagon_forward := c₂,
      hexagon_reverse := d₂ }
have e_braiding : e₁ = e₂
Tactic: congr
-- 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
inst_3 : BraidedCategory.{v, u} C
e₁ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₁ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₁ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₁ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₁ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₂ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₂ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₂ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₂ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₂ X Z).hom ▷ Y
⊢ e₁ = e₂
have e_braiding : ∀ (x x_1 : C), (e₁ x x_1).hom ≫ fst x_1 x = (e₂ x x_1).hom ≫ fst x_1 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
inst_3 : BraidedCategory.{v, u} C
e₁ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₁ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₁ X Z).hom = (e₁ X Y).hom ≫ f ▷ X
b₁ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₁ Y Z).hom = (e₁ X Z).hom ≫ Z ◁ f
c₁ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₁ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₁ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₁ X Z).hom
d₁ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₁ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₁ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₁ X Z).hom ▷ Y
e₂ : (X Y : C) → tensorObj.{v, u} (𝒞 := inst_1) X Y ≅ tensorObj.{v, u} (𝒞 := inst_1) Y X
a₂ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), X ◁ f ≫ (e₂ X Z).hom = (e₂ X Y).hom ≫ f ▷ X
b₂ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (e₂ Y Z).hom = (e₂ X Z).hom ≫ Z ◁ f
c₂ :
  ∀ (X Y Z : C),
    Iso.hom (α_ X Y Z) ≫ Iso.hom (e₂ X (tensorObj.{v, u} (𝒞 := inst_1) Y Z)) ≫ Iso.hom (α_ Y Z X) =
      (e₂ X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (e₂ X Z).hom
d₂ :
  ∀ (X Y Z : C),
    Iso.inv (α_ X Y Z) ≫ Iso.hom (e₂ (tensorObj.{v, u} (𝒞 := inst_1) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
      X ◁ (e₂ Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (e₂ X Z).hom ▷ Y
e_braiding : ∀ (x x_1 : C), (e₁ x x_1).hom ≫ fst x_1 x = (e₂ x x_1).hom ≫ fst x_1 x
⊢ e₁ = e₂
have e_braiding₁ : ∀ (x x_1 : C), (e₁ x x_1).hom ≫ snd x_1 x = (e₂ x x_1).hom ≫ snd x_1 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
inst_3 toBraidedCategory : BraidedCategory.{v, u} C
symmetry : ∀ (X Y : C), Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj.{v, u} (𝒞 := inst_1) X Y)
toBraidedCategory_1 : BraidedCategory.{v, u} C
symmetry_1 : ∀ (X Y : C), Iso.hom (β_ X Y) ≫ Iso.hom (β_ Y X) = 𝟙 (tensorObj.{v, u} (𝒞 := inst_1) X Y)
⊢ { toBraidedCategory := toBraidedCategory, symmetry := symmetry : SymmetricCategory.{v, u} C } =
    { toBraidedCategory := toBraidedCategory_1, symmetry := symmetry_1 }
have e_toBraidedCategory : toBraidedCategory = toBraidedCategory_1
Tactic: congr
-- 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 :
  IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_2)) (terminalComparison F)
⊢ PreservesLimit (Functor.empty C) F
have apply : IsLimit (F.mapCone (asEmptyCone (tensorUnit.{v, u} C (𝒞 := inst))))
Tactic: apply preservesLimit_of_preserves_limit_cone isTerminalTensorUnit
-- 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 :
  IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_2)) (terminalComparison F)
⊢ IsLimit (F.mapCone (asEmptyCone (tensorUnit.{v, u} C (𝒞 := inst))))
have hi : Cone.pt.{0, v₁, 0, u₁} (asEmptyCone (tensorUnit.{v₁, u₁} D (𝒞 := inst_2))) ≅
  (F.mapCone (asEmptyCone (tensorUnit.{v, u} C (𝒞 := inst)))).pt
Tactic: apply isLimitChangeEmptyCone D isTerminalTensorUnit
-- 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
inst_7 : PreservesLimit (Functor.empty C) F
⊢ IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst_1))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_3))
    (terminalComparison F)
have rw : IsIso (X := F.obj (tensorUnit.{v, u} C (𝒞 := inst_1))) (Y := tensorUnit.{v₁, u₁} D (𝒞 := inst_3))
  (Iso.hom (preservesTerminalIso F))
Tactic: rw [← preservesTerminalIso_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
A B A' B' : C
f : A ⟶ A'
g : B ⟶ B'
⊢ 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))
have 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 ⊗ₘ 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.map f ⊗ₘ F.map g)) (fst (F.obj A') (F.obj B')))
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
A B A' B' : C
f : A ⟶ A'
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 (f ⊗ₘ 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.map f ⊗ₘ F.map g)) (fst (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 ⊗ₘ g) ≫ prodComparison F A' B') (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g))
have 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 ⊗ₘ 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: 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
A B B' : C
g : B ⟶ 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)
have 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')))
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
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')))
⊢ 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)
have 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')))
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
A B A' : C
f : A ⟶ A'
⊢ 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)
have 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)))
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
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)))
⊢ 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)
have 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)))
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
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')
⊢ 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'))
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 ⊗ₘ g))
    (prodComparison F A' B'))
  (F.map f ⊗ₘ F.map g)
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]
-- 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' 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)
⊢ 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'))
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 ⊗ₘ g) ≫ prodComparison F A' B'))
  (F.map f ⊗ₘ F.map g)
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]
-- 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' 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)
⊢ 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'))
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 ⊗ₘ g) ≫ prodComparison F A' B') (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]
-- 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' 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))
⊢ 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'))
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.map g)) (prodComparison F A B ≫ (F.map f ⊗ₘ F.map g))
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]
-- 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')
⊢ 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 (α := 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)
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)
⊢ 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 (α := 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)
Tactic: rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerLeft]