awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  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))
H₂ :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
e_2 : (↑((cospan f g).obj WalkingCospan.one) : Type u) = (↑S : Type u)
⊢ Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : 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 ≫ g)) :
      (a : (↑(pullback f g) : Type u)) → (↑S : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
H :
  IsOpenEmbedding (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
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
H :
  IsOpenEmbedding (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 :
  Eq (α := (↑(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.snd f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
    (Function.comp (β := (↑(pullback (𝟙 S) g) : Type u))
      (⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) : (a : (↑(pullback (𝟙 S) 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) (Y := pullback (𝟙 S) g) (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯)) :
        (a : (↑(pullback f g) : Type u)) → (↑(pullback (𝟙 S) g) : Type u)))
⊢ IsOpenEmbedding (X := (↑(pullback f g) : Type u)) (Y := (↑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.snd f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))

Tactic:
convert!
    (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₂ := 𝟙 Y) f g (𝟙 _) g H
        (homeoOfIso (Iso.refl _)).isOpenEmbedding (𝟙 _) rfl (by simp))

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.id, CategoryTheory.Iso.refl, TopCat.homeoOfIso, TopCat.pullback_map_isOpenEmbedding, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp, rfl, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
H :
  IsOpenEmbedding (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
⊢ Eq (α := (↑(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.snd f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑Y : Type u))
    (Function.comp (β := (↑(pullback (𝟙 S) g) : Type u))
      (⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) : (a : (↑(pullback (𝟙 S) 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) (Y := pullback (𝟙 S) g) (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯)) :
        (a : (↑(pullback f g) : Type u)) → (↑(pullback (𝟙 S) g) : Type u)))

Tactic:
simp [homeoOfIso, ← coe_comp]

Premises used: TopCat.homeoOfIso, TopCat.coe_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑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))
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S

Tactic:
simp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑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))
h :
  Eq (α := (↑(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.fst f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
    (Function.comp (β := (↑(pullback f (𝟙 S)) : Type u))
      (⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) : (a : (↑(pullback f (𝟙 S)) : 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) (Y := pullback f (𝟙 S)) (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯)) :
        (a : (↑(pullback f g) : Type u)) → (↑(pullback f (𝟙 S)) : Type u)))
⊢ IsOpenEmbedding (X := (↑(pullback f g) : Type u)) (Y := (↑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.fst f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑X : Type u))

Tactic:
convert!
    (homeoOfIso (asIso (pullback.fst f (𝟙 S)))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₁ := 𝟙 X) f g f (𝟙 _)
        (homeoOfIso (Iso.refl _)).isOpenEmbedding H (𝟙 _) rfl (by simp))

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Iso.refl, TopCat.homeoOfIso, CategoryTheory.Limits.pullback.fst, TopCat.pullback_map_isOpenEmbedding, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp, rfl, CategoryTheory.asIso
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑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))
⊢ Eq (α := (↑(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.fst f g)) :
      (a : (↑(pullback f g) : Type u)) → (↑X : Type u))
    (Function.comp (β := (↑(pullback f (𝟙 S)) : Type u))
      (⇑(homeoOfIso (asIso (pullback.fst f (𝟙 S)))) : (a : (↑(pullback f (𝟙 S)) : 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) (Y := pullback f (𝟙 S)) (pullback.map f g f (𝟙 S) (𝟙 X) g (𝟙 S) ⋯ ⋯)) :
        (a : (↑(pullback f g) : Type u)) → (↑(pullback f (𝟙 S)) : Type u)))

Tactic:
simp [homeoOfIso, ← coe_comp]

Premises used: TopCat.homeoOfIso, TopCat.coe_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  IsOpenEmbedding (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))
H₂ :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑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))
⊢ IsOpenEmbedding (X := (↑(pullback f g) : Type u)) (Y := (↑S : Type u))
    (Function.comp (β := (↑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))
      (⇑(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)))

Tactic:
H₂.comp (snd_isOpenEmbedding_of_left H₁ g)

Premises used: TopCat.snd_isOpenEmbedding_of_left, Topology.IsOpenEmbedding.comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  IsOpenEmbedding (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))
H₂ :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑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))
h :
  (↑((cospan f g).obj WalkingCospan.one) : Type u) = (↑S : Type u) →
    Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)) :
        (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
      (Function.comp (β := (↑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))
        (⇑(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)))
⊢ IsOpenEmbedding (X := (↑(limit (cospan f g)) : Type u)) (Y := (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))

Tactic:
convert! H₂.comp (snd_isOpenEmbedding_of_left H₁ g)

Premises used: TopCat.snd_isOpenEmbedding_of_left, Topology.IsOpenEmbedding.comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  IsOpenEmbedding (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))
H₂ :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑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))
e_2 : (↑((cospan f g).obj WalkingCospan.one) : Type u) = (↑S : Type u)
h :
  Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : 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 ≫ g)) :
      (a : (↑(pullback f g) : Type u)) → (↑S : Type u))
⊢ Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.one)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (Function.comp (β := (↑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))
      (⇑(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)))

Tactic:
rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr]

Premises used: CategoryTheory.Limits.WalkingCospan.Hom.inr, TopCat.coe_comp, CategoryTheory.Limits.limit.w
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ :
  IsOpenEmbedding (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))
H₂ :
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑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))
e_2 : (↑((cospan f g).obj WalkingCospan.one) : Type u) = (↑S : Type u)
⊢ Eq (α := (↑(limit (cospan f g)) : Type u) → (↑((cospan f g).obj WalkingCospan.one) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          limit (cospan f g)) (limit.π (cospan f g) WalkingCospan.right ≫ (cospan f g).map WalkingCospan.Hom.inr)) :
      (a : (↑(limit (cospan f g)) : Type u)) → (↑((cospan f g).obj WalkingCospan.one) : 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 ≫ g)) :
      (a : (↑(pullback f g) : Type u)) → (↑S : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
H :
  Subset (α := Set (↑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)))
    (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)))
x : (↑X : Type u)
rw :
  Membership.mem (γ := Set (↑X : Type u))
    {x : (↑X : Type u) |
      ∃ (y : (↑Y : 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 (↑X : 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.fst f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑X : Type u)))
    x

Tactic:
rw [pullback_fst_range]

Premises used: TopCat.pullback_fst_range
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
H :
  Subset (α := Set (↑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)))
    (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)))
x : (↑X : Type u)
⊢ Membership.mem (γ := Set (↑X : Type u))
    {x : (↑X : Type u) |
      ∃ (y : (↑Y : 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.symm⟩

Premises used: Set.mem_range_self, Exists.choose_spec, Set.Mem, setOf, Exists.intro, Eq.symm
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
H :
  Subset (α := Set (↑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)))
    (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)))
x : (↑X : Type u)
⊢ Membership.mem (γ := Set (↑X : Type u))
    {x : (↑X : Type u) |
      ∃ (y : (↑Y : 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.symm⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
H :
  Subset (α := Set (↑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)))
    (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)))
esto : (↑(pullback f g) : Type u) ≃ₜ (↑X : Type u) :=
  ⋯.toHomeomorph.trans
    {
      toFun :=
        Subtype.val (p := fun (x : (↑X : Type u)) ↦
          Membership.mem (γ := Set (↑X : 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.fst f g)) :
                (a : (↑(pullback f g) : Type u)) → (↑X : Type u)))
            x),
      invFun := fun (x : (↑X : Type u)) ↦
        Subtype.mk (p := fun (x : (↑X : Type u)) ↦
          Membership.mem (γ := Set (↑X : 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.fst f g)) :
                (a : (↑(pullback f g) : Type u)) → (↑X : 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
g : Y ⟶ S
hg :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑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))
H :
  Subset (α := Set (↑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)))
    (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)))
esto : (↑(pullback f g) : Type u) ≃ₜ (↑X : Type u) :=
  ⋯.toHomeomorph.trans
    {
      toFun :=
        Subtype.val (p := fun (x : (↑X : Type u)) ↦
          Membership.mem (γ := Set (↑X : 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.fst f g)) :
                (a : (↑(pullback f g) : Type u)) → (↑X : Type u)))
            x),
      invFun := fun (x : (↑X : Type u)) ↦
        Subtype.mk (p := fun (x : (↑X : Type u)) ↦
          Membership.mem (γ := Set (↑X : 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.fst f g)) :
                (a : (↑(pullback f g) : Type u)) → (↑X : Type u)))
            x)
          x ⋯,
      left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsIso (X := pullback f g) (pullback.fst f g)

Tactic:
convert! (isoOfHomeo esto).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, TopCat.isoOfHomeo