awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
⊢ Eq.{u_2 + 1} (α := Set Y)
    (⋃ (i : Opens X), ⋃ (x : i ∈ Us), ⋃ (_ : Subtype.mk (p := fun (x : Opens X) ↦ x ∈ Us) i ⋯ ∈ t), f '' (↑i : Set X))
    (⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X))

Tactic:
simp
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
⊢ ⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X) = U

Tactic:
subset_antisymm (fun x ↦ ?_) ht

Premises used: subset_antisymm
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
refine_2 : ∀ (x : Y), Membership.mem (γ := Set Y) (⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X)) x → x ∈ U
⊢ ⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X) = U

Tactic:
refine subset_antisymm (fun x ↦ ?_) ht

Premises used: subset_antisymm
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
x : Y
refine_2 : (∃ (i : (↑Us : Type u_1)) (_ : i ∈ t), x ∈ f '' (↑(↑i : Opens X) : Set X)) → x ∈ U
⊢ Membership.mem (γ := Set Y) (⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X)) x → x ∈ U

Tactic:
simp_rw [Set.mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
i : (↑Us : Type u_1)
hi : i ∈ t
x : X
hx : x ∈ (↑(↑i : Opens X) : Set X)
⊢ x ∈ { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X }

Tactic:
have := heq ▸ mem_sSup.mpr ⟨i.1, i.2, hx⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
i : (↑Us : Type u_1)
hi : i ∈ t
x : X
hx : x ∈ (↑(↑i : Opens X) : Set X)
this : x ∈ { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X }
⊢ f x ∈ U

Tactic:
this

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PrespectralSpace X
f : X → Y
hfc : Continuous[inst, inst_1] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst_1] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U : Opens X | IsCompact (↑U : Set X)}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X } = sSup Us
t : Finset (↑Us : Type u_1)
ht : U ⊆ ⋃ i ∈ t, (fun (s : (↑Us : Type u_1)) ↦ f '' (↑(↑s : Opens X) : Set X)) i
i : (↑Us : Type u_1)
hi : i ∈ t
x : X
hx : x ∈ (↑(↑i : Opens X) : Set X)
this : x ∈ { carrier := f ⁻¹' U, is_open' := ⋯ : Opens X }
⊢ f x ∈ U

Tactic:
exact this
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
⊢ IsCompact.{u_1} (X := X) ∅ ∧ IsOpen[inst] ∅ ∧ Subset.{u_1} (α := Set X) ∅ ∅ ∧ ∅ ⊆ U

Tactic:
simp
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
refine_1 :
  ∀ (s t : Set X) (hst : s ⊆ t),
    (∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U) →
      ∀ (W : Set X) (Wc : IsCompact W) (Wo : IsOpen[inst] W) (hKW : t ⊆ W) (hWU : W ⊆ U),
        ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ⊆ W ∧ W ⊆ U
refine_2 :
  ∀ ⦃s t : Set X⦄,
    (∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ⊆ W ∧ W ⊆ U) →
      (∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U) →
        ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ∪ t ⊆ W ∧ W ⊆ U
refine_3 : ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U
⊢ ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ K ⊆ W ∧ W ⊆ U

Tactic:
refine hK.induction_on ⟨∅, by simp⟩ (fun s t hst ⟨W, Wc, Wo, hKW, hWU⟩ ↦ ?_) ?_ ?_
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
s t : Set X
hst : s ⊆ t
h : ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U
W : Set X
Wc : IsCompact W
Wo : IsOpen[inst] W
hKW : t ⊆ W
hWU : W ⊆ U
w : Set X
left : IsCompact W
left₁ : IsOpen[inst] W
left₂ : s ⊆ W
right : W ⊆ U
⊢ ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ⊆ W ∧ W ⊆ U

Tactic:
use W, Wc, Wo, subset_trans hst hKW, hWU

Premises used: subset_trans
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
s t : Set X
refine_2 :
  ∀ (W₁ : Set X) (Wc₁ : IsCompact W₁) (Wo₁ : IsOpen[inst] W₁) (hKW₁ : s ⊆ W₁) (hWU₁ : W₁ ⊆ U),
    (∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U) →
      ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ∪ t ⊆ W ∧ W ⊆ U
⊢ (∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ⊆ W ∧ W ⊆ U) →
    (∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U) →
      ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ∪ t ⊆ W ∧ W ⊆ U

Tactic:
⟨W₁, Wc₁, Wo₁, hKW₁, hWU₁⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
s t W₁ : Set X
Wc₁ : IsCompact W₁
Wo₁ : IsOpen[inst] W₁
hKW₁ : s ⊆ W₁
hWU₁ : W₁ ⊆ U
refine_2 :
  ∀ (W₂ : Set X) (Wc₂ : IsCompact W₂) (Wo₂ : IsOpen[inst] W₂) (hKW₂ : t ⊆ W₂) (hWU₂ : W₂ ⊆ U),
    ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ∪ t ⊆ W ∧ W ⊆ U
⊢ (∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U) →
    ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ∪ t ⊆ W ∧ W ⊆ U

Tactic:
⟨W₂, Wc₂, Wo₂, hKW₂, hWU₂⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
s t W₁ : Set X
Wc₁ : IsCompact W₁
Wo₁ : IsOpen[inst] W₁
hKW₁ : s ⊆ W₁
hWU₁ : W₁ ⊆ U
W₂ : Set X
Wc₂ : IsCompact W₂
Wo₂ : IsOpen[inst] W₂
hKW₂ : t ⊆ W₂
hWU₂ : W₂ ⊆ U
⊢ ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ∪ t ⊆ W ∧ W ⊆ U

Tactic:
⟨W₁ ∪ W₂, Wc₁.union Wc₂, Wo₁.union Wo₂, Set.union_subset_union hKW₁ hKW₂,
      Set.union_subset hWU₁ hWU₂⟩

Premises used: Set.union_subset_union, Set.union_subset, IsOpen.union, And.intro, Exists.intro, IsCompact.union, Union.union
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
s t W₁ : Set X
Wc₁ : IsCompact W₁
Wo₁ : IsOpen[inst] W₁
hKW₁ : s ⊆ W₁
hWU₁ : W₁ ⊆ U
W₂ : Set X
Wc₂ : IsCompact W₂
Wo₂ : IsOpen[inst] W₂
hKW₂ : t ⊆ W₂
hWU₂ : W₂ ⊆ U
⊢ ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ∪ t ⊆ W ∧ W ⊆ U

Tactic:
exact ⟨W₁ ∪ W₂, Wc₁.union Wc₂, Wo₁.union Wo₂, Set.union_subset_union hKW₁ hKW₂,
      Set.union_subset hWU₁ hWU₂⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
x : X
hx : x ∈ K
refine_3 :
  ∀ (V : Set X) (h : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} V) (hxV : x ∈ V)
    (hVU : V ⊆ U), ∃ t ∈ 𝓝[K] x, ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U

Tactic:
obtain ⟨V, h, hxV, hVU⟩ :=
      PrespectralSpace.isTopologicalBasis.exists_subset_of_mem_open (hKU hx) hU

Premises used: PrespectralSpace.isTopologicalBasis, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
x : X
hx : x ∈ K
V : Set X
h : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} V
hxV : x ∈ V
hVU : V ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U

Tactic:
⟨V, mem_nhdsWithin.mpr ⟨V, h.1, hxV, Set.inter_subset_left⟩, V, h.2, h.1, subset_rfl, hVU⟩

Premises used: Iff.mpr, Set.inter_subset_left, mem_nhdsWithin, And.right, And.left, And.intro, Exists.intro, subset_rfl
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst] U
hKU : K ⊆ U
x : X
hx : x ∈ K
V : Set X
h : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} V
hxV : x ∈ V
hVU : V ⊆ U
⊢ ∃ t ∈ 𝓝[K] x, ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U

Tactic:
exact ⟨V, mem_nhdsWithin.mpr ⟨V, h.1, hxV, Set.inter_subset_left⟩, V, h.2, h.1, subset_rfl, hVU⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z : Set X
hZ : ¬IsPreirreducible Z
⊢ ∃ (x : Set X) (x_1 : Set X) (_ : IsOpen[inst] x) (_ : IsOpen[inst] x_1) (_ : (Z ∩ x).Nonempty) (_ :
    (Z ∩ x_1).Nonempty), ¬(Z ∩ (x ∩ x_1)).Nonempty

Tactic:
simp only [IsPreirreducible, not_forall] at hZ

Premises used: IsPreirreducible, Classical.not_forall
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z : Set X
hZ :
  ∃ (x : Set X) (x_1 : Set X) (_ : IsOpen[inst] x) (_ : IsOpen[inst] x_1) (_ : (Z ∩ x).Nonempty) (_ :
    (Z ∩ x_1).Nonempty), ¬(Z ∩ (x ∩ x_1)).Nonempty
rcases :
  ∀ (U₁ U₂ : Set X) (hU₁ : IsOpen[inst] U₁) (hU₂ : IsOpen[inst] U₂) (hU₁Z : (Z ∩ U₁).Nonempty)
    (hU₂Z : (Z ∩ U₂).Nonempty) (hU₁₂ : ¬(Z ∩ (U₁ ∩ U₂)).Nonempty),
    ∃ (A : Set X) (B : Set X),
      IsClosed[inst] A ∧
        IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
⊢ ∃ (A : Set X) (B : Set X),
    IsClosed[inst] A ∧
      IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
rcases hZ with ⟨U₁, U₂, hU₁, hU₂, hU₁Z, hU₂Z, hU₁₂⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : ¬(Z ∩ (U₁ ∩ U₂)).Nonempty
⊢ Z ∩ (U₁ ∩ U₂) ⊆ ∅

Tactic:
rw [Set.not_nonempty_iff_eq_empty, ← Set.subset_empty_iff] at hU₁₂

Premises used: Set.not_nonempty_iff_eq_empty, Set.subset_empty_iff
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
obtain : ∀ (x : X) (hx : x ∈ Z ∩ U₁), ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂
⊢ ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂

Tactic:
obtain ⟨x, hx⟩ := hU₁Z
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x : X
hx : x ∈ Z ∩ U₁
w : X
left : x ∈ U₁
left₁ : x ∈ Z
right : x ∉ U₂
⊢ ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂

Tactic:
use x, hx.2, hx.1, fun h₂ ↦ hU₁₂ ⟨hx.1, hx.2, h₂⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
obtain :
  ∀ (x₁ : X) (hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂),
    ∃ (A : Set X) (B : Set X),
      IsClosed[inst] A ∧
        IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
⊢ ∃ (A : Set X) (B : Set X),
    IsClosed[inst] A ∧
      IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
obtain ⟨x₁, hx₁⟩ : ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂ := by
    obtain ⟨x, hx⟩ := hU₁Z
    use x, hx.2, hx.1, fun h₂ ↦ hU₁₂ ⟨hx.1, hx.2, h₂⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
obtain : ∀ (x : X) (hx : x ∈ Z ∩ U₂), ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁
⊢ ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁

Tactic:
obtain ⟨x, hx⟩ := hU₂Z
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x : X
hx : x ∈ Z ∩ U₂
w : X
left : x ∈ U₂
left₁ : x ∈ Z
right : x ∉ U₁
⊢ ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁

Tactic:
use x, hx.2, hx.1, fun h₁ ↦ hU₁₂ ⟨hx.1, h₁, hx.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
obtain :
  ∀ (x₂ : X) (hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁),
    ∃ (A : Set X) (B : Set X),
      IsClosed[inst] A ∧
        IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
⊢ ∃ (A : Set X) (B : Set X),
    IsClosed[inst] A ∧
      IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
obtain ⟨x₂, hx₂⟩ : ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁ := by
    obtain ⟨x, hx⟩ := hU₂Z
    use x, hx.2, hx.1, fun h₁ ↦ hU₁₂ ⟨hx.1, h₁, hx.2⟩
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst] U₁
hU₂ : IsOpen[inst] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
rw :
  ∀
    (hU₁ :
      ∀ a ∈ U₁,
        ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₁)
    (hU₂ :
      ∀ a ∈ U₂,
        ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₂)
    (hU₁Z : (Z ∩ U₁).Nonempty) (hU₂Z : (Z ∩ U₂).Nonempty) (hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅) (x₁ : X)
    (hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂) (x₂ : X) (hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁),
    ∃ (A : Set X) (B : Set X),
      IsClosed[inst] A ∧
        IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
⊢ ∃ (A : Set X) (B : Set X),
    IsClosed[inst] A ∧
      IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
rw [PrespectralSpace.isTopologicalBasis.isOpen_iff] at hU₁ hU₂

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, PrespectralSpace.isTopologicalBasis
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ :
  ∀ a ∈ U₁,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₁
hU₂ :
  ∀ a ∈ U₂,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
obtain :
  ∀ (W₁ : Set X)
    (hW₁ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₁ ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁),
    ∃ (A : Set X) (B : Set X),
      IsClosed[inst] A ∧
        IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
⊢ ∃ (A : Set X) (B : Set X),
    IsClosed[inst] A ∧
      IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
obtain ⟨W₁, hW₁⟩ := hU₁ x₁ hx₁.1

Premises used: And.left
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ :
  ∀ a ∈ U₁,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₁
hU₂ :
  ∀ a ∈ U₂,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₁ ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
obtain :
  ∀ (W₂ : Set X)
    (hW₂ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₂ ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂),
    ∃ (A : Set X) (B : Set X),
      IsClosed[inst] A ∧
        IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
⊢ ∃ (A : Set X) (B : Set X),
    IsClosed[inst] A ∧
      IsClosed[inst] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
obtain ⟨W₂, hW₂⟩ := hU₂ x₂ hx₂.1

Premises used: And.left
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ :
  ∀ a ∈ U₁,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₁
hU₂ :
  ∀ a ∈ U₂,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₁ ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₂ ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ IsClosed[inst] W₁ᶜ

Tactic:
simpa using hW₁.1.1

Premises used: And.left
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ :
  ∀ a ∈ U₁,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₁
hU₂ :
  ∀ a ∈ U₂,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₁ ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₂ ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ IsClosed[inst] W₂ᶜ

Tactic:
simpa using hW₂.1.1

Premises used: And.left
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ :
  ∀ a ∈ U₁,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₁
hU₂ :
  ∀ a ∈ U₂,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₁ ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₂ ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ IsCompact W₁ᶜᶜ

Tactic:
simp [hW₁.1.2]

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ :
  ∀ a ∈ U₁,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₁
hU₂ :
  ∀ a ∈ U₂,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₁ ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₂ ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ IsCompact W₂ᶜᶜ

Tactic:
simp [hW₂.1.2]

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Spectral.Prespectral
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ :
  ∀ a ∈ U₁,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₁
hU₂ :
  ∀ a ∈ U₂,
    ∃ (t : Set X), Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} t ∧ a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₁ ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : Membership.mem (γ := Set (Set X)) {U : Set X | IsOpen[inst] U ∧ IsCompact U} W₂ ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ x₁ ∈ Z ∩ W₁ᶜᶜ

Tactic:
grind