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 : 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)
apply : IsLimit (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd A B)))
⊢ PreservesLimit (pair A B) F

Tactic:
apply preservesLimit_of_preserves_limit_cone (tensorProductIsBinaryProduct A B)

Premises used: CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
inst_4 :
  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)
⊢ ((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 ≅
    Cone.pt.{0, v₁, 0, u₁} (F := pair (F.obj A) (F.obj B))
      (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:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
inst_4 :
  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))
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))
⊢ IsLimit (F.mapCone (BinaryFan.mk (P := tensorObj.{v, u} (𝒞 := inst) A B) (fst A B) (snd 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)))

Premises used: CategoryTheory.Limits.pairComp, CategoryTheory.Limits.Cone.extend, CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Limits.IsLimit.extendIso, CategoryTheory.CartesianMonoidalCategory.tensorProductIsBinaryProduct, CategoryTheory.CartesianMonoidalCategory.prodComparison, CategoryTheory.Functor.obj, Equiv.invFun, CategoryTheory.SemiCartesianMonoidalCategory.fst, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso, CategoryTheory.Limits.BinaryFan.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
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 :
  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 })
⊢ 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:
dsimp only [BinaryFan.fst]

Premises used: CategoryTheory.Limits.BinaryFan.fst
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
inst_4 :
  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 (α :=
    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:
simp [pairComp]

Premises used: CategoryTheory.Limits.pairComp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
inst_4 :
  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_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 })
⊢ 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:
dsimp only [BinaryFan.snd]

Premises used: CategoryTheory.Limits.BinaryFan.snd
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : CartesianMonoidalCategory.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
A B : C
inst_4 :
  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 (α :=
    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:
simp [pairComp]

Premises used: CategoryTheory.Limits.pairComp
-- 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
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)
preservesLimit :
  autoParam (∀ {K : Functor.{0, v, 0, u} (Discrete WalkingPair) C}, PreservesLimit K F)
    PreservesLimitsOfShape.preservesLimit._autoParam
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F

Tactic:
constructor
-- 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
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

Tactic:
@preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoPair K).symm ?_

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoPair
-- 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
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 :
  PreservesLimit
    (pair (K.obj { as := WalkingPair.left : Discrete WalkingPair })
      (K.obj { as := WalkingPair.right : Discrete WalkingPair }))
    F
⊢ PreservesLimit K F

Tactic:
refine @preservesLimit_of_iso_diagram _ _ _ _ _ _ _ _ _ (diagramIsoPair K).symm ?_

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, CategoryTheory.Iso.symm, CategoryTheory.Limits.diagramIsoPair
-- 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
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
    (pair (K.obj { as := WalkingPair.left : Discrete WalkingPair })
      (K.obj { as := WalkingPair.right : Discrete WalkingPair }))
    F

Tactic:
apply preservesLimit_pair_of_isIso_prodComparison

Premises used: CategoryTheory.CartesianMonoidalCategory.preservesLimit_pair_of_isIso_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
P : ObjectProperty.{v, u} C
inst_3 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_4 : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
⊢ ∀ (j : Discrete PEmpty.{1}), P (Functor.obj.{0, v, 0, u} (Functor.empty C) j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_3 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_4 : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : C
hX : P X
hY : P Y
⊢ P (Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
inst_3 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_4 : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : C
hX : P X
hY : P Y
⊢ P (Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
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)
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)
⊢ 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

Tactic:
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
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.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:
apply toUnit_unique

Premises used: CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique
-- 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
P : ObjectProperty.{v, u} C
inst_3 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_4 : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
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)))) ⋯)
            Y ≫
        Iso.hom (ρ_ X)))
⊢ 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))

Tactic:
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
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).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)))) ⋯)
            Y ≫
        Iso.hom (ρ_ X)))

Tactic:
fst_def X.1 Y.1

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.SemiCartesianMonoidalCategory.fst_def, CategoryTheory.SemiCartesianMonoidalCategory.toUnit
-- 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
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).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)))) ⋯)
            Y ≫
        Iso.hom (ρ_ X)))

Tactic:
exact fst_def X.1 Y.1

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.SemiCartesianMonoidalCategory.fst_def
-- 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
P : ObjectProperty.{v, u} C
inst_3 : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst_4 : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
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)))) ⋯)
            X ▷
          Y ≫
        Iso.hom (λ_ Y)))
⊢ 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))

Tactic:
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
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).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)))) ⋯)
            X ▷
          Y ≫
        Iso.hom (λ_ Y)))

Tactic:
snd_def X.1 Y.1

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, CategoryTheory.SemiCartesianMonoidalCategory.snd_def