α : Type u_1
β : Type ?u.8780
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
α : Type u_1
β : Type ?u.8780
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Closeds α
⊢ ∃ S, Set.Finite S ∧ (∀ (t : Closeds α), t ∈ S → IsIrreducible ↑t) ∧ s = sSup S
apply wellFounded_closeds.induction s
α : Type u_1
β : Type ?u.8780
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
α : Type u_1
β : Type ?u.8780
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
clear s
α : Type u_1
β : Type ?u.8780
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
α : Type u_1
β : Type ?u.8780
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
intro s H
case inl
α : Type u_1
β : Type ?u.8780
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

case inr
α : Type u_1
β : Type ?u.8780
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
α : Type u_1
β : Type ?u.8780
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
rcases eq_or_ne s ⊥ with rfl | h₀
case inl
α : Type u_1
β : Type ?u.8780
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 ∅
case inl
α : Type u_1
β : Type ?u.8780
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
use ∅
no goals
case inl
α : Type u_1
β : Type ?u.8780
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 ∅
simp
case pos
α : Type u_1
β : Type ?u.8780
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

case neg
α : Type u_1
β : Type ?u.8780
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
case inr
α : Type u_1
β : Type ?u.8780
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
by_cases h₁ : IsPreirreducible (s : Set α)
case pos
α : Type u_1
β : Type ?u.8780
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
case pos
α : Type u_1
β : Type ?u.8780
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
replace h₁ : IsIrreducible (s : Set α) := ⟨Closeds.coe_nonempty.2 h₀, h₁⟩
case pos
α : Type u_1
β : Type ?u.8780
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}
case pos
α : Type u_1
β : Type ?u.8780
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
use {s}
no goals
case pos
α : Type u_1
β : Type ?u.8780
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}
simp [h₁]
case neg
α : Type u_1
β : Type ?u.8780
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
case neg
α : Type u_1
β : Type ?u.8780
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
simp only [isPreirreducible_iff_closed_union_closed, not_forall, not_or] at h₁
case neg.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
case neg
α : Type u_1
β : Type ?u.8780
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
obtain ⟨z₁, z₂, hz₁, hz₂, h, hz₁', hz₂'⟩ := h₁
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
case neg.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
lift z₁ to Closeds α using hz₁
case neg.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
lift z₂ to Closeds α using hz₂
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
case neg.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
rcases H (s ⊓ z₁) (inf_lt_left.2 hz₁') with ⟨S₁, hSf₁, hS₁, h₁⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
rcases H (s ⊓ z₂) (inf_lt_left.2 hz₂') with ⟨S₂, hSf₂, hS₂, h₂⟩
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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₂)
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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
refine ⟨S₁ ∪ S₂, hSf₁.union hSf₂, Set.union_subset_iff.2 ⟨hS₁, hS₂⟩, ?_⟩
no goals
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.8780
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₂)
rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]