awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hUS : 𝒫 U ∈ S
hUu : K \ U ⊆ ⋃ i ∈ u, i
T : Set (Set α)
hTS : T ⊆ u
hT : T.Finite
hKT : K \ U ⊆ ⋃ i ∈ T, i
t : Set α
htK : t ⊆ K
x : α
hxt : x ∈ t
hxU : x ∉ U
V : Set α
hVT : V ∈ T
hxV : x ∈ V
⊢ Membership.mem (γ := Set (Set α)) (⋃ a ∈ T, {s : Set α | (s ∩ a).Nonempty}) t

Tactic:
exact mem_biUnion hVT ⟨x, hxt, hxV⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {V : Set α | IsOpen[inst] V} U
hUS : (fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U ∈ S
hUu :
  Membership.mem (γ := Set (Set α)) ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U) (K \ ⋃₀ u)
neg :
  ∀ (x : α) (hxu : x ∈ K \ ⋃₀ u) (hxU : x ∈ U),
    ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
obtain ⟨x, hxu, hxU⟩ := hUu
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
s : Set (Set α)
hsK : s ⊆ 𝒫 K
hs : ∀ L ∈ s, IsCompact L
S : Set (Set (Set α))
hS :
  S ⊆
    powerset '' {U : Set α | IsOpen[inst] U} ∪
      (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}
hKS : {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ S
u : Set (Set α) := {U : Set α | IsOpen[inst] U ∧ {s : Set α | (s ∩ U).Nonempty} ∈ S}
hsu : ∀ (L : Set α) (h : L ∈ s), (K \ ⋃₀ u ∩ L).Nonempty
U : Set α
hU : Membership.mem (γ := Set (Set α)) {V : Set α | IsOpen[inst] V} U
hUS : (fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U ∈ S
x : α
hxu : x ∈ K \ ⋃₀ u
hxU : x ∈ U
⊢ ∃ Q ⊆ S, Q.Finite ∧ {t : Set α | t ⊆ K ∧ ∀ L ∈ s, (t ∩ L).Nonempty} ⊆ ⋃₀ Q

Tactic:
cases hxu.2 <| mem_sUnion_of_mem hxU ⟨hU, hUS⟩

Premises used: And.right
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ IsCompact (𝒫 K)

Tactic:
simpa using isCompact_aux hK (s := ∅)

Premises used: _private.0.TopologicalSpace.vietoris.isCompact_aux
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : CompactSpace α
⊢ CompactSpace.{u_1} (Set α)

Tactic:
⟨powerset_univ ▸ isCompact_univ.powerset_vietoris⟩

Premises used: Eq.rec, Set.powerset_univ, CompactSpace.mk, isCompact_univ, IsCompact.powerset_vietoris
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : s ⤳ t
⊢ t ⊆ closure[inst] s

Tactic:
h.mem_closed isClosed_closure.powerset_vietoris subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.powerset, IsClosed.powerset_vietoris, isClosed_closure, Specializes.mem_closed
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
⊢ s ⤳ t ↔ (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s

Tactic:
⟨fun h => ⟨fun x hx => ?_, subset_closure_of_specializes h⟩, fun ⟨hst, hts⟩ => ?_⟩

Premises used: Specializes, And.intro, TopologicalSpace.vietoris.subset_closure_of_specializes, Iff.intro, _private.0.TopologicalSpace.vietoris.specializes_iff.match_1
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
refine_1 : ∀ (h : s ⤳ t) (x : α) (hx : x ∈ s), ∃ y ∈ t, x ⤳ y
refine_2 :
  (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s → ∀ (hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y) (hts : t ⊆ closure[inst] s), s ⤳ t
⊢ s ⤳ t ↔ (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s

Tactic:
refine ⟨fun h => ⟨fun x hx => ?_, subset_closure_of_specializes h⟩, fun ⟨hst, hts⟩ => ?_⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : s ⤳ t
x : α
hx : x ∈ s
refine_1 : ∀ (y : α) (hyt : y ∈ t) (hxy : Membership.mem (γ := Set α) (closure[inst] {x}) y), ∃ y ∈ t, x ⤳ y
⊢ ∃ y ∈ t, x ⤳ y

Tactic:
obtain ⟨y, hyt, hxy⟩ := h.mem_closed (s := {u | (u ∩ closure {x}).Nonempty})
      (isClosed_inter_nonempty_of_isClosed isClosed_closure) ⟨x, hx, subset_closure rfl⟩

Premises used: subset_closure, TopologicalSpace.vietoris.isClosed_inter_nonempty_of_isClosed, And.intro, Exists.intro, isClosed_closure, rfl, Specializes.mem_closed
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : s ⤳ t
x : α
hx : x ∈ s
y : α
hyt : y ∈ t
hxy : Membership.mem (γ := Set α) (closure[inst] {x}) y
⊢ ∃ y ∈ t, x ⤳ y

Tactic:
⟨y, hyt, specializes_iff_mem_closure.mpr hxy⟩

Premises used: Iff.mpr, specializes_iff_mem_closure, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : s ⤳ t
x : α
hx : x ∈ s
y : α
hyt : y ∈ t
hxy : Membership.mem (γ := Set α) (closure[inst] {x}) y
⊢ ∃ y ∈ t, x ⤳ y

Tactic:
exact ⟨y, hyt, specializes_iff_mem_closure.mpr hxy⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
refine_2 :
  ∀ (i : Set (Set α))
    (j :
      Membership.mem (γ := Set (Set (Set α)))
        {s : Set (Set α) |
          t ∈ s ∧
            Membership.mem (γ := Set (Set (Set α)))
              (powerset '' {U : Set α | IsOpen[inst] U} ∪
                (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U})
              s}
        i),
    ⨅ (s_1 : Set (Set α)),
        ⨅ (_ :
          Membership.mem (γ := Set (Set (Set α)))
            {s_2 : Set (Set α) |
              s ∈ s_2 ∧
                Membership.mem (γ := Set (Set (Set α)))
                  (powerset '' {U : Set α | IsOpen[inst] U} ∪
                    (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                  s_2}
            s_1),
          Filter.principal s_1 ≤
      Filter.principal i
⊢ s ⤳ t

Tactic:
simp_rw [Specializes, nhds_generateFrom, le_iInf₂_iff]

Premises used: Specializes, TopologicalSpace.nhds_generateFrom, le_iInf₂_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hs : t ∈ 𝒫 U
⊢ ⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1 ≤
    Filter.principal (𝒫 U)

Tactic:
iInf₂_le U.powerset ⟨fun x hx => ?_, .inl <| mem_image_of_mem _ hU⟩

Premises used: Set.Mem, iInf₂_le, setOf, Set.powerset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hs : t ∈ 𝒫 U
refine_2 : ∀ (x : α) (hx : x ∈ s), x ∈ U
⊢ ⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1 ≤
    Filter.principal (𝒫 U)

Tactic:
refine iInf₂_le U.powerset ⟨fun x hx => ?_, .inl <| mem_image_of_mem _ hU⟩

Premises used: iInf₂_le, Set.powerset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hs : t ∈ 𝒫 U
x : α
hx : x ∈ s
refine_2 : ∀ (y : α) (hyt : y ∈ t) (hxy : x ⤳ y), x ∈ U
⊢ x ∈ U

Tactic:
obtain ⟨y, hyt, hxy⟩ := hst x hx
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hs : t ∈ 𝒫 U
x : α
hx : x ∈ s
y : α
hyt : y ∈ t
hxy : x ⤳ y
⊢ x ∈ U

Tactic:
hxy.mem_open hU <| hs hyt

Premises used: Specializes.mem_open
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hs : t ∈ 𝒫 U
x : α
hx : x ∈ s
y : α
hyt : y ∈ t
hxy : x ⤳ y
⊢ x ∈ U

Tactic:
exact hxy.mem_open hU <| hs hyt

Premises used: Specializes.mem_open
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
hs : Membership.mem (γ := Set (Set α)) ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U) t
refine_2 :
  ∀ (x : α) (hxt : x ∈ t) (hxU : x ∈ U),
    LE.le.{u_1} (α := Filter (Set α))
      (⨅ (s_1 : Set (Set α)),
        ⨅ (_ :
          Membership.mem (γ := Set (Set (Set α)))
            {s_2 : Set (Set α) |
              s ∈ s_2 ∧
                Membership.mem (γ := Set (Set (Set α)))
                  (powerset '' {U : Set α | IsOpen[inst] U} ∪
                    (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                  s_2}
            s_1),
          Filter.principal s_1)
      (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))
⊢ LE.le.{u_1} (α := Filter (Set α))
    (⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1)
    (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))

Tactic:
obtain ⟨x, hxt, hxU⟩ := hs
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
x : α
hxt : x ∈ t
hxU : x ∈ U
refine_2 :
  ∀ (y : α) (hyU : y ∈ U) (hys : y ∈ s),
    LE.le.{u_1} (α := Filter (Set α))
      (⨅ (s_1 : Set (Set α)),
        ⨅ (_ :
          Membership.mem (γ := Set (Set (Set α)))
            {s_2 : Set (Set α) |
              s ∈ s_2 ∧
                Membership.mem (γ := Set (Set (Set α)))
                  (powerset '' {U : Set α | IsOpen[inst] U} ∪
                    (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                  s_2}
            s_1),
          Filter.principal s_1)
      (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))
⊢ LE.le.{u_1} (α := Filter (Set α))
    (⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1)
    (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))

Tactic:
obtain ⟨y, hyU, hys⟩ := mem_closure_iff.mp (hts hxt) U hU hxU

Premises used: mem_closure_iff, Iff.mp
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
x : α
hxt : x ∈ t
hxU : x ∈ U
y : α
hyU : y ∈ U
hys : y ∈ s
⊢ LE.le.{u_1} (α := Filter (Set α))
    (⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1)
    (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))

Tactic:
iInf₂_le {t | (t ∩ U).Nonempty} ⟨⟨y, hys, hyU⟩, .inr <| mem_image_of_mem _ hU⟩

Premises used: Set.Mem, iInf₂_le, setOf, Inter.inter, Set.Nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
h : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s
hst : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
hts : t ⊆ closure[inst] s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
x : α
hxt : x ∈ t
hxU : x ∈ U
y : α
hyU : y ∈ U
hys : y ∈ s
⊢ LE.le.{u_1} (α := Filter (Set α))
    (⨅ (s_1 : Set (Set α)),
      ⨅ (_ :
        Membership.mem (γ := Set (Set (Set α)))
          {s_2 : Set (Set α) |
            s ∈ s_2 ∧
              Membership.mem (γ := Set (Set (Set α)))
                (powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})
                s_2}
          s_1),
        Filter.principal s_1)
    (Filter.principal ((fun (V : Set α) ↦ ({s : Set α | (s ∩ V).Nonempty} : Set (Set α))) U))

Tactic:
exact iInf₂_le {t | (t ∩ U).Nonempty} ⟨⟨y, hys, hyU⟩, .inr <| mem_image_of_mem _ hU⟩

Premises used: iInf₂_le, setOf, Inter.inter, Set.Nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
inst_1 : T1Space α
simp_rw : (∀ x ∈ s, ∃ y ∈ t, x ⤳ y) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
simp_rw₁ : (∀ x ∈ s, ∃ y ∈ t, x = y) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
simp_rw₂ : (∀ x ∈ s, x ∈ t ∧ True) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
simp_rw₃ : (∀ x ∈ s, x ∈ t) ∧ t ⊆ closure[inst] s ↔ s ⊆ t ∧ t ⊆ closure[inst] s
⊢ s ⤳ t ↔ s ⊆ t ∧ t ⊆ closure[inst] s

Tactic:
simp_rw [specializes_iff, specializes_iff_eq, existsAndEq, and_true, ← subset_def]

Premises used: TopologicalSpace.vietoris.specializes_iff, and_true, Set.subset_def, ExistsAndEq.existsAndEq, specializes_iff_eq
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
inst_1 : T1Space α
h : s ⤳ t
⊢ s ⊆ t

Tactic:
(specializes_iff_of_t1Space.mp h).1

Premises used: TopologicalSpace.vietoris.specializes_iff_of_t1Space, And.left, Iff.mp
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
hts : t ⊆ closure[inst] s
⊢ s ⤳ t

Tactic:
aesop (add simp specializes_iff)

Premises used: TopologicalSpace.vietoris.specializes_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ s ⤳ closure[inst] s

Tactic:
specializes_of_subset_closure subset_closure .rfl

Premises used: TopologicalSpace.vietoris.specializes_of_subset_closure, subset_closure, Set.Subset.rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Continuous[_, TopologicalSpace.vietoris α] SetLike.coe

Tactic:
isEmbedding_coe.continuous

Premises used: TopologicalSpace.Compacts.isEmbedding_coe, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
U : Set α
h : IsOpen[inst] U
⊢ IsOpen.{u_1} (X := Compacts α) {K : Compacts α | (↑K : Set α) ⊆ U}

Tactic:
continuous_coe.isOpen_preimage _ h.powerset_vietoris

Premises used: Set.Mem, setOf, Set.powerset, TopologicalSpace.Compacts.continuous_coe, Set.preimage, IsOpen.powerset_vietoris, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
U : Set α
h : IsOpen[inst] U
⊢ IsOpen.{u_1} (X := Compacts α) {K : Compacts α | ((↑K : Set α) ∩ U).Nonempty}

Tactic:
continuous_coe.isOpen_preimage _ <| vietoris.isOpen_inter_nonempty_of_isOpen h

Premises used: Set.Mem, setOf, TopologicalSpace.Compacts.continuous_coe, Set.Nonempty, TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen, Set.preimage, Continuous.isOpen_preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
simp_rw : IsOpen.{u_1} (X := Compacts α) {a : Compacts α | ((↑a : Set α) ∩ Fᶜ).Nonempty}
⊢ IsClosed.{u_1} (X := Compacts α) {K : Compacts α | (↑K : Set α) ⊆ F}

Tactic:
simp_rw [← isOpen_compl_iff, Set.compl_setOf, ← Set.inter_compl_nonempty_iff]

Premises used: Set.inter_compl_nonempty_iff, isOpen_compl_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsOpen.{u_1} (X := Compacts α) {a : Compacts α | ((↑a : Set α) ∩ Fᶜ).Nonempty}

Tactic:
isOpen_inter_nonempty_of_isOpen h.isOpen_compl

Premises used: IsClosed.isOpen_compl, TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsOpen.{u_1} (X := Compacts α) {a : Compacts α | ((↑a : Set α) ∩ Fᶜ).Nonempty}

Tactic:
exact isOpen_inter_nonempty_of_isOpen h.isOpen_compl

Premises used: IsClosed.isOpen_compl, TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
simp_rw : IsClosed.{u_1} (X := Compacts α) {a : Compacts α | (↑a : Set α) ⊆ Fᶜ}ᶜ
⊢ IsClosed.{u_1} (X := Compacts α) {K : Compacts α | ((↑K : Set α) ∩ F).Nonempty}

Tactic:
simp_rw +singlePass [← compl_compl F, Set.inter_compl_nonempty_iff, ← Set.compl_setOf]

Premises used: compl_compl, Set.inter_compl_nonempty_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed.{u_1} (X := Compacts α) {a : Compacts α | (↑a : Set α) ⊆ Fᶜ}ᶜ

Tactic:
(isOpen_subsets_of_isOpen h.isOpen_compl).isClosed_compl

Premises used: IsClosed.isOpen_compl, Set.Mem, setOf, IsOpen.isClosed_compl, TopologicalSpace.Compacts.isOpen_subsets_of_isOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed.{u_1} (X := Compacts α) {a : Compacts α | (↑a : Set α) ⊆ Fᶜ}ᶜ

Tactic:
exact (isOpen_subsets_of_isOpen h.isOpen_compl).isClosed_compl

Premises used: IsClosed.isOpen_compl, IsOpen.isClosed_compl, TopologicalSpace.Compacts.isOpen_subsets_of_isOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsClopen (X := Compacts α) (SetLike.coe ⁻¹' {∅})

Tactic:
vietoris.isClopen_singleton_empty.preimage continuous_coe

Premises used: TopologicalSpace.vietoris.isClopen_singleton_empty, TopologicalSpace.Compacts.continuous_coe, IsClopen.preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {∅})
⊢ IsClopen (X := Compacts α) {⊥}

Tactic:
convert! vietoris.isClopen_singleton_empty.preimage continuous_coe

Premises used: TopologicalSpace.vietoris.isClopen_singleton_empty, TopologicalSpace.Compacts.continuous_coe, IsClopen.preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
h : Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {(↑⊥ : Set α)})
h₁ : Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' image (α := Compacts α) SetLike.coe {⊥})
h₂ h₃ : Eq (α := Set (Compacts α)) {⊥} {⊥}
⊢ Eq (α := Set (Compacts α)) {⊥} (SetLike.coe ⁻¹' {∅})

Tactic:
rw [← coe_bot, ← image_singleton (f := SetLike.coe), SetLike.coe_injective.preimage_image]

Premises used: Set.image_singleton, TopologicalSpace.Compacts.coe_bot, SetLike.coe_injective, Function.Injective.preimage_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ IsTopologicalBasis.{u_1} (α := Compacts α)
    ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ u ⊆ B})

Tactic:
hB.vietoris.isInducing isEmbedding_coe.isInducing
    |>.isTopologicalBasis_of_exists_subset ?_ ?_

Premises used: TopologicalSpace.IsTopologicalBasis.vietoris, TopologicalSpace.Compacts.isEmbedding_coe, Topology.IsEmbedding.isInducing, TopologicalSpace.IsTopologicalBasis.isInducing, TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset