awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
h : Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty} t
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ f U).Nonempty

Tactic:
ht₂ hU
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
s : Set α
hs₁ : s ⊆ ⋃₀ u
hs₂ : ∀ U ∈ u, (s ∩ U).Nonempty
f : (U : Set α) → Set α
hfB : ∀ U ∈ u, f U ∈ B
hfU : ∀ U ∈ u, f U ⊆ U
hfs : ∀ U ∈ u, (s ∩ f U).Nonempty
t : Set α
h : Membership.mem (γ := Set (Set α)) {s : Set α | s ⊆ (⋃₀ u, f '' u).1 ∧ ∀ U ∈ (⋃₀ u, f '' u).2, (s ∩ U).Nonempty} t
ht₁ : t ⊆ (⋃₀ u, f '' u).1
ht₂ : ∀ ⦃x : Set α⦄, x ∈ u → (t ∩ f x).Nonempty
U : Set α
hU : U ∈ u
⊢ (t ∩ f U).Nonempty

Tactic:
exact ht₂ hU
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
⊢ Continuous[inst, TopologicalSpace.vietoris β] f ↔
    (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
      ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)

Tactic:
⟨fun hf =>
      ⟨fun U hU => hU.powerset_vietoris.preimage hf, fun F hF => hF.powerset_vietoris.preimage hf⟩,
    fun ⟨h₁, h₂⟩ => ?_⟩

Premises used: _private.0.TopologicalSpace.vietoris.continuous_iff.match_1, Continuous, IsOpen.powerset_vietoris, And.intro, Iff.intro, IsClosed.powerset_vietoris, IsClosed.preimage, IsOpen.preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
refine :
  ((∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
      ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)) →
    ∀ (h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U))
      (h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)),
      Continuous[inst, TopologicalSpace.vietoris β] f
⊢ Continuous[inst, TopologicalSpace.vietoris β] f ↔
    (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
      ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)

Tactic:
refine ⟨fun hf =>
      ⟨fun U hU => hU.powerset_vietoris.preimage hf, fun F hF => hF.powerset_vietoris.preimage hf⟩,
    fun ⟨h₁, h₂⟩ => ?_⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h :
  (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
rw :
  ∀ (s : Set (Set β)),
    Membership.mem (γ := Set (Set (Set β)))
        (powerset '' {U : Set β | IsOpen[inst_1] U} ∪
          (fun (V : Set β) ↦ {s : Set β | (s ∩ V).Nonempty}) '' {V : Set β | IsOpen[inst_1] V})
        s →
      IsOpen[inst] (f ⁻¹' s)
⊢ Continuous[inst, TopologicalSpace.vietoris β] f

Tactic:
rw [continuous_generateFrom_iff]

Premises used: continuous_generateFrom_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h :
  (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
U : Set β
hU : Membership.mem (γ := Set (Set β)) {U : Set β | IsOpen[inst_1] U} U
⊢ IsOpen[inst] (f ⁻¹' 𝒫 U)

Tactic:
h₁ U hU
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h :
  (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
U : Set β
hU : Membership.mem (γ := Set (Set β)) {U : Set β | IsOpen[inst_1] U} U
⊢ IsOpen[inst] (f ⁻¹' 𝒫 U)

Tactic:
exact h₁ U hU
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h :
  (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
U : Set β
hU : Membership.mem (γ := Set (Set β)) {V : Set β | IsOpen[inst_1] V} U
inr : IsClosed[inst] {a : α | f a ⊆ Uᶜ}
⊢ IsOpen[inst] (f ⁻¹' (fun (V : Set β) ↦ ({s : Set β | (s ∩ V).Nonempty} : Set (Set β))) U)

Tactic:
simp_rw [preimage_setOf_eq, ← not_disjoint_iff_nonempty_inter, ← compl_setOf, isOpen_compl_iff,
      ← subset_compl_iff_disjoint_right]

Premises used: Set.subset_compl_iff_disjoint_right, Set.not_disjoint_iff_nonempty_inter, Set.preimage_setOf_eq, isOpen_compl_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h :
  (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
U : Set β
hU : Membership.mem (γ := Set (Set β)) {V : Set β | IsOpen[inst_1] V} U
⊢ IsClosed[inst] {a : α | f a ⊆ Uᶜ}

Tactic:
h₂ Uᶜ hU.isClosed_compl

Premises used: Set.Mem, Compl.compl, setOf, Set.powerset, IsOpen.isClosed_compl, Set.preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → Set β
h :
  (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
h₁ : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[inst] (f ⁻¹' 𝒫 U)
h₂ : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[inst] (f ⁻¹' 𝒫 F)
U : Set β
hU : Membership.mem (γ := Set (Set β)) {V : Set β | IsOpen[inst_1] V} U
⊢ IsClosed[inst] {a : α | f a ⊆ Uᶜ}

Tactic:
exact h₂ Uᶜ hU.isClosed_compl

Premises used: Compl.compl, IsOpen.isClosed_compl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  inst =
    induced (Y := Set α) (fun (x : α) ↦ {x})
      (generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₁ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₂ :
  inst =
    generateFrom
      (image (α := Set (Set α)) (preimage fun (x : α) ↦ {x}) (powerset '' {U : Set α | IsOpen[inst] U}) ∪
        image (α := Set (Set α)) (preimage fun (x : α) ↦ {x})
          ((fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst] U}))
simp_rw₃ :
  inst =
    generateFrom
      ((fun (x : Set α) ↦ (fun (x : α) ↦ {x}) ⁻¹' 𝒫 x) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₄ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {t : Set α | t ⊆ a}) ''
          {U : Set α | IsOpen[inst] U} ∪
        (fun (x : Set α) ↦ preimage (β := Set α) (fun (x : α) ↦ {x}) {s : Set α | (s ∩ x).Nonempty}) ''
          {U : Set α | IsOpen[inst] U})
simp_rw₅ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | {a_1} ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
simp_rw₆ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | ({a_1} ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
simp_rw₇ :
  inst =
    generateFrom
      ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U} ∪
        (fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U})
simp_rw₈ : inst = generateFrom ((fun (a : Set α) ↦ {a_1 : α | a_1 ∈ a}) '' {U : Set α | IsOpen[inst] U})
simp_rw₉ : inst = generateFrom ((fun (a : Set α) ↦ a) '' {U : Set α | IsOpen[inst] U})
simp_rw₁₀ : inst = generateFrom {U : Set α | IsOpen[inst] U}
⊢ inst = induced (fun (x : α) ↦ {x}) (TopologicalSpace.vietoris α)

Tactic:
simp_rw [TopologicalSpace.vietoris, induced_generateFrom_eq, image_union, image_image,
      powerset, preimage_setOf_eq, singleton_subset_iff, singleton_inter_nonempty, union_self,
      setOf_mem_eq, image_id', generateFrom_setOf_isOpen]

Premises used: Set.singleton_subset_iff, Set.image_image, Set.image_id', TopologicalSpace.vietoris, Set.powerset, TopologicalSpace.generateFrom_setOf_isOpen, Set.setOf_mem_eq, Set.preimage_setOf_eq, induced_generateFrom_eq, Set.union_self, Set.singleton_inter_nonempty, Set.image_union
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Continuous[inst, TopologicalSpace.vietoris α] fun (x : α) ↦ {x}

Tactic:
isEmbedding_singleton.continuous

Premises used: TopologicalSpace.vietoris.isEmbedding_singleton, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
rw : ∀ (x : Set α), Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ x → (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 x
⊢ IsClosed[t] (range fun (x : α) ↦ {x})

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds, isOpen_compl_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
inl :
  ∀ (hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ ∅),
    Membership.mem (γ := Filter (Set α)) (𝓝 ∅) (range fun (x : α) ↦ {x})ᶜ
inr : ∀ (h : s.Nonempty), (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s

Tactic:
rcases Set.eq_empty_or_nonempty s with rfl | h

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ ∅
inl : Membership.mem (γ := Filter (Set α)) (pure ∅) (range fun (x : α) ↦ {x})ᶜ
inl₁ inl₂ inl₃ inl₄ : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ ∅
⊢ Membership.mem (γ := Filter (Set α)) (𝓝 ∅) (range fun (x : α) ↦ {x})ᶜ

Tactic:
rwa [(isOpen_singleton_iff_nhds_eq_pure _).mp h₁, Filter.mem_pure]

Premises used: isOpen_singleton_iff_nhds_eq_pure, Iff.mp, Filter.mem_pure
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
inr :
  ∀ (x : α) (hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ {x}) (h : Set.Nonempty (α := α) {x}),
    Membership.mem (γ := Filter (Set α)) (𝓝 {x}) (range fun (x : α) ↦ {x})ᶜ
inr₁ : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : x ≠ y), (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s

Tactic:
rcases h.exists_eq_singleton_or_nontrivial with ⟨x, rfl⟩ | ⟨x, hx, y, hy, hxy⟩

Premises used: Set.Nonempty.exists_eq_singleton_or_nontrivial, rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
x : α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ {x}
h : Set.Nonempty (α := α) {x}
⊢ Membership.mem (γ := Filter (Set α)) (𝓝 {x}) (range fun (x : α) ↦ {x})ᶜ

Tactic:
cases hs <| Set.mem_range_self x

Premises used: Set.mem_range_self
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
inr :
  ∀ (U V : Set α) (hU : IsOpen[inst] U) (hV : IsOpen[inst] V) (hxU : x ∈ U) (hyV : y ∈ V) (hUV : Disjoint U V),
    (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s

Tactic:
obtain ⟨U, V, hU, hV, hxU, hyV, hUV⟩ := t2_separation hxy

Premises used: t2_separation
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
h₃ :
  ∀ (a : Set α),
    Membership.mem (γ := Set (Set α)) ({s : Set α | (s ∩ U).Nonempty} ∩ {s : Set α | (s ∩ V).Nonempty}) a →
      Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ a
⊢ (range fun (x : α) ↦ {x})ᶜ ∈ 𝓝 s

Tactic:
filter_upwards [(h₂ hU).inter (h₂ hV) |>.mem_nhds ⟨⟨x, hx, hxU⟩, ⟨y, hy, hyV⟩⟩]

Premises used: And.intro, IsOpen.mem_nhds, IsOpen.inter, Exists.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} ((fun (x : α) ↦ ({x} : Set α)) z)
hzV : Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ V).Nonempty} ((fun (x : α) ↦ ({x} : Set α)) z)
⊢ z ∈ U

Tactic:
rw [Set.mem_setOf, Set.singleton_inter_nonempty] at hzU hzV

Premises used: Set.mem_setOf, Set.singleton_inter_nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ U).Nonempty} ((fun (x : α) ↦ ({x} : Set α)) z)
hzV : Membership.mem (γ := Set (Set α)) {s : Set α | (s ∩ V).Nonempty} ((fun (x : α) ↦ ({x} : Set α)) z)
hzU₁ : z ∈ U
⊢ z ∈ V

Tactic:
rw [Set.mem_setOf, Set.singleton_inter_nonempty] at hzU hzV

Premises used: Set.mem_setOf, Set.singleton_inter_nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : z ∈ U
hzV : z ∈ V
⊢ False

Tactic:
hUV.notMem_of_mem_left hzU hzV

Premises used: Disjoint.notMem_of_mem_left
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
t : TopologicalSpace (Set α)
h₁ : IsOpen[t] {∅}
h₂ : ∀ {U : Set α}, IsOpen[inst] U → IsOpen[t] {s : Set α | (s ∩ U).Nonempty}
s : Set α
hs : Membership.mem (γ := Set (Set α)) (range fun (x : α) ↦ {x})ᶜ s
h : s.Nonempty
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hxU : x ∈ U
hyV : y ∈ V
hUV : Disjoint U V
z : α
hzU : z ∈ U
hzV : z ∈ V
⊢ False

Tactic:
exact hUV.notMem_of_mem_left hzU hzV

Premises used: Disjoint.notMem_of_mem_left
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
simp_rw :
  (∀ (U : Set α),
      IsOpen[inst] U →
        IsOpen[instTopologicalSpaceProd] ({a : Set α × Set α | a.1 ⊆ U} ∩ {a : Set α × Set α | a.2 ⊆ U})) ∧
    ∀ (F : Set α),
      IsClosed[inst] F →
        IsClosed[instTopologicalSpaceProd] ({a : Set α × Set α | a.1 ⊆ F} ∩ {a : Set α × Set α | a.2 ⊆ F})
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.vietoris α] fun (x : Set α × Set α) ↦ x.1 ∪ x.2

Tactic:
simp_rw [continuous_iff, powerset, preimage_setOf_eq, union_subset_iff, setOf_and]

Premises used: Set.setOf_and, Set.union_subset_iff, Set.powerset, Set.preimage_setOf_eq, TopologicalSpace.vietoris.continuous_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ (∀ (U : Set α),
      IsOpen[inst] U →
        IsOpen[instTopologicalSpaceProd] ({a : Set α × Set α | a.1 ⊆ U} ∩ {a : Set α × Set α | a.2 ⊆ U})) ∧
    ∀ (F : Set α),
      IsClosed[inst] F →
        IsClosed[instTopologicalSpaceProd] ({a : Set α × Set α | a.1 ⊆ F} ∩ {a : Set α × Set α | a.2 ⊆ F})

Tactic:
⟨
    fun U hU => .inter
      (hU.powerset_vietoris.preimage continuous_fst)
      (hU.powerset_vietoris.preimage continuous_snd),
    fun F hF => .inter
      (hF.powerset_vietoris.preimage continuous_fst)
      (hF.powerset_vietoris.preimage continuous_snd)⟩

Premises used: continuous_snd, continuous_fst, IsOpen.powerset_vietoris, And.intro, IsOpen.inter, IsClosed.powerset_vietoris, IsClosed.preimage, IsClosed.inter, IsOpen.preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ (∀ (U : Set α),
      IsOpen[inst] U →
        IsOpen[instTopologicalSpaceProd] ({a : Set α × Set α | a.1 ⊆ U} ∩ {a : Set α × Set α | a.2 ⊆ U})) ∧
    ∀ (F : Set α),
      IsClosed[inst] F →
        IsClosed[instTopologicalSpaceProd] ({a : Set α × Set α | a.1 ⊆ F} ∩ {a : Set α × Set α | a.2 ⊆ F})

Tactic:
exact ⟨
    fun U hU => .inter
      (hU.powerset_vietoris.preimage continuous_fst)
      (hU.powerset_vietoris.preimage continuous_snd),
    fun F hF => .inter
      (hF.powerset_vietoris.preimage continuous_fst)
      (hF.powerset_vietoris.preimage continuous_snd)⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
inst_1 : Finite ι
simp_rw :
  (∀ (U : Set α), IsOpen[inst] U → IsOpen[Pi.topologicalSpace] (⋂ (i : ι), {x : ι → α | x i ∈ U})) ∧
    ∀ (F : Set α), IsClosed[inst] F → IsClosed[Pi.topologicalSpace] (⋂ (i : ι), {x : ι → α | x i ∈ F})
⊢ Continuous[Pi.topologicalSpace, TopologicalSpace.vietoris α] range

Tactic:
simp_rw [continuous_iff, powerset, preimage_setOf_eq, range_subset_iff, setOf_forall]

Premises used: Set.powerset, Set.preimage_setOf_eq, Set.range_subset_iff, Set.setOf_forall, TopologicalSpace.vietoris.continuous_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
inst_1 : Finite ι
⊢ (∀ (U : Set α), IsOpen[inst] U → IsOpen[Pi.topologicalSpace] (⋂ (i : ι), {x : ι → α | x i ∈ U})) ∧
    ∀ (F : Set α), IsClosed[inst] F → IsClosed[Pi.topologicalSpace] (⋂ (i : ι), {x : ι → α | x i ∈ F})

Tactic:
⟨
    fun U hU => isOpen_iInter_of_finite fun i => hU.preimage <| continuous_apply i,
    fun F hF => isClosed_iInter fun i => hF.preimage <| continuous_apply i⟩

Premises used: isOpen_iInter_of_finite, And.intro, continuous_apply, IsClosed.preimage, IsOpen.preimage, isClosed_iInter
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
inst_1 : Finite ι
⊢ (∀ (U : Set α), IsOpen[inst] U → IsOpen[Pi.topologicalSpace] (⋂ (i : ι), {x : ι → α | x i ∈ U})) ∧
    ∀ (F : Set α), IsClosed[inst] F → IsClosed[Pi.topologicalSpace] (⋂ (i : ι), {x : ι → α | x i ∈ F})

Tactic:
exact ⟨
    fun U hU => isOpen_iInter_of_finite fun i => hU.preimage <| continuous_apply i,
    fun F hF => isClosed_iInter fun i => hF.preimage <| continuous_apply i⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
simp_rw :
  (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' F}
⊢ Continuous[TopologicalSpace.vietoris α, TopologicalSpace.vietoris β] fun (x : Set α) ↦ f '' x

Tactic:
simp_rw [continuous_iff, powerset, preimage_setOf_eq, image_subset_iff]

Premises used: Set.powerset, Set.preimage_setOf_eq, Set.image_subset_iff, TopologicalSpace.vietoris.continuous_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
left : ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}
right : ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' F}
⊢ (∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}) ∧
    ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' F}

Tactic:
constructor
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
⊢ ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}

Tactic:
fun U hU => (hU.preimage hf).powerset_vietoris

Premises used: Set.powerset, IsOpen.powerset_vietoris, IsOpen.preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
⊢ ∀ (U : Set β), IsOpen[inst_1] U → IsOpen[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' U}

Tactic:
exact fun U hU => (hU.preimage hf).powerset_vietoris
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
⊢ ∀ (F : Set β), IsClosed[inst_1] F → IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ f ⁻¹' F}

Tactic:
fun U hU => (hU.preimage hf).powerset_vietoris

Premises used: Set.powerset, IsClosed.powerset_vietoris, IsClosed.preimage