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
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))
    (prodComparison F A B)
have 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))
Tactic: rw [← prodComparisonIso_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
A B : C
⊢ prodComparisonIso (𝟭 C) A B = Iso.refl (Functor.obj.{v, v, u, u} (𝟭 C) (tensorObj.{v, u} (𝒞 := inst) A B))
have 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)
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
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)
⊢ prodComparisonIso (𝟭 C) A B = Iso.refl (Functor.obj.{v, v, u, u} (𝟭 C) (tensorObj.{v, u} (𝒞 := inst) A B))
have 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)
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 : 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) ≅ 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)))
have 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)))
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 : 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)))
⊢ 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)))
have 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)))
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 : 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)
⊢ PreservesLimit (pair A B) F
have apply : IsLimit (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))
Tactic: apply preservesLimit_of_preserves_limit_cone (tensorProductIsBinaryProduct A B)
-- 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 : 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)
⊢ IsLimit (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))
have refine_1 : BinaryFan.fst
    ((Cone.postcompose (pairComp A B F).hom).obj
      (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))) =
  Iso.hom
      (Iso.refl
        ((Cone.postcompose (pairComp A B F).hom).obj
            (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).pt) ≫
    BinaryFan.fst
      (Cone.extend
        (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)) (fst (F.obj A) (F.obj B))
          (snd (F.obj A) (F.obj B)))
        (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (prodComparison F A B))
Tactic: refine IsLimit.equivOfNatIsoOfIso (pairComp A B F) _
    ((BinaryFan.mk (fst (F.obj A) (F.obj B)) (snd _ _)).extend (prodComparison F A B))
      (BinaryFan.ext (by exact Iso.refl _) ?_ ?_) |>.invFun
      (IsLimit.extendIso _ (tensorProductIsBinaryProduct (F.obj A) (F.obj B)))
-- 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 : 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)
refine_1 :
  BinaryFan.fst
      ((Cone.postcompose (pairComp A B F).hom).obj
        (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))) =
    Iso.hom
        (Iso.refl
          ((Cone.postcompose (pairComp A B F).hom).obj
              (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).pt) ≫
      BinaryFan.fst
        (Cone.extend
          (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)) (fst (F.obj A) (F.obj B))
            (snd (F.obj A) (F.obj B)))
          (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (prodComparison F A B))
⊢ IsLimit (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))
have refine_2 : BinaryFan.snd
    ((Cone.postcompose (pairComp A B F).hom).obj
      (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))) =
  Iso.hom
      (Iso.refl
        ((Cone.postcompose (pairComp A B F).hom).obj
            (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).pt) ≫
    BinaryFan.snd
      (Cone.extend
        (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)) (fst (F.obj A) (F.obj B))
          (snd (F.obj A) (F.obj B)))
        (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (prodComparison F A B))
Tactic: refine IsLimit.equivOfNatIsoOfIso (pairComp A B F) _
    ((BinaryFan.mk (fst (F.obj A) (F.obj B)) (snd _ _)).extend (prodComparison F A B))
      (BinaryFan.ext (by exact Iso.refl _) ?_ ?_) |>.invFun
      (IsLimit.extendIso _ (tensorProductIsBinaryProduct (F.obj A) (F.obj B)))
-- 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 : 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)
⊢ BinaryFan.fst
      ((Cone.postcompose (pairComp A B F).hom).obj
        (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))) =
    Iso.hom
        (Iso.refl
          ((Cone.postcompose (pairComp A B F).hom).obj
              (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).pt) ≫
      BinaryFan.fst
        (Cone.extend
          (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)) (fst (F.obj A) (F.obj B))
            (snd (F.obj A) (F.obj B)))
          (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (prodComparison F A B))
have refine_1 : Eq (α :=
  Functor.obj.{0, v₁, 0, u₁}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        ((Cone.postcompose (pairComp A B F).hom).obj
            (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).pt)
      { as := WalkingPair.left : Discrete WalkingPair } ⟶
    Functor.obj.{0, v₁, 0, u₁} (pair (F.obj A) (F.obj B)) { as := WalkingPair.left : Discrete WalkingPair })
  (((Cone.postcompose (pairComp A B F).hom).obj
          (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).π.app
    { as := WalkingPair.left })
  (Iso.hom
      (Iso.refl
        ((Cone.postcompose (pairComp A B F).hom).obj
            (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).pt) ≫
    NatTrans.app
      (Cone.π
        (Cone.extend
          (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)) (fst (F.obj A) (F.obj B))
            (snd (F.obj A) (F.obj B)))
          (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (prodComparison F A B)))
      { as := WalkingPair.left })
Tactic: dsimp only [BinaryFan.fst]
-- 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 : 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)
⊢ BinaryFan.snd
      ((Cone.postcompose (pairComp A B F).hom).obj
        (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))) =
    Iso.hom
        (Iso.refl
          ((Cone.postcompose (pairComp A B F).hom).obj
              (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).pt) ≫
      BinaryFan.snd
        (Cone.extend
          (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)) (fst (F.obj A) (F.obj B))
            (snd (F.obj A) (F.obj B)))
          (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (prodComparison F A B))
have refine_2 : Eq (α :=
  Functor.obj.{0, v₁, 0, u₁}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        ((Cone.postcompose (pairComp A B F).hom).obj
            (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).pt)
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    Functor.obj.{0, v₁, 0, u₁} (pair (F.obj A) (F.obj B)) { as := WalkingPair.right : Discrete WalkingPair })
  (((Cone.postcompose (pairComp A B F).hom).obj
          (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).π.app
    { as := WalkingPair.right })
  (Iso.hom
      (Iso.refl
        ((Cone.postcompose (pairComp A B F).hom).obj
            (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))).pt) ≫
    NatTrans.app
      (Cone.π
        (Cone.extend
          (BinaryFan.mk (P := tensorObj.{v₁, u₁} (𝒞 := inst_2) (F.obj A) (F.obj B)) (fst (F.obj A) (F.obj B))
            (snd (F.obj A) (F.obj B)))
          (X := F.obj (tensorObj.{v, u} (𝒞 := inst) A B)) (prodComparison F A B)))
      { as := WalkingPair.right })
Tactic: dsimp only [BinaryFan.snd]
-- 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 :
  ∀ (A B : C),
    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)
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F
have preservesLimit : autoParam (∀ {K : Functor.{0, v, 0, u} (Discrete WalkingPair) C}, PreservesLimit K F)
  PreservesLimitsOfShape.preservesLimit._autoParam
Tactic: constructor
-- 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 :
  ∀ (A B : C),
    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)
K : Functor.{0, v, 0, u} (Discrete WalkingPair) C
⊢ PreservesLimit K F
have preservesLimit : PreservesLimit
  (pair (K.obj { as := WalkingPair.left : Discrete WalkingPair })
    (K.obj { as := WalkingPair.right : Discrete WalkingPair }))
  F
Tactic: refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoPair K).symm ?_
-- 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
P : ObjectProperty.{v, u} C
inst_3 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_4 : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
x : P.FullSubcategory
x_1 : x ⟶ tensorUnit.{v, u} P.FullSubcategory (𝒞 := ObjectProperty.FullSubcategory.category P)
⊢ x_1 =
    (fun (X : P.FullSubcategory) ↦
        (ObjectProperty.homMk (P := P) (toUnit (X.obj (P := P))) :
          X ⟶ tensorUnit.{v, u} P.FullSubcategory (𝒞 := ObjectProperty.FullSubcategory.category P)))
      x
have h : x_1.hom =
  InducedCategory.Hom.hom
    ((fun (X : P.FullSubcategory) ↦
        (ObjectProperty.homMk (P := P) (toUnit (X.obj (P := P))) :
          X ⟶ tensorUnit.{v, u} P.FullSubcategory (𝒞 := ObjectProperty.FullSubcategory.category P)))
      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
P : ObjectProperty.{v, u} C
inst_3 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_4 : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
⊢ Eq (α := tensorObj.{v, u} (𝒞 := ObjectProperty.FullSubcategory.category P) X Y ⟶ X)
    (ObjectProperty.homMk (P := P) (fst (X.obj (P := P)) (Y.obj (P := P))))
    (X ◁
        IsTerminal.from
          (IsTerminal.ofUniqueHom
            (fun (X : P.FullSubcategory) ↦ ObjectProperty.homMk (P := P) (toUnit (X.obj (P := P)))) ⋯)
          Y ≫
      Iso.hom (ρ_ X))
have h : Eq (α := (tensorObj.{v, u} (𝒞 := ObjectProperty.FullSubcategory.category P) X Y).obj (P := P) ⟶ X.obj (P := P))
  (InducedCategory.Hom.hom (ObjectProperty.homMk (P := P) (fst (X.obj (P := P)) (Y.obj (P := P)))))
  (InducedCategory.Hom.hom
    (X ◁
        IsTerminal.from
          (IsTerminal.ofUniqueHom
            (fun (X : P.FullSubcategory) ↦ ObjectProperty.homMk (P := P) (toUnit (X.obj (P := P)))) sorry)
          Y ≫
      Iso.hom (ρ_ 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
P : ObjectProperty.{v, u} C
inst_3 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_4 : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
⊢ Eq (α := tensorObj.{v, u} (𝒞 := ObjectProperty.FullSubcategory.category P) X Y ⟶ Y)
    (ObjectProperty.homMk (P := P) (snd (X.obj (P := P)) (Y.obj (P := P))))
    (IsTerminal.from
          (IsTerminal.ofUniqueHom
            (fun (X : P.FullSubcategory) ↦ ObjectProperty.homMk (P := P) (toUnit (X.obj (P := P)))) ⋯)
          X ▷
        Y ≫
      Iso.hom (λ_ Y))
have h : Eq (α := (tensorObj.{v, u} (𝒞 := ObjectProperty.FullSubcategory.category P) X Y).obj (P := P) ⟶ Y.obj (P := P))
  (InducedCategory.Hom.hom (ObjectProperty.homMk (P := P) (snd (X.obj (P := P)) (Y.obj (P := P)))))
  (InducedCategory.Hom.hom
    (IsTerminal.from
          (IsTerminal.ofUniqueHom
            (fun (X : P.FullSubcategory) ↦ ObjectProperty.homMk (P := P) (toUnit (X.obj (P := P)))) sorry)
          X ▷
        Y ≫
      Iso.hom (λ_ Y)))
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
inst_4 : F.OplaxMonoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y)
      (fst (F.obj X) (F.obj Y)))
    (F.map (fst X Y))
have trans : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (fst (F.obj X) (F.obj Y)))
  (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))
Tactic: trans F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X Y : C
trans :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y)
      (fst (F.obj X) (F.obj Y)))
    (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y)
      (fst (F.obj X) (F.obj Y)))
    (F.map (fst X Y))
have trans₁ : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X) (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))
  (F.map (fst X Y))
Tactic: trans F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y)
      (fst (F.obj X) (F.obj Y)))
    (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))
have rw : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj X)
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.map (X ◁ toUnit Y))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (δ F X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (fst (F.obj X) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))))
  (F.map (X ◁ toUnit Y) ≫ F.map (Iso.hom (ρ_ X)))
Tactic: rw [← whiskerLeft_fst _ (F.map (toUnit Y)), δ_natural_right_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X Y : C
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj Y)
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y)
      (snd (F.obj X) (F.obj Y)))
    (F.map (snd X Y))
have trans : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj Y)
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj Y)) (δ F X Y) (snd (F.obj X) (F.obj Y)))
  (F.map (toUnit X ▷ Y) ≫ F.map (Iso.hom (λ_ Y)))
Tactic: trans F.map (toUnit X ▷ Y) ≫ F.map (λ_ Y).hom