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 : ¬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 : ∃ (x : Set (Set X)) (_ : x ⊆ insert Y₁ B) (_ : x.Finite), ⋂₀ x = ∅
hY₂B : ∃ (x : Set (Set X)) (_ : x ⊆ insert Y₂ B) (_ : x.Finite), ⋂₀ x = ∅
neg : ∀ (A₁ : Set (Set X)) (hA₁ : A₁ ⊆ insert Y₁ B) (hA₁' : A₁.Finite) (hA₁'' : ⋂₀ A₁ = ∅), False
⊢ False

Tactic:
obtain ⟨A₁, hA₁, hA₁', hA₁''⟩ := hY₁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 : ∃ (x : Set (Set X)) (_ : x ⊆ insert Y₂ B) (_ : x.Finite), ⋂₀ x = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
neg : ∀ (A₂ : Set (Set X)) (hA₂ : A₂ ⊆ insert Y₂ B) (hA₂' : A₂.Finite) (hA₂'' : ⋂₀ A₂ = ∅), False
⊢ False

Tactic:
obtain ⟨A₂, hA₂, hA₂', hA₂''⟩ := hY₂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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
⊢ Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅

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 = ∅
hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
⊢ Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅

Tactic:
have : Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅ := 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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅
⊢ ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty

Tactic:
rw [← Set.not_nonempty_iff_eq_empty] at this

Premises used: Set.not_nonempty_iff_eq_empty
-- 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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
neg : (Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
⊢ False

Tactic:
apply 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 = ∅}
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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
neg : (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ Z).Nonempty
⊢ (Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty

Tactic:
rw [Set.inter_comm]

Premises used: Set.inter_comm
-- 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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
⊢ (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ Z).Nonempty

Tactic:
IsCompact.nonempty_inter_sInter ?_ (fun _ hb ↦ hb.2) fun F hsub hF ↦ ?_

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 : ¬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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
neg : IsCompact (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}))
neg₁ : ∀ (F : Set (Set X)) (hsub : F ⊆ B') (hF : F.Finite), (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ ⋂₀ F).Nonempty
⊢ (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ Z).Nonempty

Tactic:
refine IsCompact.nonempty_inter_sInter ?_ (fun _ hb ↦ hb.2) fun F hsub hF ↦ ?_

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 : ¬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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
apply : A₁ \ {Y₁} ∪ A₂ \ {Y₂} ⊆ constructibleTopologySubbasis X
⊢ IsCompact (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}))

Tactic:
apply isCompact_sInter_of_subset_constructibleTopologySubbasis _ (hA₁'.diff.union hA₂'.diff)

Premises used: Set.Finite.union, isCompact_sInter_of_subset_constructibleTopologySubbasis, Set.Finite.diff
-- 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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
⊢ A₁ \ {Y₁} ∪ A₂ \ {Y₂} ⊆ constructibleTopologySubbasis X

Tactic:
grind [hB.prop, Set.union_subset_iff]

Premises used: Set.union_subset_iff, Maximal.prop
-- 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_1 : 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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
F : Set (Set X)
hsub : F ⊆ B'
hF : F.Finite
neg : (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂} ∪ F)).Nonempty
⊢ (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ ⋂₀ F).Nonempty

Tactic:
rw [← Set.sInter_union]

Premises used: Set.sInter_union
-- 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_1 : 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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
F : Set (Set X)
hsub : F ⊆ B'
hF : F.Finite
⊢ (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂} ∪ F)).Nonempty

Tactic:
hB.prop.2.1 (_ ∪ F) ?_ <| (hA₁'.diff.union hA₂'.diff).union hF

Premises used: Set.Finite.union, Maximal.prop, Set.Finite.diff, And.right, And.left, Union.union
-- 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_1 : 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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
F : Set (Set X)
hsub : F ⊆ B'
hF : F.Finite
neg : A₁ \ {Y₁} ∪ A₂ \ {Y₂} ∪ F ⊆ B
⊢ (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂} ∪ F)).Nonempty

Tactic:
refine hB.prop.2.1 (_ ∪ F) ?_ <| (hA₁'.diff.union hA₂'.diff).union hF

Premises used: Set.Finite.union, Maximal.prop, Set.Finite.diff, And.right, And.left, Union.union
-- 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_1 : 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 = ∅
A₁ : Set (Set X)
hA₁ : A₁ ⊆ insert Y₁ B
hA₁' : A₁.Finite
hA₁'' : ⋂₀ A₁ = ∅
A₂ : Set (Set X)
hA₂ : A₂ ⊆ insert Y₂ B
hA₂' : A₂.Finite
hA₂'' : ⋂₀ A₂ = ∅
this : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
F : Set (Set X)
hsub : F ⊆ B'
hF : F.Finite
⊢ A₁ \ {Y₁} ∪ A₂ \ {Y₂} ∪ F ⊆ B

Tactic:
grind [Set.diff_singleton_subset_iff, Set.union_subset_iff]

Premises used: Set.union_subset_iff, Set.diff_singleton_subset_iff
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
s : Set β
hf : IsSpectralMap f
h₀ : IsCompact s
h₁ : IsOpen s
⊢ IsCompact (f ⁻¹' s)

Tactic:
hf.isCompact_preimage_of_isOpen h₁ h₀

Premises used: IsSpectralMap.isCompact_preimage_of_isOpen
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsSpectralMap f
⊢ Continuous f

Tactic:
hf.toContinuous

Premises used: IsSpectralMap.toContinuous
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ IsSpectralMap.{u_2, u_2} (α := α) id

Tactic:
⟨continuous_id, fun _s _ => id⟩

Premises used: id, continuous_id, IsSpectralMap.mk
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : β → γ
g : α → β
hf : IsSpectralMap f
hg : IsSpectralMap g
⊢ IsSpectralMap (f ∘ g)

Tactic:
⟨hf.continuous.comp hg.continuous, fun _s hs₀ hs₁ =>
    ((hs₁.preimage_of_isOpen hf hs₀).preimage_of_isOpen hg) (hs₀.preimage hf.continuous)⟩

Premises used: IsSpectralMap.continuous, IsCompact.preimage_of_isOpen, Continuous.comp, IsSpectralMap.mk, IsOpen.preimage
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsProperMap f
⊢ IsSpectralMap f

Tactic:
⟨hf.toContinuous, fun _ _ ↦ hf.isCompact_preimage⟩

Premises used: IsProperMap.toContinuous, IsProperMap.isCompact_preimage, IsSpectralMap.mk
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : FunLike F α β
inst_3 : SpectralMapClass F α β
⊢ ContinuousMapClass F α β

Tactic:
{ ‹SpectralMapClass F α β› with map_continuous := fun f => (map_spectral f).continuous }

Premises used: IsSpectralMap.continuous, SpectralMapClass.map_spectral, ContinuousMapClass.mk
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f g : SpectralMap α β
h : f.toFun = g.toFun
mk :
  ∀ (toFun : α → β) (spectral' : IsSpectralMap toFun)
    (h : { toFun := toFun, spectral' := spectral' : SpectralMap α β }.toFun = g.toFun),
    { toFun := toFun, spectral' := spectral' : SpectralMap α β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
g : SpectralMap α β
toFun : α → β
spectral' : IsSpectralMap toFun
h : { toFun := toFun, spectral' := spectral' : SpectralMap α β }.toFun = g.toFun
mk :
  ∀ (toFun_1 : α → β) (spectral'_1 : IsSpectralMap toFun_1)
    (h :
      { toFun := toFun, spectral' := spectral' : SpectralMap α β }.toFun =
        { toFun := toFun_1, spectral' := spectral'_1 : SpectralMap α β }.toFun),
    { toFun := toFun, spectral' := spectral' : SpectralMap α β } = { toFun := toFun_1, spectral' := spectral'_1 }
⊢ { toFun := toFun, spectral' := spectral' : SpectralMap α β } = g

Tactic:
cases g
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
toFun : α → β
spectral' : IsSpectralMap toFun
toFun_1 : α → β
spectral'_1 : IsSpectralMap toFun_1
h :
  { toFun := toFun, spectral' := spectral' : SpectralMap α β }.toFun =
    { toFun := toFun_1, spectral' := spectral'_1 : SpectralMap α β }.toFun
⊢ { toFun := toFun, spectral' := spectral' : SpectralMap α β } = { toFun := toFun_1, spectral' := spectral'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : SpectralMap α β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f g : SpectralMap α β
h : ∀ (a : α), Eq.{u_3 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : SpectralMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ (⇑(f.copy f' h) : (a : α) → β) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : SpectralMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ Eq (α := (a : α) → α) (⇑(SpectralMap.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Spectral.Hom
Goal:
α : Type u_2
inst : TopologicalSpace α
a : α
⊢ (SpectralMap.id α : (a : α) → α) a = a

Tactic:
rfl

Premises used: rfl