awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x : X ⟶ Y
refine_2 :
  ∀ (x_1 : Type u),
    Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      (NatTrans.app
        (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))
        x_1)
      (NatTrans.app
        (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)
        x_1)
⊢ 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)

Tactic:
ext : 2
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x : X ⟶ Y
x_1 : Type u
refine_2 :
  BinaryFan.IsLimit.lift (binaryProductLimit Y x_1) (↾_root_.Prod.fst ≫ x) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.fst =
    ↾_root_.Prod.fst ≫ x
⊢ Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ Y)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (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))
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.fst)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (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)
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.fst)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x : X ⟶ Y
x_1 : Type u
refine_2 :
  BinaryFan.IsLimit.lift (binaryProductLimit Y x_1) (↾_root_.Prod.fst ≫ x) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.snd =
    ↾_root_.Prod.snd
⊢ Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ x_1)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (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))
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.snd)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (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)
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.snd)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x : X ⟶ Y
x_1 : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y x_1) (↾_root_.Prod.fst ≫ x) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.fst =
    ↾_root_.Prod.fst ≫ x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x : X ⟶ Y
x_1 : Type u
⊢ BinaryFan.IsLimit.lift (binaryProductLimit Y x_1) (↾_root_.Prod.fst ≫ x) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.snd =
    ↾_root_.Prod.snd

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
J : Type v
F : J → Type (max v u)
x : Cone (Discrete.functor F)
x_1 :
  x.pt ⟶
    Cone.pt (J := Discrete J) (F := Discrete.functor F)
      { pt := (j : J) → F j,
        π :=
          Discrete.natTrans fun (x : Discrete J) ↦
            match (motive :=
              (x : Discrete J) →
                Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) x ⟶
                  Functor.obj (Discrete.functor F) x)
              x with
            | { as := j } =>
              ↾fun
                  (f :
                    Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) { as := j : Discrete J }) ↦
                f j }
w :
  ∀ (j : Discrete J),
    x_1 ≫
        NatTrans.app
          (Cone.π
            { pt := (j : J) → F j,
              π :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) x ⟶
                        Functor.obj (Discrete.functor F) x)
                    x with
                  | { as := j } =>
                    ↾fun
                        (f :
                          Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j))
                            { as := j : Discrete J }) ↦
                      f j })
          j =
      x.π.app j
h :
  ∀ (x_2 : x.pt) (j : J),
    (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun x_2 j =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (x_3 : x.pt) (j : J) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (x.π.app { as := j : Discrete J }) :
                (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj x.pt).obj { as := j })) →
                  (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := j }))
              x_3))
        x_2 j
⊢ x_1 =
    ↾fun (x_2 : x.pt) (j : J) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (x.π.app { as := j : Discrete J }) :
          (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj x.pt).obj { as := j })) →
            (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := j }))
        x_2

Tactic:
ext x j
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
J : Type v
F : J → Type (max v u)
x_1 : Cone (Discrete.functor F)
x_2 :
  x_1.pt ⟶
    Cone.pt (J := Discrete J) (F := Discrete.functor F)
      { pt := (j : J) → F j,
        π :=
          Discrete.natTrans fun (x : Discrete J) ↦
            match (motive :=
              (x : Discrete J) →
                Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) x ⟶
                  Functor.obj (Discrete.functor F) x)
              x with
            | { as := j } =>
              ↾fun
                  (f :
                    Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) { as := j : Discrete J }) ↦
                f j }
w :
  ∀ (j : Discrete J),
    x_2 ≫
        NatTrans.app
          (Cone.π
            { pt := (j : J) → F j,
              π :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) x ⟶
                        Functor.obj (Discrete.functor F) x)
                    x with
                  | { as := j } =>
                    ↾fun
                        (f :
                          Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j))
                            { as := j : Discrete J }) ↦
                      f j })
          j =
      x_1.π.app j
x : x_1.pt
j : J
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) x_2).toFun x j =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun (x : x_1.pt) (j : J) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.π.app { as := j : Discrete J }) :
              (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj x_1.pt).obj { as := j })) →
                (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := j }))
            x))
      x j

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

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
J : Type v
F : J → Type (max v u)
x_1 : Cone (Discrete.functor F)
x_2 :
  x_1.pt ⟶
    Cone.pt (J := Discrete J) (F := Discrete.functor F)
      { pt := (j : J) → F j,
        π :=
          Discrete.natTrans fun (x : Discrete J) ↦
            match (motive :=
              (x : Discrete J) →
                Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) x ⟶
                  Functor.obj (Discrete.functor F) x)
              x with
            | { as := j } =>
              ↾fun
                  (f :
                    Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) { as := j : Discrete J }) ↦
                f j }
w :
  ∀ (j : Discrete J),
    x_2 ≫
        NatTrans.app
          (Cone.π
            { pt := (j : J) → F j,
              π :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) x ⟶
                        Functor.obj (Discrete.functor F) x)
                    x with
                  | { as := j } =>
                    ↾fun
                        (f :
                          Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j))
                            { as := j : Discrete J }) ↦
                      f j })
          j =
      x_1.π.app j
x : x_1.pt
j : J
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) x_2).toFun x j =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun (x : x_1.pt) (j : J) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (x_1.π.app { as := j : Discrete J }) :
              (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj x_1.pt).obj { as := j })) →
                (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := j }))
            x))
      x j

Tactic:
exact ConcreteCategory.congr_hom (w ⟨j⟩) x

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
J : Type v
F : J → Type (max v u)
j : J
⊢ ((productIso.{v, u} F).hom ≫ ↾fun (f : (j : J) → F j) ↦ f j) = Pi.π F j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
J : Type v
F : J → Type (max v u)
j : J
⊢ (productIso.{v, u} F).inv ≫ Pi.π F j = ↾fun (f : (j : J) → F j) ↦ f j

Tactic:
limit.isoLimitCone_inv_π (productLimitCone.{v, u} F) ⟨j⟩

Premises used: CategoryTheory.Limits.Types.productLimitCone, CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit.isoLimitCone_inv_π
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
J : Type v
F : J → Type u
inst : Small.{u, v} J
j : J
⊢ Eq (α := ∏ᶜ F ⟶ F j)
    (CategoryStruct.comp (Y := Shrink.{u, max u v} ((j : J) → F j))
        (Iso.hom (productIso F) : ∏ᶜ F ⟶ Shrink.{u, max u v} ((j : J) → F j))
        (↾fun (f : Shrink.{u, max u v} ((j : J) → F j)) ↦
            (Equiv.symm (equivShrink ((j : J) → F j)) : (a : Shrink.{u, max u v} ((j : J) → F j)) → (j : J) → F j) f j :
          Shrink.{u, max u v} ((j : J) → F j) ⟶ F j) :
      ∏ᶜ F ⟶ F j)
    (Pi.π F j : ∏ᶜ F ⟶ F j)

Tactic:
limit.isoLimitCone_hom_π (productLimitCone.{v, u} F) ⟨j⟩

Premises used: CategoryTheory.Limits.Types.Small.productLimitCone, CategoryTheory.Limits.limit.isoLimitCone_hom_π, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
J : Type v
F : J → Type u
inst : Small.{u, v} J
j : J
⊢ Eq (α := Shrink.{u, max u v} ((j : J) → F j) ⟶ F j)
    (CategoryStruct.comp (Y := ∏ᶜ F) (Iso.inv (productIso F) : Shrink.{u, max u v} ((j : J) → F j) ⟶ ∏ᶜ F)
        (Pi.π F j : ∏ᶜ F ⟶ F j) :
      Shrink.{u, max u v} ((j : J) → F j) ⟶ F j)
    (↾fun (f : Shrink.{u, max u v} ((j : J) → F j)) ↦
        (Equiv.symm (equivShrink ((j : J) → F j)) : (a : Shrink.{u, max u v} ((j : J) → F j)) → (j : J) → F j) f j :
      Shrink.{u, max u v} ((j : J) → F j) ⟶ F j)

Tactic:
limit.isoLimitCone_inv_π (productLimitCone.{v, u} F) ⟨j⟩

Premises used: CategoryTheory.Limits.Types.Small.productLimitCone, CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit.isoLimitCone_inv_π
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
X' Y' Z' : Type v
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
h :
  ∀ (p : PullbackObj f g),
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1) ≫ f)) p =
      TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2) ≫ g)) p
⊢ Eq (α := PullbackObj f g ⟶ Z) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1) ≫ f)
    ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2) ≫ g)

Tactic:
ext p
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
X' Y' Z' : Type v
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
p : PullbackObj f g
⊢ TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1) ≫ f)) p =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2) ≫ g)) p

Tactic:
p.2

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
X' Y' Z' : Type v
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
p : PullbackObj f g
⊢ TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1) ≫ f)) p =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2) ≫ g)) p

Tactic:
exact p.2

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
X' Y' Z' : Type v
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ (s : PullbackCone f g),
    (fun (s : PullbackCone f g) ↦
            (↾fun (x : s.pt) ↦
                Subtype.mk (p := fun (p : X × Y) ↦
                  Eq (α := (fun (X : Type u) ↦ X) Z)
                    ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
                      (fun (X : Type u) ↦ X) Z)
                    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
                      (fun (X : Type u) ↦ X) Z))
                  ((hom (FC := TypeCat.Fun) s.fst : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) X) x,
                    (hom (FC := TypeCat.Fun) s.snd : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) x)
                  ⋯ :
              s.pt ⟶ (pullbackCone f g).pt))
          s ≫
        (pullbackCone f g).fst =
      s.fst

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
X' Y' Z' : Type v
f_1 : X ⟶ Z
g_1 : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ (s : PullbackCone f g),
    (fun (s : PullbackCone f g) ↦
            (↾fun (x : s.pt) ↦
                Subtype.mk (p := fun (p : X × Y) ↦
                  Eq (α := (fun (X : Type u) ↦ X) Z)
                    ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
                      (fun (X : Type u) ↦ X) Z)
                    ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
                      (fun (X : Type u) ↦ X) Z))
                  ((hom (FC := TypeCat.Fun) s.fst : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) X) x,
                    (hom (FC := TypeCat.Fun) s.snd : (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) Y) x)
                  ⋯ :
              s.pt ⟶ (pullbackCone f g).pt))
          s ≫
        (pullbackCone f g).snd =
      s.snd

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : c.pt
⊢ Eq (α := X) ((↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).1 : X)
    ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X) x :
      (fun (X : Type v) ↦ X) X)

Tactic:
(congr_hom (IsLimit.conePointUniqueUpToIso_hom_comp hc
    (Types.pullbackLimitCone f g).isLimit .left)) x

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.Types.pullbackLimitCone, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.WalkingCospan.left, CategoryTheory.Limits.LimitCone.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : c.pt
⊢ Eq (α := Y) ((↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).2 : Y)
    ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y) x :
      (fun (X : Type v) ↦ X) Y)

Tactic:
(congr_hom (IsLimit.conePointUniqueUpToIso_hom_comp hc
    (Types.pullbackLimitCone f g).isLimit .right)) x

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WalkingCospan.right, CategoryTheory.Limits.Types.pullbackLimitCone, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.LimitCone.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : Types.PullbackObj f g
obtain :
  ∀ (x : c.pt),
    Eq (α := (fun (X : Type v) ↦ X) X)
      ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X)
          (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt)
              ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x : Types.PullbackObj f g) :
            c.pt) :
        (fun (X : Type v) ↦ X) X)
      ((↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).1 : X)
⊢ (hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X)
      (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt) x : c.pt) =
    (↑x : X × Y).1

Tactic:
obtain ⟨x, rfl⟩ := (equivPullbackObj hc).surjective x

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : c.pt
⊢ Eq (α := (fun (X : Type v) ↦ X) X)
    ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X)
        (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt)
            ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x : Types.PullbackObj f g) :
          c.pt) :
      (fun (X : Type v) ↦ X) X)
    ((↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).1 : X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : Types.PullbackObj f g
obtain :
  ∀ (x : c.pt),
    Eq (α := (fun (X : Type v) ↦ X) Y)
      ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y)
          (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt)
              ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x : Types.PullbackObj f g) :
            c.pt) :
        (fun (X : Type v) ↦ X) Y)
      ((↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).2 : Y)
⊢ (hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y)
      (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt) x : c.pt) =
    (↑x : X × Y).2

Tactic:
obtain ⟨x, rfl⟩ := (equivPullbackObj hc).surjective x

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : c.pt
⊢ Eq (α := (fun (X : Type v) ↦ X) Y)
    ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y)
        (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt)
            ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x : Types.PullbackObj f g) :
          c.pt) :
      (fun (X : Type v) ↦ X) Y)
    ((↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).2 : Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ :
  Eq (α := (fun (X : Type v) ↦ X) X)
    ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X) x :
      (fun (X : Type v) ↦ X) X)
    ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X) y :
      (fun (X : Type v) ↦ X) X)
h₂ :
  Eq (α := (fun (X : Type v) ↦ X) Y)
    ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y) x :
      (fun (X : Type v) ↦ X) Y)
    ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y) y :
      (fun (X : Type v) ↦ X) Y)
a :
  Eq.{v + 1} (α := X) (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).1
    (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) y) : X × Y).1
a₁ :
  Eq.{v + 1} (α := Y) (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).2
    (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) y) : X × Y).2
⊢ Eq (α := Types.PullbackObj f g) ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x : Types.PullbackObj f g)
    ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) y : Types.PullbackObj f g)

Tactic:
ext