awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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

Tactic:
assumption
-- 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)
⊢ 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

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
p : pullback f g
⊢ Eq (α := X)
    ((↑((hom (FC := TypeCat.Fun) (pullbackIsoPullback f g).hom :
                (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) (PullbackObj f g))
              p) :
          X × Y).1 :
      X)
    ((hom (FC := TypeCat.Fun) (pullback.fst f g) :
          (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) X)
        p :
      (fun (X : Type u) ↦ X) X)

Tactic:
PullbackCone.IsLimit.equivPullbackObj_apply_fst (pullbackIsPullback f g) p

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_fst, CategoryTheory.Limits.pullbackIsPullback
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
p : pullback f g
⊢ Eq (α := Y)
    ((↑((hom (FC := TypeCat.Fun) (pullbackIsoPullback f g).hom :
                (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) (PullbackObj f g))
              p) :
          X × Y).2 :
      Y)
    ((hom (FC := TypeCat.Fun) (pullback.snd f g) :
          (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) Y)
        p :
      (fun (X : Type u) ↦ X) Y)

Tactic:
PullbackCone.IsLimit.equivPullbackObj_apply_snd (pullbackIsPullback f g) p

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_apply_snd, CategoryTheory.Limits.pullbackIsPullback
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
h :
  ∀ (x : PullbackObj f g),
    (hom (FC := TypeCat.Fun) ((pullbackIsoPullback f g).inv ≫ pullback.fst f g)).toFun x =
      TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1)) x
⊢ (pullbackIsoPullback f g).inv ≫ pullback.fst f g = ↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1

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

Tactic:
PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst (pullbackIsPullback f g) _

Premises used: CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
x : PullbackObj f g
⊢ (hom (FC := TypeCat.Fun) ((pullbackIsoPullback f g).inv ≫ pullback.fst f g)).toFun x =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1)) x

Tactic:
exact PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst (pullbackIsPullback f g) _

Premises used: CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
h :
  ∀ (x : PullbackObj f g),
    (hom (FC := TypeCat.Fun) ((pullbackIsoPullback f g).inv ≫ pullback.snd f g)).toFun x =
      TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2)) x
⊢ (pullbackIsoPullback f g).inv ≫ pullback.snd f g = ↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2

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

Tactic:
PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd (pullbackIsPullback f g) _

Premises used: CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
x : PullbackObj f g
⊢ (hom (FC := TypeCat.Fun) ((pullbackIsoPullback f g).inv ≫ pullback.snd f g)).toFun x =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2)) x

Tactic:
exact PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd (pullbackIsPullback f g) _

Premises used: CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
h₁ :
  ∀ (p : (fun (X : Type u) ↦ X) P),
    Eq (α := (fun (X : Type u) ↦ X) X)
      ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
        (fun (X : Type u) ↦ X) X)
      (Function.comp (β := X × Y) _root_.Prod.fst
          (Function.comp (β :=
            { 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) })
            (Subtype.val (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) e.hom) :
              (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g)))
          p :
        X)
⊢ Eq (α := (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
      (Function.comp (β :=
        { 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) })
        (Subtype.val (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) e.hom) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g))))

Tactic:
ext p
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun (X : Type u) ↦ X) P
this :
  Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) (pullback.fst f g) :
          (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) X)
        ((hom (FC := TypeCat.Fun) (Iso.hom h.isoPullback) :
              (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (pullback f g))
            p :
          (fun (X : Type u) ↦ X) (pullback f g)) :
      (fun (X : Type u) ↦ X) X)
⊢ Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
        (Function.comp (β :=
          { 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) })
          (Subtype.val (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) e.hom) :
            (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g)))
        p :
      X)

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun (X : Type u) ↦ X) P
h₁ :
  Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) (pullback.fst f g) :
          (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) X)
        ((hom (FC := TypeCat.Fun) (Iso.hom h.isoPullback) :
              (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (pullback f g))
            p :
          (fun (X : Type u) ↦ X) (pullback f g)) :
      (fun (X : Type u) ↦ X) X)
⊢ Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
        (Function.comp (β :=
          { 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) })
          (Subtype.val (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) e.hom) :
            (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g)))
        p :
      X)

Tactic:
suffices fst p = pullback.fst f g (h.isoPullback.hom p) by simpa
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun (X : Type u) ↦ X) P
h₁ :
  Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g)) :
          (a : P) → X)
        p :
      X)
h₂ h₃ :
  Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : P) → X) p : X)
⊢ Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) (pullback.fst f g) :
          (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) X)
        ((hom (FC := TypeCat.Fun) (Iso.hom h.isoPullback) :
              (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (pullback f g))
            p :
          (fun (X : Type u) ↦ X) (pullback f g)) :
      (fun (X : Type u) ↦ X) X)

Tactic:
rw [← comp_apply h.isoPullback.hom (pullback.fst f g), IsPullback.isoPullback_hom_fst]

Premises used: CategoryTheory.IsPullback.isoPullback, CategoryTheory.IsPullback.isoPullback_hom_fst, CategoryTheory.comp_apply, CategoryTheory.Limits.pullback.fst, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
⊢ Eq (α := (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
      (Function.comp (β :=
        { 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) })
        (Subtype.val (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) e.hom) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g))))

Tactic:
have : fst = _root_.Prod.fst ∘ Subtype.val ∘ e.hom := by
    ext p
    suffices fst p = pullback.fst f g (h.isoPullback.hom p) by simpa
    rw [← comp_apply h.isoPullback.hom (pullback.fst f g), IsPullback.isoPullback_hom_fst]
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this :
  Eq (α := (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
      (Function.comp (β :=
        { 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) })
        (Subtype.val (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) e.hom) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g))))
x : (fun (X : Type u) ↦ X) X
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.image (α := X × Y) _root_.Prod.fst
        (Set.image (α :=
          { 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) })
          (Subtype.val (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)))
          Set.univ))
      x ↔
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X))
      (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)
        (Set.range (ι := (fun (X : Type u) ↦ X) Y)
          (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))
      x

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
rw rw₁ :
  Eq (α := Set ((fun (X : Type u) ↦ X) Y))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))
⊢ Eq (α := Set ((fun (X : Type u) ↦ X) Y))
    (Set.range (ι := (fun (X : Type u) ↦ X) P)
      (⇑(hom (FC := TypeCat.Fun) snd) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) Y))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))

Tactic:
rw [range_fst_of_isPullback (IsPullback.flip h)]

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.Limits.Types.range_fst_of_isPullback
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := Set ((fun (X : Type u) ↦ X) X))
    (Set.range (ι := (fun (X : Type u) ↦ X) (pullback f g))
      (⇑(hom (FC := TypeCat.Fun) (pullback.fst f g)) :
        (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) X))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))

Tactic:
range_fst_of_isPullback (.of_hasPullback f g)

Premises used: CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.Limits.Types.range_fst_of_isPullback
-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := Set ((fun (X : Type u) ↦ X) Y))
    (Set.range (ι := (fun (X : Type u) ↦ X) (pullback f g))
      (⇑(hom (FC := TypeCat.Fun) (pullback.snd f g)) :
        (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) Y))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) X)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))

Tactic:
range_snd_of_isPullback (.of_hasPullback f g)

Premises used: CategoryTheory.Limits.Types.range_snd_of_isPullback, CategoryTheory.IsPullback.of_hasPullback