awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ¬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₂ᶜ
⊢ False
have hY₁ : Y₁ ∈ 𝔅
Tactic: have hY₁ : Y₁ ∈ 𝔅 := .inr ⟨hY₁_cl, hc₁⟩
-- 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 : ¬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₁ ∈ 𝔅
⊢ False
have hY₂ : Y₂ ∈ 𝔅
Tactic: have hY₂ : Y₂ ∈ 𝔅 := .inr ⟨hY₂_cl, hc₂⟩
-- 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 : ¬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₂ ∈ 𝔅
⊢ False
have hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅
Tactic: have hY₁_inter_B : Y₁ ∩ ⋂₀ B = ∅ := by grind
-- 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 : ¬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 = ∅
⊢ False
have hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅
Tactic: have hY₂_inter_B : Y₂ ∩ ⋂₀ B = ∅ := by grind
-- 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 : ¬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 = ∅
⊢ False
have hY₁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)]
-- 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 : ¬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
have hY₂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)]
-- 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 : ¬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 = ∅)
⊢ False
have hY₁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
Cleared hypotheses: hY₁B, hY₂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 : ¬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 = ∅
⊢ False
have hY₂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
Cleared hypotheses: hY₁B, hY₂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 : ¬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 = ∅
⊢ False
have neg : ∀ (A₁ : Set (Set X)) (hA₁ : A₁ ⊆ insert Y₁ B) (hA₁' : A₁.Finite) (hA₁'' : ⋂₀ A₁ = ∅), False
Tactic: obtain ⟨A₁, hA₁, hA₁', hA₁''⟩ := hY₁B
Cleared hypotheses: hY₁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 : ¬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₁ = ∅
⊢ False
have neg : ∀ (A₂ : Set (Set X)) (hA₂ : A₂ ⊆ insert Y₂ B) (hA₂' : A₂.Finite) (hA₂'' : ⋂₀ A₂ = ∅), False
Tactic: obtain ⟨A₂, hA₂, hA₂', hA₂''⟩ := hY₂B
Cleared hypotheses: hY₂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 : ¬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₂ = ∅
⊢ False
have this : Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅
Tactic: have : Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) = ∅ := by grind
-- 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 : ¬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₂}) = ∅
⊢ False
have this₁ : ¬(Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
Tactic: rw [← Set.not_nonempty_iff_eq_empty] at 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 = ∅}
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
⊢ False
have neg : (Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
Tactic: apply 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 = ∅}
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
⊢ (Z ∩ ⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂})).Nonempty
have neg : (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ Z).Nonempty
Tactic: rw [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 : ¬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
have neg : IsCompact (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}))
Tactic: refine IsCompact.nonempty_inter_sInter ?_ (fun _ hb ↦ hb.2) fun F hsub 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
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₂}))
⊢ (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ Z).Nonempty
have neg₁ : ∀ (F : Set (Set X)) (hsub : F ⊆ B') (hF : F.Finite), (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}) ∩ ⋂₀ F).Nonempty
Tactic: refine IsCompact.nonempty_inter_sInter ?_ (fun _ hb ↦ hb.2) fun F hsub 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
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
⊢ IsCompact (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂}))
have apply : A₁ \ {Y₁} ∪ A₂ \ {Y₂} ⊆ constructibleTopologySubbasis X
Tactic: apply isCompact_sInter_of_subset_constructibleTopologySubbasis _ (hA₁'.diff.union hA₂'.diff)
-- 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
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
have neg : (⋂₀ (A₁ \ {Y₁} ∪ A₂ \ {Y₂} ∪ F)).Nonempty
Tactic: rw [← Set.sInter_union]
-- 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
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
have neg : A₁ \ {Y₁} ∪ A₂ \ {Y₂} ∪ F ⊆ B
Tactic: refine hB.prop.2.1 (_ ∪ F) ?_ <| (hA₁'.diff.union hA₂'.diff).union hF
-- Lean 4 proof step from Mathlib.Topology.Spectral.Hom (goal)
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
⊢ f = g
have mk : ∀ (toFun : α → β) (spectral' : IsSpectralMap toFun)
  (h : { toFun := toFun, spectral' := spectral' : SpectralMap α β }.toFun = g.toFun),
  { toFun := toFun, spectral' := spectral' : SpectralMap α β } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Spectral.Hom (goal)
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
⊢ { toFun := toFun, spectral' := spectral' : SpectralMap α β } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h