awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
x : α
⊢ irreducibleComponent x ⊆ _root_.closure (genericPoints α)
have refine : {(↑(ofComponent (Subtype.mk (p := fun (x : Set α) ↦ x ∈ irreducibleComponents α) (irreducibleComponent x) sorry)) : α)} ⊆
  genericPoints α
Tactic: refine (isGenericPoint_ofComponent
    ⟨_, irreducibleComponent_mem_irreducibleComponents x⟩).symm.trans_subset (closure_mono ?_)
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : IrreducibleSpace α
inst_3 : T0Space α
⊢ genericPoints α = {genericPoint α}
have h : ∀ (x : α), x ∈ genericPoints α ↔ Membership.mem (γ := Set α) {genericPoint α} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : IrreducibleSpace α
inst_3 : T0Space α
x : α
⊢ x ∈ genericPoints α ↔ Membership.mem (γ := Set α) {genericPoint α} x
have h : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Set (Set α)) {univ} (closure {x})} x ↔
  Membership.mem (γ := Set α) {genericPoint α} x
Tactic: rw [genericPoints, irreducibleComponents_eq_singleton]
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
ho : IsOpen[inst] s
⊢ IsOpen[constructibleTopology X] s
have hs₁ : s ∈ constructibleTopologySubbasis X
Tactic: apply TopologicalSpace.isOpen_generateFrom_of_mem
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsCompact sᶜ
ho : IsClosed[inst] s
⊢ IsOpen[constructibleTopology X] s
have hs₁ : s ∈ constructibleTopologySubbasis X
Tactic: apply TopologicalSpace.isOpen_generateFrom_of_mem
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
s : Set X
hs : s ∈ constructibleTopologySubbasis X
⊢ IsCompact s
have inl : ∀ (hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsOpen[inst] s ∧ IsCompact s} s), IsCompact s
Tactic: obtain (hs | hs) := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
s : Set X
hs : s ∈ constructibleTopologySubbasis X
inl : ∀ (hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsOpen[inst] s ∧ IsCompact s} s), IsCompact s
⊢ IsCompact s
have inr : ∀ (hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[inst] s ∧ IsCompact sᶜ} s), IsCompact s
Tactic: obtain (hs | hs) := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
⊢ IsCompact (⋂₀ s)
have refine_1 : ∀ (t : Set X) (ht : t ∈ s), IsOpen[inst] t ∨ IsClosed[inst] t
Tactic: refine QuasiSeparatedSpace.isCompact_sInter hf (fun t ht ↦ ?_) (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
refine_1 : ∀ (t : Set X) (ht : t ∈ s), IsOpen[inst] t ∨ IsClosed[inst] t
⊢ IsCompact (⋂₀ s)
have refine_2 : ∀ (t : Set X) (ht : t ∈ s), IsCompact t
Tactic: refine QuasiSeparatedSpace.isCompact_sInter hf (fun t ht ↦ ?_) (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
⊢ IsOpen[inst] t ∨ IsClosed[inst] t
have refine_1 : Membership.mem (γ := Set (Set X)) {s : Set X | IsOpen[inst] s ∧ IsCompact s} t → IsOpen[inst] t
Tactic: apply (hs ht).imp
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSeparatedSpace X
s : Set (Set X)
hs : s ⊆ constructibleTopologySubbasis X
hf : s.Finite
t : Set X
ht : t ∈ s
refine_1 : Membership.mem (γ := Set (Set X)) {s : Set X | IsOpen[inst] s ∧ IsCompact s} t → IsOpen[inst] t
⊢ IsOpen[inst] t ∨ IsClosed[inst] t
have refine_1₁ : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[inst] s ∧ IsCompact sᶜ} t → IsClosed[inst] t
Tactic: apply (hs ht).imp
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
⊢ CompactSpace.{u_1} (WithConstructibleTopology X)
have apply : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
Tactic: apply compactSpace_generateFrom_of_compl_mem (T := constructibleTopology X) 𝔅 rfl (by simp [𝔅])
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
this : 𝒮 = ∅
⊢ ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
have contrapose! : ∀ (this : ∃ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅), 𝒮.Nonempty
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
⊢ ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
have suffices : 𝒮 = ∅
Tactic: suffices 𝒮 = ∅ by contrapose! this; tauto
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
⊢ 𝒮 = ∅
have by_contra! : ∀ (h𝒮 : 𝒮.Nonempty), False
Tactic: by_contra! h𝒮
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
h𝒮 : 𝒮.Nonempty
⊢ False
have obtain : ∀ (s : Set (Set X)) (hs : s ∈ 𝒮), False
Tactic: obtain ⟨s, hs⟩ := h𝒮
Cleared hypotheses: h𝒮
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
⊢ ∃ (m : Set (Set X)), s ⊆ m ∧ Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) m
have refine : ∀ (c : Set (Set (Set X))) (hc𝒮 : c ⊆ 𝒮) (hc : IsChain (fun (x1 x2 : Set (Set X)) ↦ x1 ⊆ x2) c),
  c.Nonempty → ∀ (hne : c.Nonempty) (x : Set (Set X)) (hxc : x ∈ c), hne = sorry → ∃ ub ∈ 𝒮, ∀ s ∈ c, s ⊆ ub
Tactic: refine zorn_subset_nonempty 𝒮 (fun c hc𝒮 hc hne@⟨x, hxc⟩ ↦ ?_) s hs
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun (x1 x2 : Set (Set X)) ↦ x1 ⊆ x2) c
h hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h_1 : hne = ⋯
⊢ ∃ ub ∈ 𝒮, ∀ s ∈ c, s ⊆ ub
have refine : ⋃₀ c ∈ 𝒮
Tactic: refine ⟨⋃₀ c, ?_, fun S hSc ↦ Set.subset_sUnion_of_subset c S subset_rfl hSc⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun (x1 x2 : Set (Set X)) ↦ x1 ⊆ x2) c
h hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h_1 : hne = ⋯
⊢ ⋃₀ c ∈ 𝒮
have refine : ∀ (a : Set (Set X)) (hac : a ⊆ ⋃₀ c) (ha : a.Finite), (⋂₀ a).Nonempty
Tactic: refine ⟨by grind, fun a hac ha ↦ ?_, by grind⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
c : Set (Set (Set X))
hc𝒮 : c ⊆ 𝒮
hc : IsChain (fun (x1 x2 : Set (Set X)) ↦ x1 ⊆ x2) c
h hne : c.Nonempty
x : Set (Set X)
hxc : x ∈ c
h_1 : hne = ⋯
a : Set (Set X)
hac : a ⊆ ⋃₀ c
ha : a.Finite
⊢ (⋂₀ a).Nonempty
have obtain : ∀ (i : Set (Set X)) (hmem : i ∈ c) (hsub : a ⊆ i), (⋂₀ a).Nonempty
Tactic: obtain ⟨i, hmem, hsub⟩ := hc.directedOn.exists_mem_subset_of_finite_of_subset_sUnion hne ha hac
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
⊢ False
have obtain : ∀ (B : Set (Set X)) (hsB : s ⊆ B) (hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B), False
Tactic: obtain ⟨B, hsB, hB⟩ := by
    refine zorn_subset_nonempty 𝒮 (fun c hc𝒮 hc hne@⟨x, hxc⟩ ↦ ?_) s hs
    refine ⟨⋃₀ c, ?_, fun S hSc ↦ Set.subset_sUnion_of_subset c S subset_rfl hSc⟩
    refine ⟨by grind, fun a hac ha ↦ ?_, by grind⟩
    obtain ⟨i, hmem, hsub⟩ := hc.directedOn.exists_mem_subset_of_finite_of_subset_sUnion hne ha hac
    exact (hc𝒮 hmem).2.1 a hsub ha
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
⊢ False
have hZ_closed : IsClosed[inst] Z
Tactic: have hZ_closed : IsClosed Z := isClosed_sInter fun b hb ↦ hb.2
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
⊢ False
have hZ_nonempty : Z.Nonempty
Tactic: have hZ_nonempty : Z.Nonempty :=
    CompactSpace.nonempty_sInter (fun _ ht ↦ ht.2) fun t ht hf ↦
      hB.prop.2.1 _ (subset_trans ht (by simp [B'])) hf
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
⊢ False
have pos : ∀ (hZ_irred : IsIrreducible Z), False
Tactic: by_cases hZ_irred : IsIrreducible Z
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
pos : ∀ (hZ_irred : IsIrreducible Z), False
⊢ False
have neg : ∀ (hZ_irred : ¬IsIrreducible Z), False
Tactic: by_cases hZ_irred : IsIrreducible Z
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
⊢ False
have pos : (⋂₀ B).Nonempty
Tactic: suffices (⋂₀ B).Nonempty by simp_all [hB.prop.2.2]
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
⊢ (⋂₀ B).Nonempty
have hη : IsGenericPoint (hZ_irred.genericPoint (S := Z)) Z
Tactic: have hη := hZ_irred.isGenericPoint_genericPoint (isClosed_sInter fun b hb ↦ hb.2)
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint (hZ_irred.genericPoint (S := Z)) Z
⊢ (⋂₀ B).Nonempty
have pos : hZ_irred.genericPoint (S := Z) ∈ ⋂₀ B
Tactic: refine ⟨hZ_irred.genericPoint, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint (hZ_irred.genericPoint (S := Z)) Z
i : Set X
hi : i ∈ B
⊢ hZ_irred.genericPoint (S := Z) ∈ i
have pos : ∀ (hiB' : i ∈ B'), hZ_irred.genericPoint (S := Z) ∈ i
Tactic: by_cases hiB' : i ∈ B'
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint (hZ_irred.genericPoint (S := Z)) Z
i : Set X
hi : i ∈ B
pos : ∀ (hiB' : i ∈ B'), hZ_irred.genericPoint (S := Z) ∈ i
⊢ hZ_irred.genericPoint (S := Z) ∈ i
have neg : ∀ (hiB' : i ∉ B'), hZ_irred.genericPoint (S := Z) ∈ i
Tactic: by_cases hiB' : i ∈ B'
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint (hZ_irred.genericPoint (S := Z)) Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
⊢ hZ_irred.genericPoint (S := Z) ∈ i
have hi_cmpt : IsCompact i
Tactic: have hi_cmpt : IsCompact i := by grind [hB.prop, constructibleTopologySubbasis]
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint (hZ_irred.genericPoint (S := Z)) Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
⊢ hZ_irred.genericPoint (S := Z) ∈ i
have neg : (i ∩ Z).Nonempty
Tactic: rw [hη.mem_open_set_iff (by grind [hB.prop, constructibleTopologySubbasis]), Set.inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint (hZ_irred.genericPoint (S := Z)) Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
⊢ (i ∩ Z).Nonempty
have neg : ∀ (a : Set (Set X)) (ha : a ⊆ B') (hfa : a.Finite), (i ∩ ⋂₀ a).Nonempty
Tactic: refine hi_cmpt.nonempty_inter_sInter (fun _ hb ↦ hb.2) fun a ha hfa ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : IsIrreducible Z
hη : IsGenericPoint (hZ_irred.genericPoint (S := Z)) Z
i : Set X
hi : i ∈ B
hiB' : i ∉ B'
hi_cmpt : IsCompact i
a : Set (Set X)
ha : a ⊆ B'
hfa : a.Finite
⊢ (i ∩ ⋂₀ a).Nonempty
have neg : (⋂₀ insert i a).Nonempty
Tactic: rw [← Set.sInter_insert]
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : ¬IsIrreducible Z
⊢ False
have hZ_irred₁ : ¬IsPreirreducible Z
Tactic: simp only [IsIrreducible, hZ_nonempty, true_and] at hZ_irred
Cleared hypotheses: hZ_irred
-- Lean 4 proof step from Mathlib.Topology.Spectral.ConstructibleTopology (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : QuasiSober X
inst_3 : PrespectralSpace X
inst_4 : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P : Set (Set X) | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
s : Set (Set X)
hs : s ∈ 𝒮
B : Set (Set X)
hsB : s ⊆ B
hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B
B' : Set (Set X) := {s : Set X | s ∈ B ∧ IsClosed[inst] s}
Z : Set X := ⋂₀ B'
hZ_closed : IsClosed[inst] Z
hZ_nonempty : Z.Nonempty
hZ_irred : ¬IsPreirreducible Z
⊢ False
have neg : ∀ (Y₁ Y₂ : Set X) (hY₁_cl : IsClosed[inst] Y₁) (hY₂_cl : IsClosed[inst] Y₂) (hc₁ : IsCompact Y₁ᶜ) (hc₂ : IsCompact Y₂ᶜ)
  (hsub : Z ⊆ Y₁ ∪ Y₂) (x₁ : X) (hx₁ : x₁ ∈ Z ∩ Y₁ᶜ) (x₂ : X) (hx₂ : x₂ ∈ Z ∩ Y₂ᶜ), False
Tactic: obtain ⟨Y₁, Y₂, hY₁_cl, hY₂_cl, hc₁, hc₂, hsub, ⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩ :=
      PrespectralSpace.exists_isClosed_of_not_isPreirreducible _ hZ_irred