awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ IsCompact.{u_1} (X := X) (carrier (⨆ s ∈ t, (↑s : Opens X)))
have refine_1 : IsCompact.{u_1} (X := X) (⋃ i ∈ t, (↑i.1 : Set X))
Tactic: simp only [iSup_mk, carrier_eq_coe, coe_mk]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ f '' (↑(⨆ s ∈ t, (↑s : Opens X)) : Set X) = U
have refine_2 : ⋃ (i : Opens X), ⋃ (x : i ∈ Us), ⋃ (_ : Subtype.mk (p := fun (x : Opens X) ↦ x ∈ Us) i sorry ∈ t), f '' (↑i : Set X) = U
Tactic: simp only [iSup_mk, carrier_eq_coe, Set.iUnion_coe_set, coe_mk, Set.image_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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 : Opens X), ⋃ (x : i ∈ Us), ⋃ (_ : Subtype.mk (p := fun (x : Opens X) ↦ x ∈ Us) i ⋯ ∈ t), f '' (↑i : Set X) = U
have h₁ : Eq.{u_2 + 1} (α := Set Y)
  (⋃ (i : Opens X), ⋃ (x : i ∈ Us), ⋃ (_ : Subtype.mk (p := fun (x : Opens X) ↦ x ∈ Us) i sorry ∈ t), f '' (↑i : Set X))
  (⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X))
Tactic: convert_to ⋃ i ∈ t, f '' i.1 = U
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
h₁ :
  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))
⊢ ⋃ (i : Opens X), ⋃ (x : i ∈ Us), ⋃ (_ : Subtype.mk (p := fun (x : Opens X) ↦ x ∈ Us) i ⋯ ∈ t), f '' (↑i : Set X) = U
have refine_2 : ⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X) = U
Tactic: convert_to ⋃ i ∈ t, f '' i.1 = U
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
have refine_2 : ∀ (x : Y), Membership.mem (γ := Set Y) (⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X)) x → x ∈ U
Tactic: refine subset_antisymm (fun x ↦ ?_) ht
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ Membership.mem (γ := Set Y) (⋃ i ∈ t, f '' (↑(↑i : Opens X) : Set X)) x → x ∈ U
have refine_2 : (∃ (i : (↑Us : Type u_1)) (_ : i ∈ t), x ∈ f '' (↑(↑i : Opens X) : Set X)) → x ∈ U
Tactic: simp_rw [Set.mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (hypothesis)
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)
⊢ f x ∈ U
have this : x ∈ { carrier := f ⁻¹' U, is_open' := sorry : Opens X }
Tactic: have := heq ▸ mem_sSup.mpr ⟨i.1, i.2, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ K ⊆ W ∧ W ⊆ U
have 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
Tactic: refine hK.induction_on ⟨∅, by simp⟩ (fun s t hst ⟨W, Wc, Wo, hKW, hWU⟩ ↦ ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ K ⊆ W ∧ W ⊆ U
have 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
Tactic: refine hK.induction_on ⟨∅, by simp⟩ (fun s t hst ⟨W, Wc, Wo, hKW, hWU⟩ ↦ ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ K ⊆ W ∧ W ⊆ U
have refine_3 : ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U
Tactic: refine hK.induction_on ⟨∅, by simp⟩ (fun s t hst ⟨W, Wc, Wo, hKW, hWU⟩ ↦ ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ⊆ W ∧ W ⊆ U
have left₂ : s ⊆ W
Tactic: use W, Wc, Wo, subset_trans hst hKW, hWU
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ (∃ (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
have 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
Tactic: ⟨W₁, Wc₁, Wo₁, hKW₁, hWU₁⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U) →
    ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ s ∪ t ⊆ W ∧ W ⊆ U
have 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
Tactic: ⟨W₂, Wc₂, Wo₂, hKW₂, hWU₂⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ t ∈ 𝓝[K] x, ∃ (W : Set X), IsCompact W ∧ IsOpen[inst] W ∧ t ⊆ W ∧ W ⊆ U
have 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
Tactic: obtain ⟨V, h, hxV, hVU⟩ :=
      PrespectralSpace.isTopologicalBasis.exists_subset_of_mem_open (hKU hx) hU
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PrespectralSpace X
Z : Set X
hZ : ¬IsPreirreducible Z
⊢ ∃ (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
have 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
Tactic: simp only [IsPreirreducible, not_forall] at hZ
Cleared hypotheses: hZ
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases hZ with ⟨U₁, U₂, hU₁, hU₂, hU₁Z, hU₂Z, hU₁₂⟩
Cleared hypotheses: hZ
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (hypothesis)
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
⊢ ∃ (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
have hU₁₃ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty, ← Set.subset_empty_iff] at hU₁₂
Cleared hypotheses: hU₁₂
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂
have obtain : ∀ (x : X) (hx : x ∈ Z ∩ U₁), ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂
Tactic: obtain ⟨x, hx⟩ := hU₁Z
Cleared hypotheses: hU₁Z
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂
have left : x ∈ U₁
Tactic: use x, hx.2, hx.1, fun h₂ ↦ hU₁₂ ⟨hx.1, hx.2, h₂⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₁
⊢ ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂
have left₁ : x ∈ Z
Tactic: use x, hx.2, hx.1, fun h₂ ↦ hU₁₂ ⟨hx.1, hx.2, h₂⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂
have right : x ∉ U₂
Tactic: use x, hx.2, hx.1, fun h₂ ↦ hU₁₂ ⟨hx.1, hx.2, h₂⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₂) ⊆ ∅
⊢ ∃ (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
have 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
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₂⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁
have obtain : ∀ (x : X) (hx : x ∈ Z ∩ U₂), ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁
Tactic: obtain ⟨x, hx⟩ := hU₂Z
Cleared hypotheses: hU₂Z
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁
have left : x ∈ U₂
Tactic: use x, hx.2, hx.1, fun h₁ ↦ hU₁₂ ⟨hx.1, h₁, hx.2⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₂
⊢ ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁
have left₁ : x ∈ Z
Tactic: use x, hx.2, hx.1, fun h₁ ↦ hU₁₂ ⟨hx.1, h₁, hx.2⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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
⊢ ∃ x₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁
have right : x ∉ U₁
Tactic: use x, hx.2, hx.1, fun h₁ ↦ hU₁₂ ⟨hx.1, h₁, hx.2⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₂
⊢ ∃ (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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₁
⊢ ∃ (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
have 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
Tactic: rw [PrespectralSpace.isTopologicalBasis.isOpen_iff] at hU₁ hU₂
Cleared hypotheses: hU₁, hU₂, hU₁Z, hU₂Z, hU₁₂, x₁, hx₁, x₂, hx₂
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₁
⊢ ∃ (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
have 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
Tactic: obtain ⟨W₁, hW₁⟩ := hU₁ x₁ hx₁.1
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₁
⊢ ∃ (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
have 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
Tactic: obtain ⟨W₂, hW₂⟩ := hU₂ x₂ hx₂.1
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₂
⊢ ∃ (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
have refine : ∀ (z : X) (hz : z ∈ Z), z ∈ W₁ᶜ ∪ W₂ᶜ
Tactic: refine ⟨W₁ᶜ, W₂ᶜ, by simpa using hW₁.1.1, by simpa using hW₂.1.1, by simp [hW₁.1.2],
    by simp [hW₂.1.2], fun z hz ↦ ?_, ⟨x₁, by grind⟩, ⟨x₂, by grind⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.Prespectral (goal)
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₂
z : X
hz : z ∈ Z
⊢ z ∈ W₁ᶜ ∪ W₂ᶜ
have by_contra! : ∀ (hc : z ∉ W₁ᶜ ∪ W₂ᶜ), False
Tactic: by_contra! hc