awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
a : (↑S.pt : Type u)
⊢ Eq (α := (↑X : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (ofHom
                {
                  toFun := fun (x : (↑S.1 : 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)))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) S.fst :
                            (a : (↑S.pt : Type u)) → (↑X : Type u))
                          x,
                        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) S.snd :
                            (a : (↑S.pt : Type u)) → (↑Y : Type u))
                          x)
                      ⋯,
                  continuous_toFun := ⋯ :
                  C((↑S.1 : Type u),
                    { 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)) }) } ≫
              (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) ⋯).fst) :
          (a : (↑S.pt : Type u)) → (↑X : Type u))
        a :
      (↑X : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) S.fst :
          (a : (↑S.pt : Type u)) → (↑X : Type u))
        a :
      (↑X : Type u))

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
a : (↑S.pt : Type u)
⊢ Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (ofHom
                {
                  toFun := fun (x : (↑S.1 : 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)))
                      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) S.fst :
                            (a : (↑S.pt : Type u)) → (↑X : Type u))
                          x,
                        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) S.snd :
                            (a : (↑S.pt : Type u)) → (↑Y : Type u))
                          x)
                      ⋯,
                  continuous_toFun := ⋯ :
                  C((↑S.1 : Type u),
                    { 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)) }) } ≫
              (PullbackCone.mk (pullbackFst f g) (pullbackSnd f g) ⋯).snd) :
          (a : (↑S.pt : Type u)) → (↑Y : Type u))
        a :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) S.snd :
          (a : (↑S.pt : Type u)) → (↑Y : Type u))
        a :
      (↑Y : Type u))

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : (↑S.pt : Type u)
⊢ Eq.{u + 1} (α := (↑X : Type u))
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
              (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
            x) :
        (↑X : Type u) × (↑Y : Type u)).1
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (ofHom
                  {
                    toFun := fun (x : (↑S.1 : 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)))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) S.fst :
                              (a : (↑S.pt : Type u)) → (↑X : Type u))
                            x,
                          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) S.snd :
                              (a : (↑S.pt : Type u)) → (↑Y : Type u))
                            x)
                        ⋯,
                    continuous_toFun := ⋯ :
                    C((↑S.1 : Type u),
                      { 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)) }) }) :
              (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
            x) :
        (↑X : Type u) × (↑Y : Type u)).1

Tactic:
simpa using ConcreteCategory.congr_hom h₁ x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : (↑S.pt : Type u)
⊢ Eq.{u + 1} (α := (↑Y : Type u))
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
              (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
            x) :
        (↑X : Type u) × (↑Y : Type u)).2
    (↑((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (ofHom
                  {
                    toFun := fun (x : (↑S.1 : 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)))
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) S.fst :
                              (a : (↑S.pt : Type u)) → (↑X : Type u))
                            x,
                          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) S.snd :
                              (a : (↑S.pt : Type u)) → (↑Y : Type u))
                            x)
                        ⋯,
                    continuous_toFun := ⋯ :
                    C((↑S.1 : Type u),
                      { 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)) }) }) :
              (a : (↑S.pt : Type u)) → (↑(pullbackCone f g).pt : Type u))
            x) :
        (↑X : Type u) × (↑Y : Type u)).2

Tactic:
simpa using ConcreteCategory.congr_hom h₂ x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).inv ≫ pullback.fst f g = pullbackFst f g

Tactic:
simp [pullbackCone, pullbackIsoProdSubtype]

Premises used: TopCat.pullbackCone, TopCat.pullbackIsoProdSubtype
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x :
  { 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)) }
⊢ (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 :
                (↑(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))
          x :
        (↑(pullback f g) : Type u)) =
    (↑x : (↑X : Type u) × (↑Y : Type u)).1

Tactic:
ConcreteCategory.congr_hom (pullbackIsoProdSubtype_inv_fst f g) x

Premises used: TopCat.pullbackIsoProdSubtype_inv_fst, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).inv ≫ pullback.snd f g = pullbackSnd f g

Tactic:
simp [pullbackCone, pullbackIsoProdSubtype]

Premises used: TopCat.pullbackCone, TopCat.pullbackIsoProdSubtype
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x :
  { 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)) }
⊢ (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))
          x :
        (↑(pullback f g) : Type u)) =
    (↑x : (↑X : Type u) × (↑Y : Type u)).2

Tactic:
ConcreteCategory.congr_hom (pullbackIsoProdSubtype_inv_snd f g) x

Premises used: TopCat.pullbackIsoProdSubtype_inv_snd, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
rw : pullbackFst f g = (pullbackIsoProdSubtype f g).inv ≫ pullback.fst f g
rw₁ rw₂ : pullbackFst f g = pullbackFst f g
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst f g

Tactic:
rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_fst]

Premises used: TopCat.pullbackIsoProdSubtype_inv_fst, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
rw : pullbackSnd f g = (pullbackIsoProdSubtype f g).inv ≫ pullback.snd f g
rw₁ rw₂ : pullbackSnd f g = pullbackSnd f g
⊢ (pullbackIsoProdSubtype f g).hom ≫ pullbackSnd f g = pullback.snd f g

Tactic:
rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_snd]

Premises used: TopCat.pullbackIsoProdSubtype_inv_snd, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
J : Type v
inst : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
x : (↑(pullback f g) : 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))
        (((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))
                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))
                x).1 :
          (↑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))
        (((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))
                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))
                x).2 :
          (↑Y : Type u)) :
      (↑Z : Type u))

Tactic:
simpa using CategoryTheory.congr_fun pullback.condition x

Premises used: CategoryTheory.congr_fun, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
homeo : (↑(pullback f g) : Type u) ≃ₜ
  (↑(of
        { 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)) }) :
    Type u) :=
  homeoOfIso (pullbackIsoProdSubtype f g)
⊢ Eq (α := TopologicalSpace (↑(pullback f g) : Type u)) (pullback f g).str
    (induced
        (⇑(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))
        X.str ⊓
      induced
        (⇑(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.str)

Tactic:
homeo.isInducing.eq_induced.trans ?_

Premises used: Homeomorph.isInducing, Topology.IsInducing.eq_induced, Eq.trans
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
h :
  ∀ (x : (↑(X ⨯ Y) : Type u)),
    Membership.mem (γ := Set (↑(X ⨯ 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) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
            (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u)))
        x ↔
      Membership.mem (γ := Set (↑(X ⨯ Y) : Type u))
        {x : (↑(X ⨯ Y) : Type u) |
          Eq (α := (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := X ⨯ Y) (prod.fst ≫ f) :
                  (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
                x :
              (↑Z : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := X ⨯ Y) (prod.snd ≫ g) :
                  (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
                x :
              (↑Z : Type u))}
        x
⊢ Eq (α := Set (↑(X ⨯ 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) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g))) :
        (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u)))
    {x : (↑(X ⨯ Y) : Type u) |
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                X ⨯ Y) (prod.fst ≫ f) :
              (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
            x :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                X ⨯ Y) (prod.snd ≫ g) :
              (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
            x :
          (↑Z : Type u))}

Tactic:
ext x
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
y : (↑(pullback f g) : Type u)
h :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g)
            (CategoryStruct.comp (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) (prod.fst ≫ f)) :
          (a : (↑(pullback f g) : 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) (X :=
            pullback f g)
            (CategoryStruct.comp (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) (prod.snd ≫ g)) :
          (a : (↑(pullback f g) : Type u)) → (↑Z : Type u))
        y :
      (↑Z : Type u))
⊢ Membership.mem (α := (↑(X ⨯ Y) : Type u)) (γ := Set (↑(X ⨯ Y) : Type u))
    {x : (↑(X ⨯ Y) : Type u) |
      Eq (α := (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                X ⨯ Y) (prod.fst ≫ f) :
              (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
            x :
          (↑Z : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                X ⨯ Y) (prod.snd ≫ g) :
              (a : (↑(X ⨯ Y) : Type u)) → (↑Z : Type u))
            x :
          (↑Z : Type u))}
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f g) (Y := X ⨯ Y) (prod.lift (pullback.fst f g) (pullback.snd f g)) :
          (a : (↑(pullback f g) : Type u)) → (↑(X ⨯ Y) : Type u))
        y :
      (↑(X ⨯ Y) : Type u))

Tactic:
simp only [← ConcreteCategory.comp_apply, Set.mem_setOf_eq]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, Set.mem_setOf_eq