-- 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:
α : 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 = (⋃ x, ↑x)ᶜ

Tactic:
rw [Set.compl_eq_univ_diff]

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 ≠ ∅
⊢ U = Set.univ \ ⋃ 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
r : U = ∅
z : Set α
hz : z ∈ ι
⊢ IsClosed z

Tactic:
exact isClosed_of_mem_irreducibleComponents _ hz.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 ≠ ∅
⊢ Set.univ \ ⋃ x, ↑x ≤ U

Tactic:
rw [← Set.compl_eq_univ_diff]

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

Tactic:
have hU0 : U ≠ ∅ := fun r ↦ by
  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)
  simp only [Set.Finite.mem_toFinset, Set.mem_diff, Set.mem_singleton_iff] at hZ'
  exact hZ'.1.2 <| le_antisymm (H.2 hZ'.1.1.1 hZ'.2) hZ'.2

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 ≠ ∅
⊢ ∃ 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 ⊆ ⋃₀ ↑hι.toFinset

Tactic:
rw [Set.Finite.coe_toFinset, Set.sUnion_eq_iUnion]

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 ⊆ ⋃ i, ↑i