awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact Set.sInter_subset_of_mem hiB' hη.mem

Premises used: Set.sInter_subset_of_mem, IsGenericPoint.mem
-- 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'
⊢ IsCompact i

Tactic:
grind [hB.prop, constructibleTopologySubbasis]

Premises used: Maximal.prop, 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
𝒮 : 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'
⊢ IsCompact i

Tactic:
have hi_cmpt : IsCompact i := by grind [hB.prop, 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
𝒮 : 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
⊢ IsOpen[inst] i

Tactic:
grind [hB.prop, constructibleTopologySubbasis]

Premises used: Maximal.prop, 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
𝒮 : 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
neg : (i ∩ Z).Nonempty
⊢ hZ_irred.genericPoint (S := Z) ∈ i

Tactic:
rw [hη.mem_open_set_iff (by grind [hB.prop, constructibleTopologySubbasis]), Set.inter_comm]

Premises used: Set.inter_comm, IsGenericPoint.mem_open_set_iff
-- 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'
hi_cmpt : IsCompact i
⊢ (i ∩ Z).Nonempty

Tactic:
hi_cmpt.nonempty_inter_sInter (fun _ hb ↦ hb.2) fun a ha hfa ↦ ?_

Premises used: And.right, IsCompact.nonempty_inter_sInter
-- 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'
hi_cmpt : IsCompact i
neg : ∀ (a : Set (Set X)) (ha : a ⊆ B') (hfa : a.Finite), (i ∩ ⋂₀ a).Nonempty
⊢ (i ∩ Z).Nonempty

Tactic:
refine hi_cmpt.nonempty_inter_sInter (fun _ hb ↦ hb.2) fun a ha hfa ↦ ?_

Premises used: IsCompact.nonempty_inter_sInter
-- 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'
hi_cmpt : IsCompact i
a : Set (Set X)
ha : a ⊆ B'
hfa : a.Finite
neg : (⋂₀ insert i a).Nonempty
⊢ (i ∩ ⋂₀ a).Nonempty

Tactic:
rw [← Set.sInter_insert]

Premises used: Set.sInter_insert
-- 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'
hi_cmpt : IsCompact i
a : Set (Set X)
ha : a ⊆ B'
hfa : a.Finite
⊢ insert i a ⊆ B

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 ∈ 𝒮
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
⊢ (insert i a).Finite

Tactic:
simpa
-- 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'
hi_cmpt : IsCompact i
a : Set (Set X)
ha : a ⊆ B'
hfa : a.Finite
⊢ (⋂₀ insert i a).Nonempty

Tactic:
exact hB.prop.2.1 _ (by grind) (by simpa)

Premises used: Maximal.prop, 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 ∈ 𝒮
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
⊢ ¬IsPreirreducible Z

Tactic:
simp only [IsIrreducible, hZ_nonempty, true_and] at hZ_irred

Premises used: IsIrreducible, true_and
-- 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 : ¬IsPreirreducible Z
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
⊢ False

Tactic:
obtain ⟨Y₁, Y₂, hY₁_cl, hY₂_cl, hc₁, hc₂, hsub, ⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩⟩ :=
      PrespectralSpace.exists_isClosed_of_not_isPreirreducible _ hZ_irred

Premises used: PrespectralSpace.exists_isClosed_of_not_isPreirreducible
-- 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 : ¬IsPreirreducible Z
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₂ᶜ
⊢ Y₁ ∈ 𝔅

Tactic:
have hY₁ : Y₁ ∈ 𝔅 := .inr ⟨hY₁_cl, hc₁⟩
-- 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 : ¬IsPreirreducible Z
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
⊢ Y₂ ∈ 𝔅

Tactic:
have hY₂ : Y₂ ∈ 𝔅 := .inr ⟨hY₂_cl, hc₂⟩
-- 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 : ¬IsPreirreducible Z
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
⊢ Y₁ ∩ ⋂₀ B = ∅

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 ∈ 𝒮
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
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
⊢ Y₁ ∩ ⋂₀ B = ∅

Tactic:
have hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅ := 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 ∈ 𝒮
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
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
⊢ Y₂ ∩ ⋂₀ B = ∅

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 ∈ 𝒮
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
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
⊢ Y₂ ∩ ⋂₀ B = ∅

Tactic:
have hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅ := 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 ∈ 𝒮
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
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
hY₁B : insert Y₁ B ∈ 𝒮
⊢ False

Tactic:
grind [show insert Y₁ B ⊆ B from hB.le_of_ge hY₁B (Set.subset_insert Y₁ B)]

Premises used: Maximal.le_of_ge, Set.subset_insert
-- 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 : ¬IsPreirreducible Z
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
⊢ insert Y₁ B ∉ 𝒮

Tactic:
have hY₁B : insert Y₁ B ∉ 𝒮 := by
      intro hY₁B
      grind [show insert Y₁ B ⊆ B from hB.le_of_ge hY₁B (Set.subset_insert Y₁ 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 : ¬IsPreirreducible Z
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
hY₁B : insert Y₁ B ∉ 𝒮
hY₂B : insert Y₂ B ∈ 𝒮
⊢ False

Tactic:
grind [show insert Y₂ B ⊆ B from hB.le_of_ge hY₂B (Set.subset_insert Y₂ B)]

Premises used: Maximal.le_of_ge, Set.subset_insert
-- 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 : ¬IsPreirreducible Z
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
hY₁B : insert Y₁ B ∉ 𝒮
⊢ insert Y₂ B ∉ 𝒮

Tactic:
have hY₂B : insert Y₂ B ∉ 𝒮 := by
      intro hY₂B
      grind [show insert Y₂ B ⊆ B from hB.le_of_ge hY₂B (Set.subset_insert Y₂ 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 : ¬IsPreirreducible Z
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
hY₁B : ¬(insert Y₁ B ⊆ 𝔅 ∧ (∀ Q ⊆ insert Y₁ B, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ insert Y₁ B = ∅)
hY₂B : ¬(insert Y₂ B ⊆ 𝔅 ∧ (∀ Q ⊆ insert Y₂ B, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ insert Y₂ B = ∅)
⊢ ∃ (x : Set (Set X)) (_ : x ⊆ insert Y₁ B) (_ : x.Finite), ⋂₀ x = ∅

Tactic:
simp only [Set.insert_subset_iff, hY₁, hB.prop.1, and_self, Set.sInter_insert, hY₁_inter_B,
      and_true, true_and, not_forall, Set.not_nonempty_iff_eq_empty, hY₂, hY₂_inter_B] at hY₁B hY₂B

Premises used: and_true, and_self, Set.not_nonempty_iff_eq_empty, Set.sInter_insert, Maximal.prop, Set.insert_subset_iff, And.left, Classical.not_forall, true_and
-- 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 : ¬IsPreirreducible Z
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₂ᶜ
hY₁ : Y₁ ∈ 𝔅
hY₂ : Y₂ ∈ 𝔅
hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
hY₁B : ¬(insert Y₁ B ⊆ 𝔅 ∧ (∀ Q ⊆ insert Y₁ B, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ insert Y₁ B = ∅)
hY₂B : ¬(insert Y₂ B ⊆ 𝔅 ∧ (∀ Q ⊆ insert Y₂ B, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ insert Y₂ B = ∅)
hY₁B₁ : ∃ (x : Set (Set X)) (_ : x ⊆ insert Y₁ B) (_ : x.Finite), ⋂₀ x = ∅
⊢ ∃ (x : Set (Set X)) (_ : x ⊆ insert Y₂ B) (_ : x.Finite), ⋂₀ x = ∅

Tactic:
simp only [Set.insert_subset_iff, hY₁, hB.prop.1, and_self, Set.sInter_insert, hY₁_inter_B,
      and_true, true_and, not_forall, Set.not_nonempty_iff_eq_empty, hY₂, hY₂_inter_B] at hY₁B hY₂B

Premises used: and_true, and_self, Set.not_nonempty_iff_eq_empty, Set.sInter_insert, Maximal.prop, Set.insert_subset_iff, And.left, Classical.not_forall, true_and