awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ 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:
hs i
-- 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))
h :
  (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u) = (↑((ofOpenSubsets U).U i) : Type u) →
    Eq (α := Set (↑(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))
      ((⇑(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)
⊢ 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))

Tactic:
convert! hs i using 1
-- 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))
e_1 : (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u) = (↑((ofOpenSubsets U).U i) : Type u)
h :
  Set.preimage (β := (↑(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)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
        s) =
    s
⊢ Eq (α := Set (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
    (Set.preimage (β := (↑(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 : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
      (Set.preimage (β := (↑(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)
                (fromOpenSubsetsGlue U)) :
            (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : 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)) ⁻¹'
      s)

Tactic:
congr! 1
-- 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))
e_1 : (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u) = (↑((ofOpenSubsets U).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)
            (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)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
        s) =
    s

Tactic:
Set.preimage_image_eq _ (fromOpenSubsetsGlue_injective U)

Premises used: TopCat.GlueData.fromOpenSubsetsGlue_injective, Set.preimage_image_eq
-- 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))
e_1 : (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u) = (↑((ofOpenSubsets U).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)
            (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)
              (fromOpenSubsetsGlue U)) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u)) ''
        s) =
    s

Tactic:
exact Set.preimage_image_eq _ (fromOpenSubsetsGlue_injective U)

Premises used: TopCat.GlueData.fromOpenSubsetsGlue_injective, Set.preimage_image_eq
-- 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))
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := 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 ∩
      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)))
    ((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))

Tactic:
⟨Set.mem_image_of_mem _ hx, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, Set.mem_image_of_mem, And.intro
-- 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 :
  Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u))
    (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)))
    ((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') :
      α)
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u))
    (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)))
    ((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))

Tactic:
rw [ι_fromOpenSubsetsGlue_apply]

Premises used: TopCat.GlueData.ι_fromOpenSubsetsGlue_apply
-- 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))
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u))
    (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)))
    ((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') :
      α)

Tactic:
Set.mem_range_self (f := (Opens.inclusion' _).hom) ⟨x, hx'⟩

Premises used: Set.mem_range_self, Set.Mem, Subtype.mk
-- 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))
⊢ Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(of α) : Type u))
    (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)))
    ((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') :
      α)

Tactic:
exact Set.mem_range_self (f := (Opens.inclusion' _).hom) ⟨x, hx'⟩

Premises used: Set.mem_range_self, Subtype.mk
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ IsOpenEmbedding (X := (↑(ofOpenSubsets U).glued : Type u)) (Y := (↑(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))

Tactic:
.of_continuous_injective_isOpenMap (ContinuousMap.continuous_toFun _)
    (fromOpenSubsetsGlue_injective U) (fromOpenSubsetsGlue_isOpenMap U)

Premises used: Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, TopCat.GlueData.fromOpenSubsetsGlue_injective, ContinuousMap.continuous_toFun, TopCat.GlueData.fromOpenSubsetsGlue_isOpenMap
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
h :
  ∀ (x : (↑(of α) : Type u)),
    Membership.mem (γ := Set (↑(of α) : Type u))
        (Set.range (ι := (↑(ofOpenSubsets U).glued : 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 ↔
      Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x
⊢ Eq (α := Set (↑(of α) : Type u))
    (Set.range (ι := (↑(ofOpenSubsets U).glued : 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)))
    (⋃ (i : J), (↑(U i) : Set α))

Tactic:
ext
-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
x : (↑(of α) : Type u)
h :
  Membership.mem (γ := Set (↑(of α) : Type u))
      (Set.range (ι := (↑(ofOpenSubsets U).glued : 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 →
    Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x
h₁ :
  Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x →
    Membership.mem (γ := Set (↑(of α) : Type u))
      (Set.range (ι := (↑(ofOpenSubsets U).glued : 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
⊢ Membership.mem (γ := Set (↑(of α) : Type u))
      (Set.range (ι := (↑(ofOpenSubsets U).glued : 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 ↔
    Membership.mem (γ := Set (↑(of α) : Type u)) (⋃ (i : J), (↑(U i) : Set α)) x

Tactic:
constructor