-- Mathlib/Topology/NoetherianSpace.lean
theorem NoetherianSpace.exists_open_ne_empty_le_irreducibleComponent [NoetherianSpace α]
    (Z : Set α) (H : Z ∈ irreducibleComponents α) :
    ∃ o : Set α, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z

Proof state:
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
h : a ∈ U
⊢ a ∈ ⋃₀ insert U ι

Tactic:
exact ⟨U, Set.mem_insert _ _, h⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
r : U = ∅
⊢ Z ⊆ ⋃ i, ↑i

Tactic:
rw [Set.diff_eq_empty] at r

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
r : Z ⊆ ⋃ x, ↑x
⊢ Z ⊆ ⋃ i, ↑i

Proof state:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
r : U = ∅
Z' : Set α
hZ' : Z' ∈ hι.toFinset ∧ Z ⊆ Z'
⊢ False

Tactic:
simp only [Set.Finite.mem_toFinset, Set.mem_diff, Set.mem_singleton_iff] at hZ'

Result:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
r : U = ∅
Z' : Set α
hZ' : Z' ∈ ι ∧ Z ⊆ Z'
⊢ False

Proof state:
case neg.inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
h : a ∉ Z
⊢ irreducibleComponent a ∈ irreducibleComponents α ∧ ¬irreducibleComponent a = Z

Tactic:
refine ⟨irreducibleComponent_mem_irreducibleComponents _, ?_⟩

Result:
case neg.inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
h : a ∉ Z
⊢ ¬irreducibleComponent a = Z

Proof state:
case neg.inr.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
i : ↑ι
hi : a ∈ ↑i
⊢ a ∈ ⋃₀ insert U ι

Tactic:
exact ⟨i, Or.inr i.2, hi⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
hU1 : U = (⋃ x, ↑x)ᶜ
⊢ IsClosed (⋃ x, ↑x)

Tactic:
exact isClosed_iUnion_of_finite fun i ↦ isClosed_of_mem_irreducibleComponents i.1 i.2.1

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
⊢ U = Set.univ \ ⋃ x, ↑x

Tactic:
refine le_antisymm (Set.diff_subset_diff le_top <| subset_refl _) ?_

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
⊢ Set.univ \ ⋃ x, ↑x ≤ U

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
hU1 : U = (⋃ x, ↑x)ᶜ
⊢ ∃ o, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z

Tactic:
refine ⟨U, hU1 ▸ isOpen_compl_iff.mpr ?_, hU0, sdiff_le⟩

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
hU1 : U = (⋃ x, ↑x)ᶜ
⊢ IsClosed (⋃ x, ↑x)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
⊢ Set.univ ≤ ⋃₀ insert U ι

Tactic:
rintro a -

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
⊢ a ∈ ⋃₀ insert U ι

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
⊢ a ∈ ⋃₀ insert U ι

Tactic:
by_cases h : a ∈ U

Result:
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
h : a ∈ U
⊢ a ∈ ⋃₀ insert U ι

case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
h : a ∉ U
⊢ a ∈ ⋃₀ insert U ι

Proof state:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
r : U = ∅
Z' : Set α
hZ' : Z' ∈ ι ∧ Z ⊆ Z'
⊢ False

Tactic:
exact hZ'.1.2 <| le_antisymm (H.2 hZ'.1.1.1 hZ'.2) hZ'.2

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
h : a ∉ Z ∨ ∃ i, a ∈ ↑i
⊢ a ∈ ⋃₀ insert U ι

Tactic:
rcases h with (h|⟨i, hi⟩)

Result:
case neg.inl
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
h : a ∉ Z
⊢ a ∈ ⋃₀ insert U ι

case neg.inr.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
a : α
i : ↑ι
hi : a ∈ ↑i
⊢ a ∈ ⋃₀ insert U ι

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
⊢ Set.univ ≤ (⋃ x, ↑x) ∪ U

Tactic:
rw [Set.union_comm, ← Set.sUnion_eq_iUnion, ← Set.sUnion_insert]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
U : Set α := Z \ ⋃ x, ↑x
hU0 : U ≠ ∅
⊢ Set.univ ≤ ⋃₀ insert U ι

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
⊢ Finite ↑ι

Tactic:
rwa [Set.finite_coe_iff]

Result:
no goals