awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑Y : 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.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)) ⁻¹'
      U)
    y
⊢ Membership.mem (α := (↑X : Type u)) (γ := 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))
    ((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))
        y :
      (↑X : Type u))

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

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, CategoryTheory.Limits.pullback.snd, setOf, CategoryTheory.congr_fun, Set.preimage, And.intro, Exists.intro, Set.image, CategoryTheory.Limits.pullback.condition, Eq.symm, DFunLike.coe
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑Y : 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.snd f g)) :
        (a : (↑(pullback f g) : Type u)) → (↑Y : Type u)) ⁻¹'
      U)
    y
⊢ Membership.mem (α := (↑X : Type u)) (γ := 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))
    ((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))
        y :
      (↑X : Type u))

Tactic:
exact
      ⟨(pullback.snd f g) y, hy,
        (CategoryTheory.congr_fun pullback.condition y).symm⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
U : Set (↑Y : Type u)
x : (↑X : Type u)
y : (↑Y : 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) g :
          (a : (↑Y : 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) f :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x :
      (↑Z : 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

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

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, Prod.mk, Subtype.mk, TopCat.pullbackIsoProdSubtype, And.intro, Exists.intro, Set.image, Eq.symm, 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 (↑Y : Type u)
x : (↑X : Type u)
y : (↑Y : 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) g :
          (a : (↑Y : 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) f :
          (a : (↑X : 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 (↑Y : Type u)
x : (↑X : Type u)
y : (↑Y : 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) g :
          (a : (↑Y : 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) f :
          (a : (↑X : 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)))
            (x, y) ⋯) :
        (↑X : Type u) × (↑Y : Type u)).2 =
    y
⊢ (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 :
                { 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)))
            (x, y) ⋯) :
        (↑(pullback f g) : Type u)) =
    y

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)
x : (↑X : Type u)
y : (↑Y : 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) g :
          (a : (↑Y : 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) f :
          (a : (↑X : 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)))
            (x, y) ⋯) :
        (↑X : Type u) × (↑Y : Type u)).1 =
    x
⊢ (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))
          (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)))
            (x, y) ⋯) :
        (↑(pullback f g) : Type u)) =
    x

Tactic:
rw [pullbackIsoProdSubtype_inv_fst_apply]

Premises used: TopCat.pullbackIsoProdSubtype_inv_fst_apply
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
rw :
  (∀ (j : WalkingParallelPair),
      IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑((parallelPair f g).obj j) : Type u)) →
              (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
          U)) ↔
    IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        U)
⊢ IsOpen U ↔
    IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        U)

Tactic:
rw [isOpen_iff_of_isColimit _ hc]

Premises used: TopCat.isOpen_iff_of_isColimit
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
mp :
  (∀ (j : WalkingParallelPair),
      IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑((parallelPair f g).obj j) : Type u)) →
              (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
          U)) →
    IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        U)
mpr :
  IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        U) →
    ∀ (j : WalkingParallelPair),
      IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑((parallelPair f g).obj j) : Type u)) →
              (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
          U)
⊢ (∀ (j : WalkingParallelPair),
      IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (c.ι.app j)) :
            (a : (↑((parallelPair f g).obj j) : Type u)) →
              (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
          U)) ↔
    IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        U)

Tactic:
constructor
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
h :
  ∀ (j : WalkingParallelPair),
    IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑((parallelPair f g).obj j) : Type u)) →
            (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
        U)
⊢ IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)

Tactic:
h .one

Premises used: CategoryTheory.Limits.WalkingParallelPair.one
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
h :
  ∀ (j : WalkingParallelPair),
    IsOpen (X := (↑((parallelPair f g).obj j) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (c.ι.app j)) :
          (a : (↑((parallelPair f g).obj j) : Type u)) →
            (↑(((Functor.const WalkingParallelPair).obj c.pt).obj j) : Type u)) ⁻¹'
        U)
⊢ IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)

Tactic:
exact h .one

Premises used: CategoryTheory.Limits.WalkingParallelPair.one
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
h :
  IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)
mpr :
  IsOpen (X := (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            ((parallelPair f g).map WalkingParallelPairHom.left ≫ c.ι.app WalkingParallelPair.one)) :
        (a : (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u)) →
          (↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.zero) : Type u)) ⁻¹'
      U)
⊢ IsOpen (X := (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.ι.app WalkingParallelPair.zero)) :
        (a : (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u)) →
          (↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.zero) : Type u)) ⁻¹'
      U)

Tactic:
rw [← c.w .left]

Premises used: CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.WalkingParallelPairHom.left
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
h :
  IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)
⊢ IsOpen (X := (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            ((parallelPair f g).map WalkingParallelPairHom.left ≫ c.ι.app WalkingParallelPair.one)) :
        (a : (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u)) →
          (↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.zero) : Type u)) ⁻¹'
      U)

Tactic:
Continuous.isOpen_preimage f.hom.continuous (c.π ⁻¹' U) h

Premises used: ContinuousMap.continuous, CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, Set.preimage, TopCat.Hom.hom, Continuous.isOpen_preimage, DFunLike.coe, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
h :
  IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)
⊢ IsOpen (X := (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            ((parallelPair f g).map WalkingParallelPairHom.left ≫ c.ι.app WalkingParallelPair.one)) :
        (a : (↑((parallelPair f g).obj WalkingParallelPair.zero) : Type u)) →
          (↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.zero) : Type u)) ⁻¹'
      U)

Tactic:
exact Continuous.isOpen_preimage f.hom.continuous (c.π ⁻¹' U) h

Premises used: ContinuousMap.continuous, CategoryTheory.ConcreteCategory.hom, Set.preimage, TopCat.Hom.hom, Continuous.isOpen_preimage, DFunLike.coe, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
h :
  IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)
⊢ IsOpen (X := (↑((parallelPair f g).obj WalkingParallelPair.one) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.ι.app WalkingParallelPair.one)) :
        (a : (↑((parallelPair f g).obj WalkingParallelPair.one) : Type u)) →
          (↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.one) : Type u)) ⁻¹'
      U)

Tactic:
h
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set (↑c.pt : Type u)
h :
  IsOpen (X := (↑Y : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
      U)
⊢ IsOpen (X := (↑((parallelPair f g).obj WalkingParallelPair.one) : Type u))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (c.ι.app WalkingParallelPair.one)) :
        (a : (↑((parallelPair f g).obj WalkingParallelPair.one) : Type u)) →
          (↑(((Functor.const WalkingParallelPair).obj c.pt).obj WalkingParallelPair.one) : Type u)) ⁻¹'
      U)

Tactic:
exact h
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
rw :
  IsCoinducing (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ∧
    Function.Surjective (α := (↑Y : Type u)) (β := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u))
⊢ IsQuotientMap (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
      (a : (↑Y : Type u)) → (↑c.pt : Type u))

Tactic:
rw [isQuotientMap_iff]

Premises used: Topology.isQuotientMap_iff
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
⊢ IsCoinducing (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ∧
    Function.Surjective (α := (↑Y : Type u)) (β := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u))

Tactic:
⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, ?_⟩

Premises used: Topology.IsCoinducing.of_isOpen_preimage_iff_isOpen, And.intro
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
refine_1 :
  ∀ (s : Set (↑c.pt : Type u)),
    IsOpen (X := (↑Y : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
            (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
          s) ↔
      IsOpen s
refine_2 :
  Function.Surjective (α := (↑Y : Type u)) (β := (↑c.pt : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
      (a : (↑Y : Type u)) → (↑c.pt : Type u))
⊢ IsCoinducing (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u)) ∧
    Function.Surjective (α := (↑Y : Type u)) (β := (↑c.pt : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
        (a : (↑Y : Type u)) → (↑c.pt : Type u))

Tactic:
refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦ ?_, ?_⟩
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
s : Set (↑c.pt : Type u)
⊢ IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        s) ↔
    IsOpen s

Tactic:
(isOpen_iff_of_isColimit_cofork c hc s).symm

Premises used: TopCat.isOpen_iff_of_isColimit_cofork, Iff.symm
-- Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks
Goal:
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
s : Set (↑c.pt : Type u)
⊢ IsOpen (X := (↑Y : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) c.π) :
          (a : (↑Y : Type u)) → (↑c.pt : Type u)) ⁻¹'
        s) ↔
    IsOpen s

Tactic:
exact (isOpen_iff_of_isColimit_cofork c hc s).symm

Premises used: TopCat.isOpen_iff_of_isColimit_cofork, Iff.symm