awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i j : (ofOpenSubsets U).J
w :
  ∀ (x : (↑((ofOpenSubsets U).diagram.left (i, j)) : Type u)),
    Eq (α := (↑(of α) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              (ofOpenSubsets U).diagram.left (i, j)) (Y := of α)
              ((ofOpenSubsets U).diagram.fst (i, j) ≫
                (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
                    ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
                  ((MultispanShape.prod (ofOpenSubsets U).J).fst (i, j))) :
            (a : (↑((ofOpenSubsets U).diagram.left (i, j)) : Type u)) → (↑(of α) : Type u))
          x :
        (↑(of α) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              (ofOpenSubsets U).diagram.left (i, j)) (Y := of α)
              ((ofOpenSubsets U).diagram.snd (i, j) ≫
                (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
                    ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
                  ((MultispanShape.prod (ofOpenSubsets U).J).snd (i, j))) :
            (a : (↑((ofOpenSubsets U).diagram.left (i, j)) : Type u)) → (↑(of α) : Type u))
          x :
        (↑(of α) : Type u))
⊢ Eq (α := (ofOpenSubsets U).diagram.left (i, j) ⟶ of α)
    ((ofOpenSubsets U).diagram.fst (i, j) ≫
      (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
          ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
        ((MultispanShape.prod (ofOpenSubsets U).J).fst (i, j)))
    ((ofOpenSubsets U).diagram.snd (i, j) ≫
      (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
          ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
        ((MultispanShape.prod (ofOpenSubsets U).J).snd (i, j)))

Tactic:
ext x
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i j : (ofOpenSubsets U).J
x : (↑((ofOpenSubsets U).diagram.left (i, j)) : Type u)
⊢ Eq (α := (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).diagram.left (i, j)) (Y := of α)
            ((ofOpenSubsets U).diagram.fst (i, j) ≫
              (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
                  ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
                ((MultispanShape.prod (ofOpenSubsets U).J).fst (i, j))) :
          (a : (↑((ofOpenSubsets U).diagram.left (i, j)) : Type u)) → (↑(of α) : Type u))
        x :
      (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).diagram.left (i, j)) (Y := of α)
            ((ofOpenSubsets U).diagram.snd (i, j) ≫
              (fun (x : (MultispanShape.prod (ofOpenSubsets U).J).R) ↦
                  ((U x).inclusion' : Functor.obj (Opens.toTopCat (of α)) (U x) ⟶ of α))
                ((MultispanShape.prod (ofOpenSubsets U).J).snd (i, j))) :
          (a : (↑((ofOpenSubsets U).diagram.left (i, j)) : Type u)) → (↑(of α) : Type u))
        x :
      (↑(of α) : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
⊢ (ofOpenSubsets U).ι i ≫ fromOpenSubsetsGlue U = (U i).inclusion'

Tactic:
Multicoequalizer.π_desc _ _ _ _ _

Premises used: CategoryTheory.Limits.Multicoequalizer.π_desc
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
x y : (↑(ofOpenSubsets U).glued : Type u)
e :
  Eq (α := (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        x :
      (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        y :
      (↑(of α) : Type u))
obtain :
  ∀ (i : (ofOpenSubsets U).J) (x : (↑(of α) : Type u)) (hx : x ∈ U i)
    (e :
      Eq (α := (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (fromOpenSubsetsGlue U) :
              (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (Y := (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
                  (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
                (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
              (↑(ofOpenSubsets U).glued : Type u)) :
          (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (fromOpenSubsetsGlue U) :
              (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
            y :
          (↑(of α) : Type u))),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) =
      y
⊢ x = y

Tactic:
obtain ⟨i, ⟨x, hx⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x

Premises used: TopCat.GlueData.ofOpenSubsets, TopCat.GlueData.ι_jointly_surjective, rfl
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx : x ∈ U i
j : (ofOpenSubsets U).J
y : (↑(of α) : Type u)
hy : y ∈ U j
e :
  Eq (α := (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
              (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
            (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
          (↑(ofOpenSubsets U).glued : Type u)) :
      (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι j) :
              (a : (↑((ofOpenSubsets U).U j) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
            (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j) y hy) :
          (↑(ofOpenSubsets U).glued : Type u)) :
      (↑(of α) : Type u))
⊢ Eq (α := (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).U i) (U i).inclusion' :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
      α)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).U j) (U j).inclusion' :
          (a : (↑((ofOpenSubsets U).U j) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j) y hy) :
      α)

Tactic:
rw [ι_fromOpenSubsetsGlue_apply, ι_fromOpenSubsetsGlue_apply] at e

Premises used: TopCat.GlueData.ι_fromOpenSubsetsGlue_apply
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy :
  Membership.mem (α := (↑(of α) : Type u)) (U j)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).U i) (U i).inclusion' :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
      α)
rw :
  (ofOpenSubsets U).Rel
    (Sigma.mk (β := fun (i : (ofOpenSubsets U).J) ↦ (↑((ofOpenSubsets U).U i) : Type u)) i
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx))
    (Sigma.mk (β := fun (i : (ofOpenSubsets U).J) ↦ (↑((ofOpenSubsets U).U i) : Type u)) j
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              (ofOpenSubsets U).U i) (U i).inclusion' :
            (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
          (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx))
        hy))
⊢ Eq (α := (↑(ofOpenSubsets U).glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
      (↑(ofOpenSubsets U).glued : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι j) :
          (a : (↑((ofOpenSubsets U).U j) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j)
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := (ofOpenSubsets U).U i) (U i).inclusion' :
                (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
              (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx))
            hy :
          ↥(U j)) :
      (↑(ofOpenSubsets U).glued : Type u))

Tactic:
rw [(ofOpenSubsets U).ι_eq_iff_rel]

Premises used: TopCat.GlueData.ofOpenSubsets, TopCat.GlueData.ι_eq_iff_rel
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy :
  Membership.mem (α := (↑(of α) : Type u)) (U j)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).U i) (U i).inclusion' :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
      α)
⊢ (ofOpenSubsets U).Rel
    (Sigma.mk (β := fun (i : (ofOpenSubsets U).J) ↦ (↑((ofOpenSubsets U).U i) : Type u)) i
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx))
    (Sigma.mk (β := fun (i : (ofOpenSubsets U).J) ↦ (↑((ofOpenSubsets U).U i) : Type u)) j
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              (ofOpenSubsets U).U i) (U i).inclusion' :
            (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
          (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx))
        hy))

Tactic:
⟨⟨⟨x, hx⟩, hy⟩, rfl, rfl⟩

Premises used: Subtype.mk, And.intro, TopCat.GlueData.Rel, Exists.intro, rfl
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx : x ∈ U i
j : (ofOpenSubsets U).J
hy :
  Membership.mem (α := (↑(of α) : Type u)) (U j)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).U i) (U i).inclusion' :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
      α)
⊢ (ofOpenSubsets U).Rel
    (Sigma.mk (β := fun (i : (ofOpenSubsets U).J) ↦ (↑((ofOpenSubsets U).U i) : Type u)) i
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx))
    (Sigma.mk (β := fun (i : (ofOpenSubsets U).J) ↦ (↑((ofOpenSubsets U).U i) : Type u)) j
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              (ofOpenSubsets U).U i) (U i).inclusion' :
            (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
          (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx))
        hy))

Tactic:
exact ⟨⟨⟨x, hx⟩, hy⟩, rfl, rfl⟩
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set (↑(ofOpenSubsets U).glued : Type u)
hs : IsOpen s
⊢ ∀ (i : (ofOpenSubsets U).J),
    IsOpen (X := (↑((ofOpenSubsets U).U i) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i)) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u)) ⁻¹'
        s)

Tactic:
rw [(ofOpenSubsets U).isOpen_iff] at hs

Premises used: TopCat.GlueData.isOpen_iff, TopCat.GlueData.ofOpenSubsets
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set (↑(ofOpenSubsets U).glued : Type u)
hs :
  ∀ (i : (ofOpenSubsets U).J),
    IsOpen (X := (↑((ofOpenSubsets U).U i) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i)) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u)) ⁻¹'
        s)
rw :
  ∀ (x : (↑(of α) : Type u)),
    Membership.mem (γ := Set (↑(of α) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (fromOpenSubsetsGlue U)) :
            (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
          s)
        x →
      ∃
        t ⊆
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (fromOpenSubsetsGlue U)) :
              (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
            s,
        IsOpen[inst] t ∧ x ∈ t
⊢ IsOpen[inst]
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U)) :
        (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
      s)

Tactic:
rw [isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set (↑(ofOpenSubsets U).glued : Type u)
hs :
  ∀ (i : (ofOpenSubsets U).J),
    IsOpen (X := (↑((ofOpenSubsets U).U i) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i)) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u)) ⁻¹'
        s)
x : (↑(ofOpenSubsets U).glued : Type u)
hx : x ∈ s
obtain :
  ∀ (i : (ofOpenSubsets U).J) (x : (↑(of α) : Type u)) (hx' : x ∈ U i)
    (hx :
      Membership.mem (α := (↑(ofOpenSubsets U).glued : Type u)) s
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
              (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
            (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
          (↑(ofOpenSubsets U).glued : Type u))),
    ∃
      t ⊆
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (fromOpenSubsetsGlue U)) :
            (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
          s,
      IsOpen[inst] t ∧
        Membership.mem (α := (↑(of α) : Type u)) t
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (fromOpenSubsetsGlue U) :
                (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (Y := (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
                    (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
                  (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
                (↑(ofOpenSubsets U).glued : Type u)) :
            (↑(of α) : Type u))
⊢ ∃
    t ⊆
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
        s,
    IsOpen[inst] t ∧
      Membership.mem (α := (↑(of α) : Type u)) t
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (fromOpenSubsetsGlue U) :
              (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
            x :
          (↑(of α) : Type u))

Tactic:
obtain ⟨i, ⟨x, hx'⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x

Premises used: TopCat.GlueData.ofOpenSubsets, TopCat.GlueData.ι_jointly_surjective, rfl
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set (↑(ofOpenSubsets U).glued : Type u)
hs :
  ∀ (i : (ofOpenSubsets U).J),
    IsOpen (X := (↑((ofOpenSubsets U).U i) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i)) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u)) ⁻¹'
        s)
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx' : x ∈ U i
hx :
  Membership.mem (α := (↑(ofOpenSubsets U).glued : Type u)) s
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
      (↑(ofOpenSubsets U).glued : Type u))
right :
  IsOpen[inst]
    (Set.image (α := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
        (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u))
      (Set.preimage (β := (↑(of α) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
          (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (fromOpenSubsetsGlue U)) :
            (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
          s)))
⊢ IsOpen[inst]
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
        s ∩
      Set.range (ι := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
          (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u)))

Tactic:
rw [← Set.image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set (↑(ofOpenSubsets U).glued : Type u)
hs :
  ∀ (i : (ofOpenSubsets U).J),
    IsOpen (X := (↑((ofOpenSubsets U).U i) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i)) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u)) ⁻¹'
        s)
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx' : x ∈ U i
hx :
  Membership.mem (α := (↑(ofOpenSubsets U).glued : Type u)) s
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx') :
      (↑(ofOpenSubsets U).glued : Type u))
right :
  IsOpen (X := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
    (Set.preimage (β := (↑(of α) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
        (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
        s))
⊢ IsOpen[inst]
    (Set.image (α := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
        (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u))
      (Set.preimage (β := (↑(of α) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
          (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (fromOpenSubsetsGlue U)) :
            (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
          s)))

Tactic:
apply (Opens.isOpenEmbedding (X := TopCat.of α) (U i)).isOpenMap

Premises used: Topology.IsOpenEmbedding.isOpenMap, TopologicalSpace.Opens.isOpenEmbedding