-- 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 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

Tactic:
rintro rfl

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

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
⊢ ∃ o, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z

Tactic:
have hι : ι.Finite := NoetherianSpace.finite_irreducibleComponents.subset Set.diff_subset

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
⊢ ∃ o, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z

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 : Set α
hz : z ∈ hι.toFinset
⊢ IsClosed z

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

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 : U = ∅
z : Set α
hz : z ∈ ι
⊢ IsClosed z

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 = ∅
⊢ False

Tactic:
obtain ⟨Z', hZ'⟩ := isIrreducible_iff_sUnion_isClosed.mp H.1 hι.toFinset
  (fun z hz ↦ by
    simp only [Set.Finite.mem_toFinset, Set.mem_diff, Set.mem_singleton_iff] at hz
    exact isClosed_of_mem_irreducibleComponents _ hz.1)
  (by
    rw [Set.Finite.coe_toFinset, Set.sUnion_eq_iUnion]
    rw [Set.diff_eq_empty] at r
    exact r)

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' ∈ hι.toFinset ∧ 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 ∈ ι

Tactic:
simp only [ι, Set.mem_diff, Set.mem_singleton_iff]

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 ∈ irreducibleComponents α ∧ ¬irreducibleComponent a = Z

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 ≠ ∅
⊢ (⋃ x, ↑x)ᶜ ≤ U

Tactic:
refine Set.compl_subset_iff_union.mpr (le_antisymm le_top ?_)

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:
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 ι

Tactic:
refine ⟨irreducibleComponent a, Or.inr ?_, mem_irreducibleComponent⟩

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 ∈ ι

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

Tactic:
let U := Z \ ⋃ (x : ι), x

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
⊢ ∃ o, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z

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 : Z ⊆ ⋃ x, ↑x
⊢ Z ⊆ ⋃ i, ↑i

Tactic:
exact r

Result:
no goals

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

Tactic:
exact h mem_irreducibleComponent

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 ∉ U
⊢ a ∈ ⋃₀ insert U ι

Tactic:
rw [Set.mem_diff, Decidable.not_and_iff_or_not_not, not_not, Set.mem_iUnion] at h

Result:
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 ι

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

Tactic:
have hι' : Finite ι := by rwa [Set.finite_coe_iff]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
hι : ι.Finite
hι' : Finite ↑ι
⊢ ∃ o, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
⊢ ∃ o, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z

Tactic:
let ι : Set (Set α) := irreducibleComponents α \ {Z}

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
ι : Set (Set α) := irreducibleComponents α \ {Z}
⊢ ∃ o, IsOpen o ∧ o ≠ ∅ ∧ o ≤ Z