[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
[PROOFSTEP]
rw [noetherianSpace_iff, CompleteLattice.wellFounded_iff_isSupFiniteCompact,
  CompleteLattice.isSupFiniteCompact_iff_all_elements_compact]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ (∀ (k : Opens α), CompleteLattice.IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact ↑s
[PROOFSTEP]
exact forall_congr' Opens.isCompactElement_iff
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
⊢ IsCompact s
[PROOFSTEP]
refine isCompact_iff_finite_subcover.2 fun U hUo hs => ?_
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ (i : ι✝), U i
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
[PROOFSTEP]
rcases((noetherianSpace_iff_opens α).mp ‹_› ⟨⋃ i, U i, isOpen_iUnion hUo⟩).elim_finite_subcover U hUo
    Set.Subset.rfl with
  ⟨t, ht⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ (i : ι✝), U i
t : Finset ι✝
ht : ↑{ carrier := ⋃ (i : ι✝), U i, is_open' := (_ : IsOpen (⋃ (i : ι✝), U i)) } ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
[PROOFSTEP]
exact ⟨t, hs.trans ht⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
[PROOFSTEP]
tfae_have 1 ↔ 2
[GOAL]
case tfae_1_iff_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ NoetherianSpace α ↔ WellFounded fun s t => s < t
[PROOFSTEP]
refine' (noetherianSpace_iff α).trans (Surjective.wellFounded_iff Opens.compl_bijective.2 _)
[GOAL]
case tfae_1_iff_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ ∀ {a b : Opens α}, a > b ↔ Opens.compl a < Opens.compl b
[PROOFSTEP]
exact (@OrderIso.compl (Set α)).lt_iff_lt.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
[PROOFSTEP]
tfae_have 1 ↔ 4
[GOAL]
case tfae_1_iff_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
[PROOFSTEP]
exact noetherianSpace_iff_opens α
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
[PROOFSTEP]
tfae_have 1 → 3
[GOAL]
case tfae_1_to_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
⊢ NoetherianSpace α → ∀ (s : Set α), IsCompact s
[PROOFSTEP]
exact @NoetherianSpace.isCompact α _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
[PROOFSTEP]
tfae_have 3 → 4
[GOAL]
case tfae_3_to_4
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
⊢ (∀ (s : Set α), IsCompact s) → ∀ (s : Opens α), IsCompact ↑s
[PROOFSTEP]
exact fun h s => h s
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
tfae_1_iff_2 : NoetherianSpace α ↔ WellFounded fun s t => s < t
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact ↑s
tfae_1_to_3 : NoetherianSpace α → ∀ (s : Set α), IsCompact s
tfae_3_to_4 : (∀ (s : Set α), IsCompact s) → ∀ (s : Opens α), IsCompact ↑s
⊢ TFAE [NoetherianSpace α, WellFounded fun s t => s < t, ∀ (s : Set α), IsCompact s, ∀ (s : Opens α), IsCompact ↑s]
[PROOFSTEP]
tfae_finish
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type ?u.3614
⊢ NoetherianSpace (CofiniteTopology α)
[PROOFSTEP]
simp only [noetherianSpace_iff_isCompact, isCompact_iff_ultrafilter_le_nhds, CofiniteTopology.nhds_eq,
  Ultrafilter.le_sup_iff, Filter.le_principal_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type ?u.3614
⊢ ∀ (s : Set (CofiniteTopology α)) (f : Ultrafilter (CofiniteTopology α)),
    s ∈ ↑f → ∃ a, a ∈ s ∧ (↑f ≤ pure a ∨ ↑f ≤ Filter.cofinite)
[PROOFSTEP]
intro s f hs
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type ?u.3614
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ ↑f
⊢ ∃ a, a ∈ s ∧ (↑f ≤ pure a ∨ ↑f ≤ Filter.cofinite)
[PROOFSTEP]
rcases f.le_cofinite_or_eq_pure with (hf | ⟨a, rfl⟩)
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type ?u.3614
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ ↑f
hf : ↑f ≤ Filter.cofinite
⊢ ∃ a, a ∈ s ∧ (↑f ≤ pure a ∨ ↑f ≤ Filter.cofinite)
[PROOFSTEP]
rcases Filter.nonempty_of_mem hs with ⟨a, ha⟩
[GOAL]
case inl.intro
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type ?u.3614
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ ↑f
hf : ↑f ≤ Filter.cofinite
a : CofiniteTopology α
ha : a ∈ s
⊢ ∃ a, a ∈ s ∧ (↑f ≤ pure a ∨ ↑f ≤ Filter.cofinite)
[PROOFSTEP]
exact ⟨a, ha, Or.inr hf⟩
[GOAL]
case inr.intro
α✝ : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α✝
inst✝ : TopologicalSpace β
α : Type ?u.3614
s : Set (CofiniteTopology α)
a : CofiniteTopology α
hs : s ∈ ↑(pure a)
⊢ ∃ a_1, a_1 ∈ s ∧ (↑(pure a) ≤ pure a_1 ∨ ↑(pure a) ≤ Filter.cofinite)
[PROOFSTEP]
exact ⟨a, hs, Or.inl le_rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
⊢ NoetherianSpace ↑s ↔ ∀ (t : Set α), t ⊆ s → IsCompact t
[PROOFSTEP]
simp only [noetherianSpace_iff_isCompact, embedding_subtype_val.isCompact_iff_isCompact_image,
  Subtype.forall_set_subtype]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), NoetherianSpace ↑(f i)
⊢ NoetherianSpace ↑(⋃ (i : ι), f i)
[PROOFSTEP]
simp_rw [noetherianSpace_set_iff] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι) (t : Set α), t ⊆ f i → IsCompact t
⊢ ∀ (t : Set α), t ⊆ ⋃ (i : ι), f i → IsCompact t
[PROOFSTEP]
intro t ht
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι) (t : Set α), t ⊆ f i → IsCompact t
t : Set α
ht : t ⊆ ⋃ (i : ι), f i
⊢ IsCompact t
[PROOFSTEP]
rw [← Set.inter_eq_left_iff_subset.mpr ht, Set.inter_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι) (t : Set α), t ⊆ f i → IsCompact t
t : Set α
ht : t ⊆ ⋃ (i : ι), f i
⊢ IsCompact (⋃ (i : ι), t ∩ f i)
[PROOFSTEP]
exact isCompact_iUnion fun i => hf i _ (Set.inter_subset_right _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
apply wellFounded_closeds.induction s
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∀ (x : Closeds α),
    (∀ (y : Closeds α), y < x → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S) →
      ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ x = sSup S
[PROOFSTEP]
clear s
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
⊢ ∀ (x : Closeds α),
    (∀ (y : Closeds α), y < x → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S) →
      ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ x = sSup S
[PROOFSTEP]
intro s H
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
rcases eq_or_ne s ⊥ with rfl | h₀
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
H : ∀ (y : Closeds α), y < ⊥ → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ ⊥ = sSup S
[PROOFSTEP]
use∅
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
H : ∀ (y : Closeds α), y < ⊥ → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
⊢ Set.Finite ∅ ∧ (∀ (t : Closeds α), t ∈ ∅ → IsIrreducible ↑t) ∧ ⊥ = sSup ∅
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
by_cases h₁ : IsPreirreducible (s : Set α)
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsPreirreducible ↑s
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
replace h₁ : IsIrreducible (s : Set α) := ⟨Closeds.coe_nonempty.2 h₀, h₁⟩
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsIrreducible ↑s
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
use{ s }
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsIrreducible ↑s
⊢ Set.Finite {s} ∧ (∀ (t : Closeds α), t ∈ {s} → IsIrreducible ↑t) ∧ s = sSup {s}
[PROOFSTEP]
simp [h₁]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : ¬IsPreirreducible ↑s
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
simp only [isPreirreducible_iff_closed_union_closed, not_forall, not_or] at h₁
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : ∃ x x_1 h h h, ¬↑s ⊆ x ∧ ¬↑s ⊆ x_1
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
obtain ⟨z₁, z₂, hz₁, hz₂, h, hz₁', hz₂'⟩ := h₁
[GOAL]
case neg.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ z₂ : Set α
hz₁ : IsClosed z₁
hz₂ : IsClosed z₂
h : ↑s ⊆ z₁ ∪ z₂
hz₁' : ¬↑s ⊆ z₁
hz₂' : ¬↑s ⊆ z₂
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
lift z₁ to Closeds α using hz₁
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₂ : Set α
hz₂ : IsClosed z₂
hz₂' : ¬↑s ⊆ z₂
z₁ : Closeds α
h : ↑s ⊆ ↑z₁ ∪ z₂
hz₁' : ¬↑s ⊆ ↑z₁
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
lift z₂ to Closeds α using hz₂
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
rcases H (s ⊓ z₁) (inf_lt_left.2 hz₁') with ⟨S₁, hSf₁, hS₁, h₁⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : Set.Finite S₁
hS₁ : ∀ (t : Closeds α), t ∈ S₁ → IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
rcases H (s ⊓ z₂) (inf_lt_left.2 hz₂') with ⟨S₂, hSf₂, hS₂, h₂⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : Set.Finite S₁
hS₁ : ∀ (t : Closeds α), t ∈ S₁ → IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : Set.Finite S₂
hS₂ : ∀ (t : Closeds α), t ∈ S₂ → IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
[PROOFSTEP]
refine ⟨S₁ ∪ S₂, hSf₁.union hSf₂, Set.union_subset_iff.2 ⟨hS₁, hS₂⟩, ?_⟩
[GOAL]
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ (y : Closeds α), y < s → ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
S₁ : Set (Closeds α)
hSf₁ : Set.Finite S₁
hS₁ : ∀ (t : Closeds α), t ∈ S₁ → IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : Set.Finite S₂
hS₂ : ∀ (t : Closeds α), t ∈ S₂ → IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = sSup (S₁ ∪ S₂)
[PROOFSTEP]
rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
hs : IsClosed s
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Set α), t ∈ S → IsClosed t) ∧ (∀ (t : Set α), t ∈ S → IsIrreducible t) ∧ s = ⋃₀ S
[PROOFSTEP]
lift s to Closeds α using hs
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Set α), t ∈ S → IsClosed t) ∧ (∀ (t : Set α), t ∈ S → IsIrreducible t) ∧ ↑s = ⋃₀ S
[PROOFSTEP]
rcases NoetherianSpace.exists_finite_set_closeds_irreducible s with ⟨S, hSf, hS, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Set (Closeds α)
hSf : Set.Finite S
hS : ∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t
⊢ ∃ S_1,
    Set.Finite S_1 ∧
      (∀ (t : Set α), t ∈ S_1 → IsClosed t) ∧ (∀ (t : Set α), t ∈ S_1 → IsIrreducible t) ∧ ↑(sSup S) = ⋃₀ S_1
[PROOFSTEP]
refine ⟨(↑) '' S, hSf.image _, Set.ball_image_iff.2 fun S _ => S.2, Set.ball_image_iff.2 hS, ?_⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Set (Closeds α)
hSf : Set.Finite S
hS : ∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t
⊢ ↑(sSup S) = ⋃₀ (SetLike.coe '' S)
[PROOFSTEP]
lift S to Finset (Closeds α) using hSf
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Finset (Closeds α)
hS : ∀ (t : Closeds α), t ∈ ↑S → IsIrreducible ↑t
⊢ ↑(sSup ↑S) = ⋃₀ (SetLike.coe '' ↑S)
[PROOFSTEP]
simp [← Finset.sup_id_eq_sSup, Closeds.coe_finset_sup]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, (∀ (k : { x // x ∈ S }), IsIrreducible ↑↑k) ∧ s = Finset.sup S id
[PROOFSTEP]
simpa [Set.exists_finite_iff_finset, Finset.sup_id_eq_sSup] using
  NoetherianSpace.exists_finite_set_closeds_irreducible s
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
⊢ Set.Finite (irreducibleComponents α)
[PROOFSTEP]
obtain ⟨S : Set (Set α), hSf, hSc, hSi, hSU⟩ :=
  NoetherianSpace.exists_finite_set_isClosed_irreducible isClosed_univ (α := α)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : Set.Finite S
hSc : ∀ (t : Set α), t ∈ S → IsClosed t
hSi : ∀ (t : Set α), t ∈ S → IsIrreducible t
hSU : Set.univ = ⋃₀ S
⊢ Set.Finite (irreducibleComponents α)
[PROOFSTEP]
refine hSf.subset fun s hs => ?_
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : Set.Finite S
hSc : ∀ (t : Set α), t ∈ S → IsClosed t
hSi : ∀ (t : Set α), t ∈ S → IsIrreducible t
hSU : Set.univ = ⋃₀ S
s : Set α
hs : s ∈ irreducibleComponents α
⊢ s ∈ S
[PROOFSTEP]
lift S to Finset (Set α) using hSf
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ (t : Set α), t ∈ ↑S → IsClosed t
hSi : ∀ (t : Set α), t ∈ ↑S → IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
⊢ s ∈ ↑S
[PROOFSTEP]
rcases isIrreducible_iff_sUnion_closed.1 hs.1 S hSc (hSU ▸ Set.subset_univ _) with ⟨t, htS, ht⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ (t : Set α), t ∈ ↑S → IsClosed t
hSi : ∀ (t : Set α), t ∈ ↑S → IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ s ∈ ↑S
[PROOFSTEP]
rwa [ht.antisymm (hs.2 (hSi _ htS) ht)]