awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
hf :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑S : Type u))
g : Y ⟶ S
H :
  Subset (α := Set (↑S : Type u))
    (Set.range (ι := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑S : Type u)))
    (Set.range (ι := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑S : Type u)))
x : (↑Y : Type u)
rw :
  Membership.mem (γ := Set (↑Y : Type u))
    {y : (↑Y : Type u) |
      ∃ (x : (↑X : Type u)),
        Eq (α := (↑S : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                (a : (↑X : Type u)) → (↑S : Type u))
              x :
            (↑S : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                (a : (↑Y : Type u)) → (↑S : Type u))
              y :
            (↑S : Type u))}
    x
⊢ Membership.mem (γ := Set (↑Y : Type u))
    (Set.range (ι := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)))
    x

Tactic:
rw [pullback_snd_range]

Premises used: TopCat.pullback_snd_range
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
hf :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑S : Type u))
g : Y ⟶ S
H :
  Subset (α := Set (↑S : Type u))
    (Set.range (ι := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑S : Type u)))
    (Set.range (ι := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑S : Type u)))
x : (↑Y : Type u)
⊢ Membership.mem (γ := Set (↑Y : Type u))
    {y : (↑Y : Type u) |
      ∃ (x : (↑X : Type u)),
        Eq (α := (↑S : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                (a : (↑X : Type u)) → (↑S : Type u))
              x :
            (↑S : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                (a : (↑Y : Type u)) → (↑S : Type u))
              y :
            (↑S : Type u))}
    x

Tactic:
⟨_, (H (Set.mem_range_self x)).choose_spec⟩

Premises used: Set.mem_range_self, Exists.choose_spec, Set.Mem, setOf, Exists.intro
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
hf :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑S : Type u))
g : Y ⟶ S
H :
  Subset (α := Set (↑S : Type u))
    (Set.range (ι := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑S : Type u)))
    (Set.range (ι := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑S : Type u)))
x : (↑Y : Type u)
⊢ Membership.mem (γ := Set (↑Y : Type u))
    {y : (↑Y : Type u) |
      ∃ (x : (↑X : Type u)),
        Eq (α := (↑S : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                (a : (↑X : Type u)) → (↑S : Type u))
              x :
            (↑S : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                (a : (↑Y : Type u)) → (↑S : Type u))
              y :
            (↑S : Type u))}
    x

Tactic:
exact ⟨_, (H (Set.mem_range_self x)).choose_spec⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
hf :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑S : Type u))
g : Y ⟶ S
H :
  Subset (α := Set (↑S : Type u))
    (Set.range (ι := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑S : Type u)))
    (Set.range (ι := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑S : Type u)))
esto : (↑(pullback f g) : Type u) ≃ₜ (↑Y : Type u) :=
  ⋯.toHomeomorph.trans
    {
      toFun :=
        Subtype.val (p := fun (x : (↑Y : Type u)) ↦
          Membership.mem (γ := Set (↑Y : Type u))
            (Set.range (ι := (↑(pullback f g) : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := pullback f g) (pullback.snd f g)) :
                (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)))
            x),
      invFun := fun (x : (↑Y : Type u)) ↦
        Subtype.mk (p := fun (x : (↑Y : Type u)) ↦
          Membership.mem (γ := Set (↑Y : Type u))
            (Set.range (ι := (↑(pullback f g) : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := pullback f g) (pullback.snd f g)) :
                (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)))
            x)
          x ⋯,
      left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsIso (isoOfHomeo esto).hom

Tactic:
(isoOfHomeo esto).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, TopCat.isoOfHomeo
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
hf :
  IsEmbedding (X := (↑X : Type u)) (Y := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑X : Type u)) → (↑S : Type u))
g : Y ⟶ S
H :
  Subset (α := Set (↑S : Type u))
    (Set.range (ι := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑S : Type u)))
    (Set.range (ι := (↑X : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑S : Type u)))
esto : (↑(pullback f g) : Type u) ≃ₜ (↑Y : Type u) :=
  ⋯.toHomeomorph.trans
    {
      toFun :=
        Subtype.val (p := fun (x : (↑Y : Type u)) ↦
          Membership.mem (γ := Set (↑Y : Type u))
            (Set.range (ι := (↑(pullback f g) : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := pullback f g) (pullback.snd f g)) :
                (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)))
            x),
      invFun := fun (x : (↑Y : Type u)) ↦
        Subtype.mk (p := fun (x : (↑Y : Type u)) ↦
          Membership.mem (γ := Set (↑Y : Type u))
            (Set.range (ι := (↑(pullback f g) : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := pullback f g) (pullback.snd f g)) :
                (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)))
            x)
          x ⋯,
      left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsIso (X := pullback f g) (pullback.snd f g)

Tactic:
convert! (isoOfHomeo esto).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, TopCat.isoOfHomeo
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
h :
  ∀ (x : (↑Y : Type u)),
    Membership.mem (γ := Set (↑Y : Type u))
        (Set.image (α := (↑(pullback f g) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f g) (pullback.snd f g)) :
            (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := pullback f g) (pullback.fst f g)) :
              (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
            U))
        x ↔
      Membership.mem (γ := Set (↑Y : Type u))
        (Set.preimage (β := (↑Z : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
            (a : (↑Y : Type u)) → (↑Z : Type u))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
              (a : (↑X : Type u)) → (↑Z : Type u)) ''
            U))
        x
⊢ Eq (α := Set (↑Y : Type u))
    (Set.image (α := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (pullback.fst f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
        U))
    (Set.preimage (β := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Z : Type u)) ''
        U))

Tactic:
ext x
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
y : (↑(pullback f g) : Type u)
hy :
  Membership.mem (γ := Set (↑(pullback f g) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.fst f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
      U)
    y
⊢ Membership.mem (α := (↑Y : Type u)) (γ := Set (↑Y : Type u))
    (Set.preimage (β := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Z : Type u)) ''
        U))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
        y :
      (↑Y : Type u))

Tactic:
⟨(pullback.fst f g) y, hy, CategoryTheory.congr_fun pullback.condition y⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, CategoryTheory.congr_fun, Set.preimage, And.intro, CategoryTheory.Limits.pullback.fst, Exists.intro, Set.image, CategoryTheory.Limits.pullback.condition, DFunLike.coe
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
y : (↑(pullback f g) : Type u)
hy :
  Membership.mem (γ := Set (↑(pullback f g) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.fst f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
      U)
    y
⊢ Membership.mem (α := (↑Y : Type u)) (γ := Set (↑Y : Type u))
    (Set.preimage (β := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Z : Type u)) ''
        U))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
        y :
      (↑Y : Type u))

Tactic:
exact
      ⟨(pullback.fst f g) y, hy, CategoryTheory.congr_fun pullback.condition y⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
x : (↑Y : Type u)
y : (↑X : Type u)
hy : y ∈ U
eq :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
⊢ Membership.mem (γ := Set (↑Y : Type u))
    (Set.image (α := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (pullback.fst f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑X : Type u)) ⁻¹'
        U))
    x

Tactic:
⟨(TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨_, _⟩, eq⟩, ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, Prod.mk, Subtype.mk, TopCat.pullbackIsoProdSubtype, And.intro, Exists.intro, Set.image, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
x : (↑Y : Type u)
y : (↑X : Type u)
hy : y ∈ U
eq :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
⊢ y ∈ U

Tactic:
hy
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
x : (↑Y : Type u)
y : (↑X : Type u)
hy : y ∈ U
eq :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
h h₁ :
  (↑(Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
            Eq (α := (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑X : Type u)) → (↑Z : Type u))
                  p.1 :
                (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑Z : Type u))
                  p.2 :
                (↑Z : Type u)))
            (y, x) eq) :
        (↑X : Type u) × (↑Y : Type u)).1 =
    y
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.fst f g) :
        (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackIsoProdSubtype f g).inv :
            (a :
                { p : (↑X : Type u) × (↑Y : Type u) //
                  (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                    (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) →
              (↑(pullback f g) : Type u))
          (Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
            Eq (α := (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑X : Type u)) → (↑Z : Type u))
                  p.1 :
                (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑Z : Type u))
                  p.2 :
                (↑Z : Type u)))
            (y, x) eq) :
        (↑(pullback f g) : Type u)) =
    y

Tactic:
rw [pullbackIsoProdSubtype_inv_fst_apply]

Premises used: TopCat.pullbackIsoProdSubtype_inv_fst_apply
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑X : Type u)
x : (↑Y : Type u)
y : (↑X : Type u)
hy : y ∈ U
eq :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
h h₁ :
  (↑(Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
            Eq (α := (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑X : Type u)) → (↑Z : Type u))
                  p.1 :
                (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑Z : Type u))
                  p.2 :
                (↑Z : Type u)))
            (y, x) eq) :
        (↑X : Type u) × (↑Y : Type u)).2 =
    x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback f g) (pullback.snd f g) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (pullbackIsoProdSubtype f g).inv :
            (a :
                (↑(of
                      { p : (↑X : Type u) × (↑Y : Type u) //
                        (ConcreteCategory.hom f : (a : (↑X : Type u)) → (↑Z : Type u)) p.1 =
                          (ConcreteCategory.hom g : (a : (↑Y : Type u)) → (↑Z : Type u)) p.2 }) :
                  Type u)) →
              (↑(pullback f g) : Type u))
          (Subtype.mk (p := fun (p : (↑X : Type u) × (↑Y : Type u)) ↦
            Eq (α := (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑X : Type u)) → (↑Z : Type u))
                  p.1 :
                (↑Z : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑Z : Type u))
                  p.2 :
                (↑Z : Type u)))
            (y, x) eq) :
        (↑(pullback f g) : Type u)) =
    x

Tactic:
rw [pullbackIsoProdSubtype_inv_snd_apply]

Premises used: TopCat.pullbackIsoProdSubtype_inv_snd_apply
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑Y : Type u)
h :
  ∀ (x : (↑X : Type u)),
    Membership.mem (γ := Set (↑X : Type u))
        (Set.image (α := (↑(pullback f g) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback f g) (pullback.fst f g)) :
            (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := pullback f g) (pullback.snd f g)) :
              (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)) ⁻¹'
            U))
        x ↔
      Membership.mem (γ := Set (↑X : Type u))
        (Set.preimage (β := (↑Z : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
            (a : (↑X : Type u)) → (↑Z : Type u))
          ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
              (a : (↑Y : Type u)) → (↑Z : Type u)) ''
            U))
        x
⊢ Eq (α := Set (↑X : Type u))
    (Set.image (α := (↑(pullback f g) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (pullback.fst f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f g) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)) ⁻¹'
        U))
    (Set.preimage (β := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Z : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u)) ''
        U))

Tactic:
ext x