awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
inr : ∀ (hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[inst] s ∧ IsCompact sᶜ} s), IsCompact s
⊢ IsCompact s

Tactic:
obtain (hs | hs) := hs
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsOpen[inst] s ∧ IsCompact s} s
⊢ IsCompact s

Tactic:
hs.2

Premises used: And.right
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsOpen[inst] s ∧ IsCompact s} s
⊢ IsCompact s

Tactic:
exact hs.2

Premises used: And.right
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[inst] s ∧ IsCompact sᶜ} s
⊢ IsCompact s

Tactic:
hs.1.isCompact

Premises used: And.left, IsClosed.isCompact
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
s : Set X
hs : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[inst] s ∧ IsCompact sᶜ} s
⊢ IsCompact s

Tactic:
exact hs.1.isCompact

Premises used: And.left, IsClosed.isCompact
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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)

Tactic:
QuasiSeparatedSpace.isCompact_sInter hf (fun t ht ↦ ?_) (fun t ht ↦ ?_)

Premises used: QuasiSeparatedSpace.isCompact_sInter
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
refine_2 : ∀ (t : Set X) (ht : t ∈ s), IsCompact t
⊢ IsCompact (⋂₀ s)

Tactic:
refine QuasiSeparatedSpace.isCompact_sInter hf (fun t ht ↦ ?_) (fun t ht ↦ ?_)

Premises used: QuasiSeparatedSpace.isCompact_sInter
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
refine_1₁ : Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[inst] s ∧ IsCompact sᶜ} t → IsClosed[inst] t
⊢ IsOpen[inst] t ∨ IsClosed[inst] t

Tactic:
apply (hs ht).imp

Premises used: Or.imp
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
⊢ Membership.mem (γ := Set (Set X)) {s : Set X | IsOpen[inst] s ∧ IsCompact s} t → IsOpen[inst] t

Tactic:
grind
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
⊢ Membership.mem (γ := Set (Set X)) {s : Set X | IsClosed[inst] s ∧ IsCompact sᶜ} t → IsClosed[inst] t

Tactic:
grind
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
⊢ IsCompact t

Tactic:
isCompact_of_mem_constructibleTopologySubbasis (hs ht)

Premises used: isCompact_of_mem_constructibleTopologySubbasis
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
⊢ IsCompact t

Tactic:
exact isCompact_of_mem_constructibleTopologySubbasis (hs ht)

Premises used: isCompact_of_mem_constructibleTopologySubbasis
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
⊢ ∀ s ∈ 𝔅, sᶜ ∈ 𝔅

Tactic:
simp [𝔅]
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
apply : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
⊢ CompactSpace.{u_1} (WithConstructibleTopology X)

Tactic:
apply compactSpace_generateFrom_of_compl_mem (T := constructibleTopology X) 𝔅 rfl (by simp [𝔅])

Premises used: compactSpace_generateFrom_of_compl_mem, rfl
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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 : 𝒮 = ∅
contrapose! : ∀ (this : ∃ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅), 𝒮.Nonempty
⊢ ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty

Tactic:
contrapose! this
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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

Tactic:
tauto
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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 = ∅}
suffices : 𝒮 = ∅
⊢ ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty

Tactic:
suffices 𝒮 = ∅ by contrapose! this; tauto
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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 = ∅}
by_contra! : ∀ (h𝒮 : 𝒮.Nonempty), False
⊢ 𝒮 = ∅

Tactic:
by_contra! h𝒮
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
obtain : ∀ (s : Set (Set X)) (hs : s ∈ 𝒮), False
⊢ False

Tactic:
obtain ⟨s, hs⟩ := h𝒮
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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

Tactic:
zorn_subset_nonempty 𝒮 (fun c hc𝒮 hc hne@⟨x, hxc⟩ ↦ ?_) s hs

Premises used: Membership.mem, Exists, And, _private.0.compactSpace_withConstructibleTopology.match_1, zorn_subset_nonempty
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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 ∈ 𝒮
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 = ⋯ → ∃ ub ∈ 𝒮, ∀ s ∈ c, s ⊆ ub
⊢ ∃ (m : Set (Set X)), s ⊆ m ∧ Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) m

Tactic:
refine zorn_subset_nonempty 𝒮 (fun c hc𝒮 hc hne@⟨x, hxc⟩ ↦ ?_) s hs

Premises used: Membership.mem, Exists, And, _private.0.compactSpace_withConstructibleTopology.match_1, zorn_subset_nonempty
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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

Tactic:
⟨⋃₀ c, ?_, fun S hSc ↦ Set.subset_sUnion_of_subset c S subset_rfl hSc⟩

Premises used: Set.sUnion, Set.subset_sUnion_of_subset, And.intro, Exists.intro, subset_rfl
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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 = ⋯
refine : ⋃₀ c ∈ 𝒮
⊢ ∃ ub ∈ 𝒮, ∀ s ∈ c, s ⊆ ub

Tactic:
refine ⟨⋃₀ c, ?_, fun S hSc ↦ Set.subset_sUnion_of_subset c S subset_rfl hSc⟩
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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 ⊆ 𝔅

Tactic:
grind
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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 = ∅

Tactic:
grind
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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 = ⋯
refine : ∀ (a : Set (Set X)) (hac : a ⊆ ⋃₀ c) (ha : a.Finite), (⋂₀ a).Nonempty
⊢ ⋃₀ c ∈ 𝒮

Tactic:
refine ⟨by grind, fun a hac ha ↦ ?_, by grind⟩
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
obtain : ∀ (i : Set (Set X)) (hmem : i ∈ c) (hsub : a ⊆ i), (⋂₀ a).Nonempty
⊢ (⋂₀ a).Nonempty

Tactic:
obtain ⟨i, hmem, hsub⟩ := hc.directedOn.exists_mem_subset_of_finite_of_subset_sUnion hne ha hac

Premises used: IsChain.directedOn, DirectedOn.exists_mem_subset_of_finite_of_subset_sUnion
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
i : Set (Set X)
hmem : i ∈ c
hsub : a ⊆ i
⊢ (⋂₀ a).Nonempty

Tactic:
(hc𝒮 hmem).2.1 a hsub ha

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
i : Set (Set X)
hmem : i ∈ c
hsub : a ⊆ i
⊢ (⋂₀ a).Nonempty

Tactic:
exact (hc𝒮 hmem).2.1 a hsub ha

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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 ∈ 𝒮
obtain : ∀ (B : Set (Set X)) (hsB : s ⊆ B) (hB : Maximal (fun (x : Set (Set X)) ↦ x ∈ 𝒮) B), False
⊢ 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
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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'
⊢ IsClosed[inst] Z

Tactic:
have hZ_closed : IsClosed Z := isClosed_sInter fun b hb ↦ hb.2
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
t : Set (Set X)
ht : t ⊆ B'
hf : t.Finite
⊢ B' ⊆ B

Tactic:
simp [B']
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
⊢ 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
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
neg : ∀ (hZ_irred : ¬IsIrreducible Z), False
⊢ False

Tactic:
by_cases hZ_irred : IsIrreducible Z

Premises used: IsIrreducible
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
this : (⋂₀ B).Nonempty
⊢ False

Tactic:
simp_all [hB.prop.2.2]

Premises used: Maximal.prop, And.right
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
pos : (⋂₀ B).Nonempty
⊢ False

Tactic:
suffices (⋂₀ B).Nonempty by simp_all [hB.prop.2.2]
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
⊢ IsGenericPoint (hZ_irred.genericPoint (S := Z)) Z

Tactic:
have hη := hZ_irred.isGenericPoint_genericPoint (isClosed_sInter fun b hb ↦ hb.2)
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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

Tactic:
⟨hZ_irred.genericPoint, ?_⟩

Premises used: IsIrreducible.genericPoint, Set.Nonempty, Exists.intro
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
pos : hZ_irred.genericPoint (S := Z) ∈ ⋂₀ B
⊢ (⋂₀ B).Nonempty

Tactic:
refine ⟨hZ_irred.genericPoint, ?_⟩
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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
neg : ∀ (hiB' : i ∉ B'), hZ_irred.genericPoint (S := Z) ∈ i
⊢ hZ_irred.genericPoint (S := Z) ∈ i

Tactic:
by_cases hiB' : i ∈ B'
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
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

Tactic:
Set.sInter_subset_of_mem hiB' hη.mem

Premises used: Set.sInter_subset_of_mem, IsGenericPoint.mem