awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
β : Type v
inst : Small.{u, v} β
f : β → Type u
P : Type u
s : (b : β) → P ⟶ f b
b : β
x : P
⊢ Eq (α := (fun (X : Type u) ↦ X) (f b))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π f b) :
          (a : (fun (X : Type u) ↦ X) (∏ᶜ f)) → (fun (X : Type u) ↦ X) (f b))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.lift (f := f) s) :
              (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (∏ᶜ f))
            x :
          (fun (X : Type u) ↦ X) (∏ᶜ f)) :
      (fun (X : Type u) ↦ X) (f b))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s b) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (f b))
        x :
      (fun (X : Type u) ↦ X) (f b))

Tactic:
ConcreteCategory.congr_hom (limit.lift_π (Fan.mk P s) ⟨b⟩) x

Premises used: CategoryTheory.Limits.Fan.mk, CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
β : Type v
f : β → Type v
P : Type v
s : (b : β) → P ⟶ f b
b : β
x : P
⊢ Eq (α := (fun (X : Type v) ↦ X) (f b))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π f b) :
          (a : (fun (X : Type v) ↦ X) (∏ᶜ f)) → (fun (X : Type v) ↦ X) (f b))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.lift (f := f) s) :
            (a : (fun (X : Type v) ↦ X) P) → (fun (X : Type v) ↦ X) (∏ᶜ f))
          x) :
      (fun (X : Type v) ↦ X) (f b))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (s b) : (a : (fun (X : Type v) ↦ X) P) → (fun (X : Type v) ↦ X) (f b))
        x :
      (fun (X : Type v) ↦ X) (f b))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
β : Type v
inst : Small.{u, v} β
f g : β → Type u
α : (j : β) → f j ⟶ g j
b : β
x : (fun (X : Type u) ↦ X) (∏ᶜ f)
⊢ Eq (α := (fun (X : Type u) ↦ X) (g b))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π g b) :
          (a : (fun (X : Type u) ↦ X) (∏ᶜ g)) → (fun (X : Type u) ↦ X) (g b))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.map (f := f) (g := g) α) :
              (a : (fun (X : Type u) ↦ X) (∏ᶜ f)) → (fun (X : Type u) ↦ X) (∏ᶜ g))
            x :
          (fun (X : Type u) ↦ X) (∏ᶜ g)) :
      (fun (X : Type u) ↦ X) (g b))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α b) :
          (a : (fun (X : Type u) ↦ X) (f b)) → (fun (X : Type u) ↦ X) (g b))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π f b) :
              (a : (fun (X : Type u) ↦ X) (∏ᶜ f)) → (fun (X : Type u) ↦ X) (f b))
            x :
          (fun (X : Type u) ↦ X) (f b)) :
      (fun (X : Type u) ↦ X) (g b))

Tactic:
limMap_π_apply _ _ _

Premises used: CategoryTheory.Limits.limMap_π_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
β : Type v
f g : β → Type v
α : (j : β) → f j ⟶ g j
b : β
x : (fun (X : Type v) ↦ X) (∏ᶜ f)
⊢ Eq (α := (fun (X : Type v) ↦ X) (g b))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π g b) :
          (a : (fun (X : Type v) ↦ X) (∏ᶜ g)) → (fun (X : Type v) ↦ X) (g b))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.map (f := f) (g := g) α) :
            (a : (fun (X : Type v) ↦ X) (∏ᶜ f)) → (fun (X : Type v) ↦ X) (∏ᶜ g))
          x) :
      (fun (X : Type v) ↦ X) (g b))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α b) :
          (a : (fun (X : Type v) ↦ X) (f b)) → (fun (X : Type v) ↦ X) (g b))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pi.π f b) :
            (a : (fun (X : Type v) ↦ X) (∏ᶜ f)) → (fun (X : Type v) ↦ X) (f b))
          x) :
      (fun (X : Type v) ↦ X) (g b))

Tactic:
simp [pi_map_π_apply]

Premises used: CategoryTheory.Limits.Types.pi_map_π_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X : Type u
x : X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (isTerminalPUnit.from X) :
        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) PUnit.{u + 1})
      x =
    PUnit.unit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X : Type u
⊢ IsTerminal X ≃ (X ≅ PUnit.{u + 1})

Tactic:
calc
    IsTerminal X ≃ Unique X := isTerminalEquivUnique _
    _ ≃ (X ≃ PUnit) := uniqueEquivEquivUnique _ _
    _ ≃ (X ≅ PUnit) := equivEquivIso

Premises used: CategoryTheory.Limits.Types.isTerminalEquivUnique, CategoryTheory.Limits.IsTerminal, Unique, Equiv, CategoryTheory.Iso, PUnit, uniqueEquivEquivUnique, equivEquivIso
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
⊢ (binaryProductCone X Y).fst = ↾_root_.Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
⊢ (binaryProductCone X Y).snd = ↾_root_.Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x : Cone (pair X Y)
x_1 : x.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x_1 ≫ (binaryProductCone X Y).π.app j = x.π.app j
h :
  ∀ (x_2 : x.pt),
    (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun x_2 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x_3 : x.pt) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.fst x) :
                  (a : (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                x_3,
              (ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.snd x) :
                  (a : (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                x_3)))
        x_2
⊢ x_1 =
    ↾fun (x_2 : x.pt) ↦
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.fst x) :
            (a : (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left })) →
              (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
          x_2,
        (ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.snd x) :
            (a : (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right })) →
              (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
          x_2)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x_1 : Cone (pair X Y)
x_2 : x_1.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x_2 ≫ (binaryProductCone X Y).π.app j = x_1.π.app j
x : x_1.pt
h :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) x_2).toFun x).1 =
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : x_1.pt) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.fst x_1) :
                  (a :
                      (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := left })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                x,
              (ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.snd x_1) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := right })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                x)))
        x).1
h₁ :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) x_2).toFun x).2 =
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : x_1.pt) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.fst x_1) :
                  (a :
                      (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := left })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                x,
              (ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.snd x_1) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := right })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                x)))
        x).2
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) x_2).toFun x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun (x : x_1.pt) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.fst x_1) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := left })) →
                  (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
              x,
            (ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.snd x_1) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := right })) →
                  (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
              x)))
      x

Tactic:
apply Prod.ext

Premises used: Prod.ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x_1 : Cone (pair X Y)
x_2 : x_1.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x_2 ≫ (binaryProductCone X Y).π.app j = x_1.π.app j
x : x_1.pt
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) x_2).toFun x).1 =
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : x_1.pt) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.fst x_1) :
                  (a :
                      (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := left })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                x,
              (ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.snd x_1) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := right })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                x)))
        x).1

Tactic:
ConcreteCategory.congr_hom (w ⟨left⟩) x

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x_1 : Cone (pair X Y)
x_2 : x_1.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x_2 ≫ (binaryProductCone X Y).π.app j = x_1.π.app j
x : x_1.pt
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) x_2).toFun x).2 =
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : x_1.pt) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.fst x_1) :
                  (a :
                      (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := left })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                x,
              (ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.snd x_1) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := right })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                x)))
        x).2

Tactic:
ConcreteCategory.congr_hom (w ⟨right⟩) x

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x_1 : Cone (pair X Y)
x_2 : x_1.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x_2 ≫ (binaryProductCone X Y).π.app j = x_1.π.app j
x : x_1.pt
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) x_2).toFun x).1 =
    (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x : x_1.pt) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.fst x_1) :
                  (a :
                      (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := left })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left }))
                x,
              (ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryFan.snd x_1) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        (((Functor.const (Discrete WalkingPair)).obj x_1.pt).obj { as := right })) →
                    (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right }))
                x)))
        x).1

Tactic:
exacts [ConcreteCategory.congr_hom (w ⟨left⟩) x, ConcreteCategory.congr_hom (w ⟨right⟩) x]

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
⊢ (binaryProductIso X Y).hom ≫ ↾_root_.Prod.fst = prod.fst

Tactic:
limit.isoLimitCone_hom_π (binaryProductLimitCone X Y) ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.limit.isoLimitCone_hom_π, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Types.binaryProductLimitCone, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
⊢ (binaryProductIso X Y).hom ≫ ↾_root_.Prod.snd = prod.snd

Tactic:
limit.isoLimitCone_hom_π (binaryProductLimitCone X Y) ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.limit.isoLimitCone_hom_π, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Types.binaryProductLimitCone
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
⊢ (binaryProductIso X Y).inv ≫ prod.fst = ↾_root_.Prod.fst

Tactic:
limit.isoLimitCone_inv_π (binaryProductLimitCone X Y) ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit.isoLimitCone_inv_π, CategoryTheory.Limits.Types.binaryProductLimitCone, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
⊢ (binaryProductIso X Y).inv ≫ prod.snd = ↾_root_.Prod.snd

Tactic:
limit.isoLimitCone_inv_π (binaryProductLimitCone X Y) ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit.isoLimitCone_inv_π, CategoryTheory.Limits.Types.binaryProductLimitCone
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
refine_1 : (X : Type u) → binaryProductFunctor.obj X ≅ Functor.obj prod.functor X
refine_2 :
  ∀ {X Y : Type u} (x : X ⟶ Y),
    Eq (α := binaryProductFunctor.obj X ⟶ Functor.obj prod.functor Y)
      (binaryProductFunctor.map x ≫
        Iso.hom
          ((fun (X : Type u) ↦
              (NatIso.ofComponents
                  (fun (Y : Type u) ↦
                    Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                  ⋯ :
                binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
            Y))
      (Iso.hom
          ((fun (X : Type u) ↦
              (NatIso.ofComponents
                  (fun (Y : Type u) ↦
                    Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                  ⋯ :
                binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
            X) ≫
        Functor.map prod.functor x)
⊢ binaryProductFunctor ≅ prod.functor

Tactic:
refine NatIso.ofComponents (fun X => ?_) (fun _ => ?_)

Premises used: CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X : Type u
refine_1 : (Y : Type u) → (binaryProductFunctor.obj X).obj Y ≅ Functor.obj (Functor.obj prod.functor X) Y
refine_1₁ :
  ∀ {X_1 Y : Type u} (x : X_1 ⟶ Y),
    Eq (α := (binaryProductFunctor.obj X).obj X_1 ⟶ Functor.obj (Functor.obj prod.functor X) Y)
      ((binaryProductFunctor.obj X).map x ≫
        Iso.hom
          ((fun (Y : Type u) ↦
              (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
            Y))
      (Iso.hom
          ((fun (Y : Type u) ↦
              (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
            X_1) ≫
        Functor.map (Functor.obj prod.functor X) x)
⊢ binaryProductFunctor.obj X ≅ Functor.obj prod.functor X

Tactic:
refine NatIso.ofComponents (fun Y => ?_) (fun _ => ?_)

Premises used: CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
⊢ (binaryProductFunctor.obj X).obj Y ≅ Functor.obj (Functor.obj prod.functor X) Y

Tactic:
exact ((limit.isLimit _).conePointUniqueUpToIso (binaryProductLimit X Y)).symm

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.Types.binaryProductLimit, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X X_1 Y : Type u
x : X_1 ⟶ Y
refine_1 :
  Eq (α := (binaryProductFunctor.obj X).obj X_1 ⟶ X)
    (CategoryStruct.comp (Y := X ⨯ Y)
      ((binaryProductFunctor.obj X).map x ≫
        Iso.hom
          ((fun (Y : Type u) ↦
              (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
            Y))
      prod.fst)
    (CategoryStruct.comp (Y := X ⨯ Y)
      (Iso.hom
            ((fun (Y : Type u) ↦
                (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                  (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
              X_1) ≫
          Functor.map (Functor.obj prod.functor X) x :
        (binaryProductFunctor.obj X).obj X_1 ⟶ Functor.obj (Functor.obj prod.functor X) Y)
      prod.fst)
refine_1₁ :
  Eq (α := (binaryProductFunctor.obj X).obj X_1 ⟶ Y)
    (CategoryStruct.comp (Y := X ⨯ Y)
      ((binaryProductFunctor.obj X).map x ≫
        Iso.hom
          ((fun (Y : Type u) ↦
              (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
            Y))
      prod.snd)
    (CategoryStruct.comp (Y := X ⨯ Y)
      (Iso.hom
            ((fun (Y : Type u) ↦
                (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                  (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
              X_1) ≫
          Functor.map (Functor.obj prod.functor X) x :
        (binaryProductFunctor.obj X).obj X_1 ⟶ Functor.obj (Functor.obj prod.functor X) Y)
      prod.snd)
⊢ Eq (α := (binaryProductFunctor.obj X).obj X_1 ⟶ Functor.obj (Functor.obj prod.functor X) Y)
    ((binaryProductFunctor.obj X).map x ≫
      Iso.hom
        ((fun (Y : Type u) ↦
            (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
              (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
          Y))
    (Iso.hom
        ((fun (Y : Type u) ↦
            (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
              (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
          X_1) ≫
      Functor.map (Functor.obj prod.functor X) x)

Tactic:
apply Limits.prod.hom_ext

Premises used: CategoryTheory.Limits.prod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X X_1 Y : Type u
x : X_1 ⟶ Y
refine_1 :
  Eq.{u + 1} (α := X × X_1 ⟶ X)
    (CategoryStruct.comp (Y := X × Y)
      (↾fun (x_1 : X × X_1) ↦ (x_1.1, (ConcreteCategory.hom (FC := TypeCat.Fun) x : (a : X_1) → Y) x_1.2))
      (↾_root_.Prod.fst))
    (↾_root_.Prod.fst)
⊢ Eq (α := (binaryProductFunctor.obj X).obj X_1 ⟶ X)
    (CategoryStruct.comp (Y := X ⨯ Y)
      ((binaryProductFunctor.obj X).map x ≫
        Iso.hom
          ((fun (Y : Type u) ↦
              (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
            Y))
      prod.fst)
    (CategoryStruct.comp (Y := X ⨯ Y)
      (Iso.hom
            ((fun (Y : Type u) ↦
                (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                  (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
              X_1) ≫
          Functor.map (Functor.obj prod.functor X) x :
        (binaryProductFunctor.obj X).obj X_1 ⟶ Functor.obj (Functor.obj prod.functor X) Y)
      prod.fst)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X X_1 Y : Type u
x : X_1 ⟶ Y
refine_1 :
  Eq (α := X × X_1 ⟶ Y)
    (CategoryStruct.comp (Y := X × Y)
      (↾fun (x_1 : X × X_1) ↦ (x_1.1, (ConcreteCategory.hom (FC := TypeCat.Fun) x : (a : X_1) → Y) x_1.2))
      (↾_root_.Prod.snd))
    (↾_root_.Prod.snd ≫ x)
⊢ Eq (α := (binaryProductFunctor.obj X).obj X_1 ⟶ Y)
    (CategoryStruct.comp (Y := X ⨯ Y)
      ((binaryProductFunctor.obj X).map x ≫
        Iso.hom
          ((fun (Y : Type u) ↦
              (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
            Y))
      prod.snd)
    (CategoryStruct.comp (Y := X ⨯ Y)
      (Iso.hom
            ((fun (Y : Type u) ↦
                (Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)) :
                  (binaryProductCone X Y).pt ≅ Cone.pt (F := pair X Y) (limit.cone (pair X Y))))
              X_1) ≫
          Functor.map (Functor.obj prod.functor X) x :
        (binaryProductFunctor.obj X).obj X_1 ⟶ Functor.obj (Functor.obj prod.functor X) Y)
      prod.snd)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X X_1 Y : Type u
x : X_1 ⟶ Y
⊢ Eq.{u + 1} (α := X × X_1 ⟶ X)
    (CategoryStruct.comp (Y := X × Y)
      (↾fun (x_1 : X × X_1) ↦ (x_1.1, (ConcreteCategory.hom (FC := TypeCat.Fun) x : (a : X_1) → Y) x_1.2))
      (↾_root_.Prod.fst))
    (↾_root_.Prod.fst)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X X_1 Y : Type u
x : X_1 ⟶ Y
⊢ Eq (α := X × X_1 ⟶ Y)
    (CategoryStruct.comp (Y := X × Y)
      (↾fun (x_1 : X × X_1) ↦ (x_1.1, (ConcreteCategory.hom (FC := TypeCat.Fun) x : (a : X_1) → Y) x_1.2))
      (↾_root_.Prod.snd))
    (↾_root_.Prod.snd ≫ x)

Tactic:
rfl