awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsInducing f
⊢ IsInducing (Compacts.map f ⋯)

Tactic:
isEmbedding_coe.isInducing.of_comp_iff.mp <| hf.image_vietoris.comp isEmbedding_coe.isInducing

Premises used: TopologicalSpace.Compacts.isEmbedding_coe, Topology.IsInducing.comp, Topology.IsInducing.of_comp_iff, Topology.IsEmbedding.isInducing, Topology.IsInducing.image_vietoris, Iff.mp
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsEmbedding f
⊢ IsEmbedding (Compacts.map f ⋯)

Tactic:
isEmbedding_coe.of_comp_iff.mp <| hf.image_vietoris.comp isEmbedding_coe

Premises used: TopologicalSpace.Compacts.isEmbedding_coe, Topology.IsEmbedding.image_vietoris, Topology.IsEmbedding.comp, Iff.mp, Topology.IsEmbedding.of_comp_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : DiscreteTopology α
rw : ∀ (a : Compacts α), IsOpen (X := Compacts α) {a}
⊢ DiscreteTopology.{u_1} (Compacts α)

Tactic:
rw [discreteTopology_iff_isOpen_singleton]

Premises used: discreteTopology_iff_isOpen_singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : DiscreteTopology α
K : Compacts α
⊢ IsOpen.{u_1} (X := Compacts α)
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})

Tactic:
(isOpen_subsets_of_isOpen (isOpen_discrete (K : Set α))).inter
      (K.isCompact.finite_of_discrete.isOpen_biInter fun x hx =>
        isOpen_inter_nonempty_of_isOpen (isOpen_discrete { x }))

Premises used: TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen, SetLike.coe, TopologicalSpace.Compacts.isCompact, isOpen_discrete, IsOpen.inter, IsCompact.finite_of_discrete, TopologicalSpace.Compacts.isOpen_subsets_of_isOpen, Set.Finite.isOpen_biInter, Singleton.singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : DiscreteTopology α
K : Compacts α
h :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})
⊢ IsOpen (X := Compacts α) {K}

Tactic:
convert!
    (isOpen_subsets_of_isOpen (isOpen_discrete (K : Set α))).inter
      (K.isCompact.finite_of_discrete.isOpen_biInter fun x hx =>
        isOpen_inter_nonempty_of_isOpen (isOpen_discrete { x }))

Premises used: TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen, SetLike.coe, TopologicalSpace.Compacts.isCompact, isOpen_discrete, IsOpen.inter, IsCompact.finite_of_discrete, TopologicalSpace.Compacts.isOpen_subsets_of_isOpen, Set.Finite.isOpen_biInter, Singleton.singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : DiscreteTopology α
K : Compacts α
h :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), ((↑x : Set α) ∩ {i}).Nonempty})
h₁ :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), i ∈ (↑x : Set α)})
h₂ :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩ {x : Compacts α | (↑K : Set α) ⊆ (↑x : Set α)})
h₃ : Eq (α := Set (Compacts α)) {K} {a : Compacts α | (↑a : Set α) ⊆ (↑K : Set α) ∧ (↑K : Set α) ⊆ (↑a : Set α)}
h₄ : Eq (α := Set (Compacts α)) {K} {a : Compacts α | (↑a : Set α) = (↑K : Set α)}
h₅ : Eq (α := Set (Compacts α)) {K} {a : Compacts α | a = K}
⊢ Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})

Tactic:
simp_rw [← setOf_forall, inter_singleton_nonempty, ← Set.subset_def, ← setOf_and,
    ← subset_antisymm_iff, SetLike.coe_set_eq, setOf_eq_eq_singleton]

Premises used: Set.setOf_eq_eq_singleton, Set.setOf_and, Set.subset_def, subset_antisymm_iff, SetLike.coe_set_eq, Set.setOf_forall, Set.inter_singleton_nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ DiscreteTopology.{u_1} (Compacts α) ↔ DiscreteTopology α

Tactic:
⟨fun _ => isEmbedding_singleton.discreteTopology, fun _ => inferInstance⟩

Premises used: inferInstance, Topology.IsEmbedding.discreteTopology, Iff.intro, TopologicalSpace.Compacts.isEmbedding_singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T1Space α
⊢ T0Space.{u_1} (Compacts α)

Tactic:
isEmbedding_coe.t0Space

Premises used: TopologicalSpace.Compacts.isEmbedding_coe, Topology.IsEmbedding.t0Space
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
inr :
  ∀
    (this :
      ∀ (K₁ K₂ : Compacts α) (h : K₁ ≠ K₂) (h' : ¬K₁ ≤ K₂),
        (fun (x y : Compacts α) ↦
            ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
          K₁ K₂)
    (h' : ¬¬K₁ ≤ K₂),
    ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
wlog :
  ∀ (K₁ K₂ : Compacts α) (h : K₁ ≠ K₂) (h' : ¬K₁ ≤ K₂),
    ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

Tactic:
wlog h' : ¬(K₁ ≤ K₂) generalizing K₁ K₂

Premises used: LE.le
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
this :
  ∀ (K₁ K₂ : Compacts α) (h : K₁ ≠ K₂) (h' : ¬K₁ ≤ K₂),
    (fun (x y : Compacts α) ↦
        ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v)
      K₁ K₂
h' : ¬¬K₁ ≤ K₂
⊢ ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

Tactic:
grind [Disjoint.symm, le_antisymm]

Premises used: le_antisymm, Disjoint.symm
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
h' : ¬K₁ ≤ K₂
⊢ ∃ x ∈ K₁, x ∉ K₂

Tactic:
rw [SetLike.not_le_iff_exists] at h'

Premises used: SetLike.not_le_iff_exists
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
h' : ∃ x ∈ K₁, x ∉ K₂
obtain :
  ∀ (x : α) (hx₁ : x ∈ K₁) (hx₂ : x ∉ K₂),
    ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := h'
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
x : α
hx₁ : x ∈ K₁
hx₂ : x ∉ K₂
obtain :
  ∀ (U V : Set α) (hU : IsOpen[inst] U) (hV : IsOpen[inst] V) (hU' : (↑K₂ : Set α) ⊆ U) (hV' : x ∈ V)
    (hUV : Disjoint U V),
    ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

Tactic:
obtain ⟨U, V, hU, hV, hU', hV', hUV⟩ := K₂.isCompact.separation_of_notMem hx₂

Premises used: IsCompact.separation_of_notMem, TopologicalSpace.Compacts.isCompact
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
x : α
hx₁ : x ∈ K₁
hx₂ : x ∉ K₂
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hU' : (↑K₂ : Set α) ⊆ U
hV' : x ∈ V
hUV : Disjoint U V
⊢ Disjoint.{u_1} (α := Set (Compacts α)) {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty}
    {K : Compacts α | (↑K : Set α) ⊆ U}

Tactic:
grind [Set.Nonempty]

Premises used: Set.Nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : T2Space α
K₁ K₂ : Compacts α
h : K₁ ≠ K₂
x : α
hx₁ : x ∈ K₁
hx₂ : x ∉ K₂
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
hU' : (↑K₂ : Set α) ⊆ U
hV' : x ∈ V
hUV : Disjoint U V
⊢ ∃ (u : Set (Compacts α)) (v : Set (Compacts α)), IsOpen u ∧ IsOpen v ∧ K₁ ∈ u ∧ K₂ ∈ v ∧ Disjoint u v

Tactic:
exact ⟨_, _, isOpen_inter_nonempty_of_isOpen hV, isOpen_subsets_of_isOpen hU, ⟨x, hx₁, hV'⟩,
      hU', by grind [Set.Nonempty]⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ T2Space.{u_1} (Compacts α) ↔ T2Space α

Tactic:
⟨fun _ => isEmbedding_singleton.t2Space, fun _ => inferInstance⟩

Premises used: inferInstance, Iff.intro, TopologicalSpace.Compacts.isEmbedding_singleton, Topology.IsEmbedding.t2Space
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
simp_rw :
  ∀ (t : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (a : Set α) ↦ {a_1 : Compacts α | (↑a_1 : Set α) ⊆ a}) '' {U : Set α | IsOpen[inst] U} ∪
          (fun (a : Set α) ↦ {a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty}) '' {U : Set α | IsOpen[inst] U})
        t →
      ∀ a ∈ t, ∃ s ∈ 𝓝ˢ tᶜ, ∃ t ∈ 𝓝 a, Disjoint s t
⊢ RegularSpace.{u_1} (Compacts α)

Tactic:
simp_rw [regularSpace_generateFrom induced_generateFrom_eq, image_union, image_image, powerset,
    preimage_setOf_eq, Filter.disjoint_iff]

Premises used: Set.image_image, Set.powerset, Filter.disjoint_iff, Set.preimage_setOf_eq, induced_generateFrom_eq, regularSpace_generateFrom, Set.image_union
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U) K
inl :
  ∀ (V W : Set α) (hV : IsOpen[inst] V) (hW : IsOpen[inst] W) (hKV : (↑K : Set α) ⊆ V) (hUW : Uᶜ ⊆ W)
    (hVW : Disjoint V W),
    ∃ (s : Set (Compacts α)),
      Membership.mem (γ := Filter (Compacts α))
          (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ) s ∧
        ∃ t ∈ 𝓝 K, Disjoint s t
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t

Tactic:
obtain ⟨V, W, hV, hW, hKV, hUW, hVW⟩ :=
      SeparatedNhds.of_isCompact_isClosed K.isCompact hU.isClosed_compl
        (disjoint_compl_right_iff_subset.mpr hK)

Premises used: Iff.mpr, SeparatedNhds.of_isCompact_isClosed, Set.disjoint_compl_right_iff_subset, IsOpen.isClosed_compl, TopologicalSpace.Compacts.isCompact
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U) K
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hKV : (↑K : Set α) ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Disjoint.{u_1} (α := Set (Compacts α)) {K : Compacts α | ((↑K : Set α) ∩ W).Nonempty}
    {K : Compacts α | (↑K : Set α) ⊆ V}

Tactic:
grind [Set.Nonempty]

Premises used: Set.Nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U) K
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hKV : (↑K : Set α) ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
inl :
  Membership.mem (γ := Filter (Compacts α))
    (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ)
    {K : Compacts α | ((↑K : Set α) ∩ W).Nonempty}
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t

Tactic:
refine ⟨{K | (↑K ∩ W).Nonempty}, ?_, {K | ↑K ⊆ V},
      (isOpen_subsets_of_isOpen hV).mem_nhds_iff.mpr hKV, by grind [Set.Nonempty]⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U) K
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hKV : (↑K : Set α) ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
inl :
  Subset.{u_1} (α := Set (Compacts α)) {a : Compacts α | ((↑a : Set α) ∩ Uᶜ).Nonempty}
    {K : Compacts α | ((↑K : Set α) ∩ W).Nonempty}
⊢ Membership.mem (γ := Filter (Compacts α))
    (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U)ᶜ)
    {K : Compacts α | ((↑K : Set α) ∩ W).Nonempty}

Tactic:
simp_rw [(isOpen_inter_nonempty_of_isOpen hW).mem_nhdsSet, compl_setOf,
      ← inter_compl_nonempty_iff]

Premises used: TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen, Set.inter_compl_nonempty_iff, Set.compl_setOf, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | (↑a_1 : Set α) ⊆ a} : Set (Compacts α))) U) K
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hKV : (↑K : Set α) ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
inl inl₁ :
  Subset.{u_1} (α := Set (Compacts α)) {a : Compacts α | ((↑a : Set α) ∩ W).Nonempty}
    {a : Compacts α | ((↑a : Set α) ∩ W).Nonempty}
⊢ Subset.{u_1} (α := Set (Compacts α)) {a : Compacts α | ((↑a : Set α) ∩ Uᶜ).Nonempty}
    {K : Compacts α | ((↑K : Set α) ∩ W).Nonempty}

Tactic:
grw [hUW]
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
hK :
  Membership.mem (γ := Set (Compacts α))
    ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U) K
inr :
  ∀ (x : α) (hx₁ : x ∈ (↑K : Set α)) (hx₂ : x ∈ U),
    ∃ (s : Set (Compacts α)),
      Membership.mem (γ := Filter (Compacts α))
          (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
        ∃ t ∈ 𝓝 K, Disjoint s t
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := hK
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
⊢ Disjoint {x} Uᶜ

Tactic:
simpa
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
inr :
  ∀ (V W : Set α) (hV : IsOpen[inst] V) (hW : IsOpen[inst] W) (hxV : {x} ⊆ V) (hUW : Uᶜ ⊆ W) (hVW : Disjoint V W),
    ∃ (s : Set (Compacts α)),
      Membership.mem (γ := Filter (Compacts α))
          (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
        ∃ t ∈ 𝓝 K, Disjoint s t
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t

Tactic:
obtain ⟨V, W, hV, hW, hxV, hUW, hVW⟩ :=
      SeparatedNhds.of_isCompact_isClosed (isCompact_singleton (x := x)) hU.isClosed_compl
        (by simpa)

Premises used: SeparatedNhds.of_isCompact_isClosed, isCompact_singleton, IsOpen.isClosed_compl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Disjoint.{u_1} (α := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ W}
    {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty}

Tactic:
grind [Set.Nonempty]

Premises used: Set.Nonempty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
inr :
  Membership.mem (γ := Filter (Compacts α))
    (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ)
    {K : Compacts α | (↑K : Set α) ⊆ W}
inr₁ : {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty} ∈ 𝓝 K
⊢ ∃ (s : Set (Compacts α)),
    Membership.mem (γ := Filter (Compacts α))
        (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ) s ∧
      ∃ t ∈ 𝓝 K, Disjoint s t

Tactic:
refine ⟨{K | ↑K ⊆ W}, ?_, {K | (↑K ∩ V).Nonempty}, ?_, by grind [Set.Nonempty]⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
inr : Subset.{u_1} (α := Set (Compacts α)) {a : Compacts α | (↑a : Set α) ⊆ Uᶜ} {K : Compacts α | (↑K : Set α) ⊆ W}
⊢ Membership.mem (γ := Filter (Compacts α))
    (𝓝ˢ ((fun (a : Set α) ↦ ({a_1 : Compacts α | ((↑a_1 : Set α) ∩ a).Nonempty} : Set (Compacts α))) U)ᶜ)
    {K : Compacts α | (↑K : Set α) ⊆ W}

Tactic:
simp_rw [(isOpen_subsets_of_isOpen hW).mem_nhdsSet, compl_setOf, not_nonempty_iff_eq_empty,
        ← disjoint_iff_inter_eq_empty, ← subset_compl_iff_disjoint_right]

Premises used: Set.subset_compl_iff_disjoint_right, Set.not_nonempty_iff_eq_empty, Set.disjoint_iff_inter_eq_empty, TopologicalSpace.Compacts.isOpen_subsets_of_isOpen, Set.compl_setOf, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Subset.{u_1} (α := Set (Compacts α)) {a : Compacts α | (↑a : Set α) ⊆ Uᶜ} {K : Compacts α | (↑K : Set α) ⊆ W}

Tactic:
gcongr
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
inr : Membership.mem (γ := Set (Compacts α)) {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty} K
⊢ {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty} ∈ 𝓝 K

Tactic:
rw [(isOpen_inter_nonempty_of_isOpen hV).mem_nhds_iff]

Premises used: TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen, IsOpen.mem_nhds_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Membership.mem (γ := Set (Compacts α)) {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty} K

Tactic:
⟨x, hx₁, hxV <| Set.mem_singleton x⟩

Premises used: Set.mem_singleton, Set.Mem, setOf, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : RegularSpace α
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst] U} U
K : Compacts α
x : α
hx₁ : x ∈ (↑K : Set α)
hx₂ : x ∈ U
V W : Set α
hV : IsOpen[inst] V
hW : IsOpen[inst] W
hxV : {x} ⊆ V
hUW : Uᶜ ⊆ W
hVW : Disjoint V W
⊢ Membership.mem (γ := Set (Compacts α)) {K : Compacts α | ((↑K : Set α) ∩ V).Nonempty} K

Tactic:
exact ⟨x, hx₁, hxV <| Set.mem_singleton x⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ RegularSpace.{u_1} (Compacts α) ↔ RegularSpace α

Tactic:
⟨fun _ => isEmbedding_singleton.regularSpace, fun _ => inferInstance⟩

Premises used: inferInstance, Iff.intro, Topology.IsEmbedding.toIsInducing, Topology.IsInducing.regularSpace, TopologicalSpace.Compacts.isEmbedding_singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ T3Space.{u_1} (Compacts α) ↔ T3Space α

Tactic:
⟨fun _ => isEmbedding_singleton.t3Space, fun _ => inferInstance⟩

Premises used: inferInstance, Topology.IsEmbedding.t3Space, Iff.intro, TopologicalSpace.Compacts.isEmbedding_singleton
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
rw : IsCompact (image (α := Compacts α) SetLike.coe {L : Compacts α | (↑L : Set α) ⊆ K})
⊢ IsCompact.{u_1} (X := Compacts α) {L : Compacts α | (↑L : Set α) ⊆ K}

Tactic:
rw [isEmbedding_coe.isCompact_iff]

Premises used: TopologicalSpace.Compacts.isEmbedding_coe, Topology.IsEmbedding.isCompact_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
K : Set α
hK : IsCompact K
⊢ image (α := Compacts α) SetLike.coe {L : Compacts α | (↑L : Set α) ⊆ K} ⊆ 𝒫 K

Tactic:
grind