case intro
α : Type u_1
β : Type ?u.13042
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
α : Type u_1
β : Type ?u.13042
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
lift s to Closeds α using hs
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.13042
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
case intro
α : Type u_1
β : Type ?u.13042
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
rcases NoetherianSpace.exists_finite_set_closeds_irreducible s with ⟨S, hSf, hS, rfl⟩
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.13042
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)
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.13042
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
refine ⟨(↑) '' S, hSf.image _, Set.ball_image_iff.2 fun S _ => S.2, Set.ball_image_iff.2 hS, ?_⟩
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.13042
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Finset (Closeds α)
hS : ∀ (t : Closeds α), t ∈ ↑S → IsIrreducible ↑t
⊢ ↑(sSup ↑S) = ⋃₀ (SetLike.coe '' ↑S)
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.13042
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)
lift S to Finset (Closeds α) using hSf
no goals
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.13042
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Finset (Closeds α)
hS : ∀ (t : Closeds α), t ∈ ↑S → IsIrreducible ↑t
⊢ ↑(sSup ↑S) = ⋃₀ (SetLike.coe '' ↑S)
simp [← Finset.sup_id_eq_sSup, Closeds.coe_finset_sup]