-- Mathlib/Topology/NoetherianSpace.lean
theorem NoetherianSpace.exists_finite_set_closeds_irreducible [NoetherianSpace α] (s : Closeds α) :
    ∃ S : Set (Closeds α), S.Finite ∧ (∀ t ∈ S, IsIrreducible (t : Set α)) ∧ s = sSup S

Proof state:
case neg.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
rcases H (s ⊓ z₁) (inf_lt_left.2 hz₁') with ⟨S₁, hSf₁, hS₁, h₁⟩

Result:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ 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₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Proof state:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
by_cases h₁ : IsPreirreducible (s : Set α)

Result:
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsPreirreducible ↑s
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : ¬IsPreirreducible ↑s
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Proof state:
case neg.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ 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, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
lift z₁ to Closeds α using hz₁

Result:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ 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, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Proof state:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∅.Finite ∧ (∀ t ∈ ∅, IsIrreducible ↑t) ∧ ⊥ = sSup ∅

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsIrreducible ↑s
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
use {s}

Result:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsIrreducible ↑s
⊢ {s}.Finite ∧ (∀ t ∈ {s}, IsIrreducible ↑t) ∧ s = sSup {s}

Proof state:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ 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₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible ↑t
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible ↑t
h₂ : s ⊓ z₂ = sSup S₂
⊢ s = sSup (S₁ ∪ S₂)

Tactic:
rwa [sSup_union, ← h₁, ← h₂, ← inf_sup_left, left_eq_inf]

Result:
no goals

Proof state:
case neg.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ 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, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
lift z₂ to Closeds α using hz₂

Result:
case neg.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬↑s ⊆ ↑z₁
z₂ : Closeds α
hz₂' : ¬↑s ⊆ ↑z₂
h : ↑s ⊆ ↑z₁ ∪ ↑z₂
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Proof state:
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsPreirreducible ↑s
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
replace h₁ : IsIrreducible (s : Set α) := ⟨Closeds.coe_nonempty.2 h₀, h₁⟩

Result:
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsIrreducible ↑s
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Proof state:
case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ ⊥ = sSup S

Tactic:
use ∅

Result:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∅.Finite ∧ (∀ t ∈ ∅, IsIrreducible ↑t) ∧ ⊥ = sSup ∅

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Tactic:
rcases eq_or_ne s ⊥ with rfl | h₀

Result:
case inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
H : ∀ y < ⊥, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ ⊥ = sSup S

case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
⊢ ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ s = sSup S

Proof state:
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ S, S.Finite ∧ (∀ t ∈ S, IsIrreducible ↑t) ∧ y = sSup S
h₀ : s ≠ ⊥
h₁ : IsIrreducible ↑s
⊢ {s}.Finite ∧ (∀ t ∈ {s}, IsIrreducible ↑t) ∧ s = sSup {s}

Tactic:
simp [h₁]

Result:
no goals