awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
z₂ : Closeds α
hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible (↑t : Set α)
h₁ : s ⊓ z₁ = sSup S₁
neg :
  ∀ (S₂ : Set (Closeds α)) (hSf₂ : S₂.Finite) (hS₂ : ∀ t ∈ S₂, IsIrreducible (↑t : Set α)) (h₂ : s ⊓ z₂ = sSup S₂),
    ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S

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

Premises used: Iff.mpr, inf_lt_left, Min.min
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
z₂ : Closeds α
hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible (↑t : Set α)
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible (↑t : Set α)
h₂ : s ⊓ z₂ = sSup S₂
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S

Tactic:
⟨S₁ ∪ S₂, hSf₁.union hSf₂, Set.union_subset_iff.2 ⟨hS₁, hS₂⟩, ?_⟩

Premises used: Iff.mpr, Set.Finite.union, Set.union_subset_iff, And.intro, Exists.intro, Union.union
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
z₂ : Closeds α
hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible (↑t : Set α)
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible (↑t : Set α)
h₂ : s ⊓ z₂ = sSup S₂
neg : s = sSup (S₁ ∪ S₂)
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S

Tactic:
refine ⟨S₁ ∪ S₂, hSf₁.union hSf₂, Set.union_subset_iff.2 ⟨hS₁, hS₂⟩, ?_⟩
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
H : ∀ y < s, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h₀ : s ≠ ⊥
z₁ : Closeds α
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
z₂ : Closeds α
hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)
S₁ : Set (Closeds α)
hSf₁ : S₁.Finite
hS₁ : ∀ t ∈ S₁, IsIrreducible (↑t : Set α)
h₁ : s ⊓ z₁ = sSup S₁
S₂ : Set (Closeds α)
hSf₂ : S₂.Finite
hS₂ : ∀ t ∈ S₂, IsIrreducible (↑t : Set α)
h₂ : s ⊓ z₂ = sSup S₂
neg : s = sSup S₁ ⊔ sSup S₂
neg₁ : s = s ⊓ z₁ ⊔ sSup S₂
neg₂ : s = s ⊓ z₁ ⊔ s ⊓ z₂
neg₃ : s = s ⊓ (z₁ ⊔ z₂)
neg₄ neg₅ neg₆ neg₇ : s ≤ z₁ ⊔ z₂
⊢ s = sSup (S₁ ∪ S₂)

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

Premises used: sSup_union, inf_sup_left, left_eq_inf
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
hs : IsClosed[inst] s
⊢ IsClosed[inst] s

Tactic:
hs
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
hs : IsClosed[inst] s
lift :
  ∀ (s : Closeds α),
    ∃ (S : Set (Set α)), S.Finite ∧ (∀ t ∈ S, IsClosed[inst] t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ (↑s : Set α) = ⋃₀ S
⊢ ∃ (S : Set (Set α)), S.Finite ∧ (∀ t ∈ S, IsClosed[inst] t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ s = ⋃₀ S

Tactic:
lift s to Closeds α using hs

Premises used: TopologicalSpace.Closeds
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
rcases :
  ∀ (S : Set (Closeds α)) (hSf : S.Finite) (hS : ∀ t ∈ S, IsIrreducible (↑t : Set α)),
    ∃ (S_1 : Set (Set α)),
      S_1.Finite ∧ (∀ t ∈ S_1, IsClosed[inst] t) ∧ (∀ t ∈ S_1, IsIrreducible t) ∧ (↑(sSup S) : Set α) = ⋃₀ S_1
⊢ ∃ (S : Set (Set α)), S.Finite ∧ (∀ t ∈ S, IsClosed[inst] t) ∧ (∀ t ∈ S, IsIrreducible t) ∧ (↑s : Set α) = ⋃₀ S

Tactic:
rcases NoetherianSpace.exists_finite_set_closeds_irreducible s with ⟨S, hSf, hS, rfl⟩

Premises used: TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible, rfl
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible (↑t : Set α)
⊢ ∃ (S_1 : Set (Set α)),
    S_1.Finite ∧ (∀ t ∈ S_1, IsClosed[inst] t) ∧ (∀ t ∈ S_1, IsIrreducible t) ∧ (↑(sSup S) : Set α) = ⋃₀ S_1

Tactic:
⟨(↑) '' S, hSf.image _, Set.forall_mem_image.2 fun S _ ↦ S.2, Set.forall_mem_image.2 hS,
    ?_⟩

Premises used: Iff.mpr, Set.Finite.image, And.intro, Exists.intro, Set.image, Set.forall_mem_image
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible (↑t : Set α)
refine : (↑(sSup S) : Set α) = ⋃₀ (SetLike.coe '' S)
⊢ ∃ (S_1 : Set (Set α)),
    S_1.Finite ∧ (∀ t ∈ S_1, IsClosed[inst] t) ∧ (∀ t ∈ S_1, IsIrreducible t) ∧ (↑(sSup S) : Set α) = ⋃₀ S_1

Tactic:
refine ⟨(↑) '' S, hSf.image _, Set.forall_mem_image.2 fun S _ ↦ S.2, Set.forall_mem_image.2 hS,
    ?_⟩
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible (↑t : Set α)
⊢ S.Finite

Tactic:
hSf
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Closeds α)
hSf : S.Finite
hS : ∀ t ∈ S, IsIrreducible (↑t : Set α)
lift :
  ∀ (S : Finset (Closeds α)) (hS : ∀ t ∈ (↑S : Set (Closeds α)), IsIrreducible (↑t : Set α)),
    (↑(sSup (↑S : Set (Closeds α))) : Set α) = ⋃₀ (SetLike.coe '' (↑S : Set (Closeds α)))
⊢ (↑(sSup S) : Set α) = ⋃₀ (SetLike.coe '' S)

Tactic:
lift S to Finset (Closeds α) using hSf

Premises used: Finset, TopologicalSpace.Closeds
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Finset (Closeds α)
hS : ∀ t ∈ (↑S : Set (Closeds α)), IsIrreducible (↑t : Set α)
⊢ (↑(sSup (↑S : Set (Closeds α))) : Set α) = ⋃₀ (SetLike.coe '' (↑S : Set (Closeds α)))

Tactic:
simp [← Finset.sup_id_eq_sSup, Closeds.coe_finset_sup]

Premises used: TopologicalSpace.Closeds.coe_finset_sup, Finset.sup_id_eq_sSup
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
⊢ ∃ (S : Finset (Closeds α)), (∀ (k : ↥S), IsIrreducible (↑(↑k : Closeds α) : Set α)) ∧ s = S.sup id

Tactic:
simpa [Set.exists_finite_iff_finset, Finset.sup_id_eq_sSup]
    using NoetherianSpace.exists_finite_set_closeds_irreducible s

Premises used: TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible, Set.exists_finite_iff_finset, Finset.sup_id_eq_sSup
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
obtain :
  ∀ (S : Set (Set α)) (hSf : S.Finite) (hSc : ∀ t ∈ S, IsClosed[inst] t) (hSi : ∀ t ∈ S, IsIrreducible t)
    (hSU : Set.univ = ⋃₀ S), (irreducibleComponents α).Finite
⊢ (irreducibleComponents α).Finite

Tactic:
obtain ⟨S : Set (Set α), hSf, hSc, hSi, hSU⟩ :=
    NoetherianSpace.exists_finite_set_isClosed_irreducible isClosed_univ (α := α)

Premises used: isClosed_univ, TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible, Set
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed[inst] t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
⊢ (irreducibleComponents α).Finite

Tactic:
hSf.subset fun s hs => ?_

Premises used: Set.Finite.subset
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed[inst] t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
refine : ∀ (s : Set α) (hs : s ∈ irreducibleComponents α), s ∈ S
⊢ (irreducibleComponents α).Finite

Tactic:
refine hSf.subset fun s hs => ?_

Premises used: Set.Finite.subset
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed[inst] t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
s : Set α
hs : s ∈ irreducibleComponents α
⊢ S.Finite

Tactic:
hSf
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
S : Set (Set α)
hSf : S.Finite
hSc : ∀ t ∈ S, IsClosed[inst] t
hSi : ∀ t ∈ S, IsIrreducible t
hSU : Set.univ = ⋃₀ S
s : Set α
hs : s ∈ irreducibleComponents α
lift :
  ∀ (S : Finset (Set α)) (hSc : ∀ t ∈ (↑S : Set (Set α)), IsClosed[inst] t)
    (hSi : ∀ t ∈ (↑S : Set (Set α)), IsIrreducible t) (hSU : Set.univ = ⋃₀ (↑S : Set (Set α))), s ∈ (↑S : Set (Set α))
⊢ s ∈ S

Tactic:
lift S to Finset (Set α) using hSf

Premises used: Finset, Set
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ (↑S : Set (Set α)), IsClosed[inst] t
hSi : ∀ t ∈ (↑S : Set (Set α)), IsIrreducible t
hSU : Set.univ = ⋃₀ (↑S : Set (Set α))
rcases : ∀ (t : Set α) (htS : t ∈ S) (ht : s ⊆ t), s ∈ (↑S : Set (Set α))
⊢ s ∈ (↑S : Set (Set α))

Tactic:
rcases isIrreducible_iff_sUnion_isClosed.1 hs.1 S hSc (hSU ▸ Set.subset_univ _) with ⟨t, htS, ht⟩

Premises used: isIrreducible_iff_sUnion_isClosed, Set.subset_univ, Eq.rec, And.left, Iff.mp
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ t ∈ (↑S : Set (Set α)), IsClosed[inst] t
hSi : ∀ t ∈ (↑S : Set (Set α)), IsIrreducible t
hSU : Set.univ = ⋃₀ (↑S : Set (Set α))
t : Set α
htS : t ∈ S
ht : s ⊆ t
rwa rwa₁ rwa₂ rwa₃ : t ∈ (↑S : Set (Set α))
⊢ s ∈ (↑S : Set (Set α))

Tactic:
rwa [ht.antisymm (hs.2 (hSi _ htS) ht)]

Premises used: And.right, HasSubset.Subset.antisymm
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
⊢ (irreducibleComponents α).Finite

Tactic:
have hα : (irreducibleComponents α).Finite := finite_irreducibleComponents
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
⊢ closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z

Tactic:
have hZ := closure_sUnion_irreducibleComponents_diff_singleton hα Z H
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
⊢ ∃ (o : Set α), IsOpen[inst] o ∧ o.Nonempty ∧ o ⊆ Z

Tactic:
⟨(⋃₀ (irreducibleComponents α \ {Z}))ᶜ, ?_, ?_, subset_closure.trans hZ.le⟩

Premises used: irreducibleComponents, subset_closure, Compl.compl, Set.sUnion, HasSubset.Subset.trans, Eq.le, SDiff.sdiff, And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
refine_1 : IsOpen[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ
refine_2 : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ.Nonempty
⊢ ∃ (o : Set α), IsOpen[inst] o ∧ o.Nonempty ∧ o ⊆ Z

Tactic:
refine ⟨(⋃₀ (irreducibleComponents α \ {Z}))ᶜ, ?_, ?_, subset_closure.trans hZ.le⟩
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
refine_1 : IsClosed[inst] (⋃ i ∈ irreducibleComponents α \ {Z}, i)
⊢ IsOpen[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ

Tactic:
rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]

Premises used: Set.sUnion_eq_biUnion, isOpen_compl_iff
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
⊢ IsClosed[inst] (⋃ i ∈ irreducibleComponents α \ {Z}, i)

Tactic:
hα.diff.isClosed_biUnion fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Premises used: isClosed_of_mem_irreducibleComponents, Set.Finite.diff, And.left, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
⊢ IsClosed[inst] (⋃ i ∈ irreducibleComponents α \ {Z}, i)

Tactic:
exact hα.diff.isClosed_biUnion fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Premises used: isClosed_of_mem_irreducibleComponents, Set.Finite.diff, And.left, Set.Finite.isClosed_biUnion
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = Z
refine_2 : ∀ (hZ : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = ∅), closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ ≠ Z
⊢ (⋃₀ (irreducibleComponents α \ {Z}))ᶜ.Nonempty

Tactic:
contrapose! hZ
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = ∅
refine_2 : Z.Nonempty
⊢ closure[inst] (⋃₀ (irreducibleComponents α \ {Z}))ᶜ ≠ Z

Tactic:
rw [hZ, closure_empty, ← Set.nonempty_iff_empty_ne]

Premises used: Set.nonempty_iff_empty_ne, closure_empty
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = ∅
⊢ Z.Nonempty

Tactic:
H.1.nonempty

Premises used: IsIrreducible.nonempty, And.left
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
hα : (irreducibleComponents α).Finite
hZ : (⋃₀ (irreducibleComponents α \ {Z}))ᶜ = ∅
⊢ Z.Nonempty

Tactic:
exact H.1.nonempty

Premises used: IsIrreducible.nonempty, And.left
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
Z : Set α
H : Z ∈ irreducibleComponents α
⊢ ∃ (o : Set α), IsOpen[inst] o ∧ o.Nonempty ∧ o ≤ Z

Tactic:
simpa using exists_isOpen_nonempty_subset_irreducibleComponent Z H

Premises used: TopologicalSpace.NoetherianSpace.exists_isOpen_nonempty_subset_irreducibleComponent
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
W V : Set α
inst_1 : NoetherianSpace.{u_1} (↑W : Type u_1)
h : V ⊆ W
⊢ NoetherianSpace.{u_1} (↑V : Type u_1)

Tactic:
Topology.IsInducing.noetherianSpace (Topology.IsEmbedding.inclusion h).isInducing

Premises used: Topology.IsInducing.noetherianSpace, Topology.IsEmbedding.inclusion, Topology.IsEmbedding.isInducing
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
W V : Set α
inst_1 : NoetherianSpace.{u_1} (↑W : Type u_1)
⊢ NoetherianSpace.{u_1} (↑(W ∩ V) : Type u_1)

Tactic:
.of_subset Set.inter_subset_left

Premises used: Set.inter_subset_left, TopologicalSpace.NoetherianSpace.of_subset
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
W V : Set α
inst_1 : NoetherianSpace.{u_1} (↑V : Type u_1)
⊢ NoetherianSpace.{u_1} (↑(W ∩ V) : Type u_1)

Tactic:
.of_subset Set.inter_subset_right

Premises used: TopologicalSpace.NoetherianSpace.of_subset, Set.inter_subset_right
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α))
f : α → Prop
a b : α
hab : a ≤ b
h : Eq (α := Set α) ((fun (c : Chain α) ↦ (range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) (Chain.pair a b hab)) {a, b}
⊢ Membership.mem (γ := Set (Set α)) (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α)) {a, b}

Tactic:
use Chain.pair a b hab

Premises used: OmegaCompletePartialOrder.Chain.pair
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α))
f : α → Prop
a b : α
hab : a ≤ b
⊢ Eq (α := Set α) ((fun (c : Chain α) ↦ (range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) (Chain.pair a b hab)) {a, b}

Tactic:
OmegaCompletePartialOrder.Chain.range_pair a b hab

Premises used: OmegaCompletePartialOrder.Chain.range_pair
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α))
f : α → Prop
a b : α
hab : a ≤ b
⊢ Eq (α := Set α) ((fun (c : Chain α) ↦ (range (ι := ℕ) (⇑c : (a : ℕ) → α) : Set α)) (Chain.pair a b hab)) {a, b}

Tactic:
exact OmegaCompletePartialOrder.Chain.range_pair a b hab

Premises used: OmegaCompletePartialOrder.Chain.range_pair
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α))
f : α → Prop
rw : ScottContinuousOn (range fun (c : Chain α) ↦ range (ι := ℕ) (⇑c : (a : ℕ) → α)) f ↔ Continuous[inst_1, _] f
rw₁ rw₂ : Continuous[inst_1, _] f ↔ Continuous[inst_1, _] f
⊢ ωScottContinuous f ↔ Continuous[inst_1, _] f

Tactic:
rw [ωScottContinuous, scottContinuousOn_iff_continuous (fun a b hab => by
    use Chain.pair a b hab; exact OmegaCompletePartialOrder.Chain.range_pair a b hab)]

Premises used: Topology.IsScott.scottContinuousOn_iff_continuous, OmegaCompletePartialOrder.ωScottContinuous
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u
inst : Preorder α
c : Chain α
x : α
⊢ IsωSup c x ↔ IsLUB (range (ι := ℕ) (⇑c : (a : ℕ) → α)) x

Tactic:
simp [IsωSup, IsLUB, IsLeast, upperBounds, lowerBounds]

Premises used: lowerBounds, upperBounds, IsLeast, IsLUB, Scott.IsωSup
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u
inst : OmegaCompletePartialOrder α
⊢ IsOpen α univ

Tactic:
@CompleteLattice.ωScottContinuous.top α Prop _ _

Premises used: Set.Mem, Set.univ, setOf, CompleteLattice.ωScottContinuous.top, Scott.IsOpen
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u
inst : OmegaCompletePartialOrder α
s t : Set α
⊢ IsOpen α s → IsOpen α t → IsOpen α (s ∩ t)

Tactic:
CompleteLattice.ωScottContinuous.inf

Premises used: Set.Mem, setOf, Set.inter, CompleteLattice.ωScottContinuous.inf, Scott.IsOpen
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u
inst : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous (β := Prop) fun (x : α) ↦ x ∈ t
⊢ ωScottContinuous (sSup s)

Tactic:
CompleteLattice.ωScottContinuous.sSup hs

Premises used: CompleteLattice.ωScottContinuous.sSup
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u
inst : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous (β := Prop) fun (x : α) ↦ x ∈ t
h : ∀ (x : α), Membership.mem (⋃₀ s) = sSup s
⊢ ωScottContinuous (β := Prop) fun (x : α) ↦ x ∈ ⋃₀ s

Tactic:
convert! CompleteLattice.ωScottContinuous.sSup hs

Premises used: CompleteLattice.ωScottContinuous.sSup
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u
inst : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, ωScottContinuous (β := Prop) fun (x : α) ↦ x ∈ t
x : α
⊢ Membership.mem (⋃₀ s) = sSup s

Tactic:
aesop
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u
inst : OmegaCompletePartialOrder α
s : Set α
hs : IsOpen α s
⊢ IsUpperSet s

Tactic:
hs.monotone

Premises used: Monotone, IsUpperSet, OmegaCompletePartialOrder.ωScottContinuous.monotone
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
c : Chain α
left : ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ ωSup c
right : ∀ (y : α), (∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ y) → ωSup c ≤ y
⊢ IsωSup c (ωSup c)

Tactic:
constructor
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ ωSup c

Tactic:
apply le_ωSup

Premises used: OmegaCompletePartialOrder.le_ωSup
-- Module: Mathlib.Topology.OmegaCompletePartialOrder
Goal:
α : Type u_1
inst : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (y : α), (∀ (i : ℕ), (c : (a : ℕ) → α) i ≤ y) → ωSup c ≤ y

Tactic:
apply ωSup_le

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ toPartialEquiv (OpenPartialHomeomorph.refl X) = PartialEquiv.refl X

Tactic:
rfl

Premises used: Equiv.toPartialEquivOfImageEq, Equiv.toPartialEquiv, Equiv.refl, PartialEquiv.refl, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Eq (α := OpenPartialHomeomorph X X) (OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl X))
    (OpenPartialHomeomorph.refl X)

Tactic:
rfl

Premises used: Equiv.toPartialEquivOfImageEq, Homeomorph.toOpenPartialHomeomorphOfImageEq, Set.univ, setOf, PartialEquiv.symm, rfl, OpenPartialHomeomorph.symm, Homeomorph.toOpenPartialHomeomorph, OpenPartialHomeomorph.refl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.source ⊆ (↑e : X → Y) ⁻¹' e.target

Tactic:
e.mapsTo

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.MapsTo, OpenPartialHomeomorph.mapsTo
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
h : s ⊆ e.source
⊢ (↑e : X → Y) '' s = e.target ∩ (↑e.symm : Y → X) ⁻¹' s

Tactic:
e.toPartialEquiv.image_eq_target_inter_inv_preimage h

Premises used: PartialEquiv.image_eq_target_inter_inv_preimage, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.toPartialEquiv
-- Module: Mathlib.Topology.OpenPartialHomeomorph.Basic
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
⊢ (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ (↑e.symm : Y → X) ⁻¹' s

Tactic:
e.toPartialEquiv.image_source_inter_eq' s

Premises used: OpenPartialHomeomorph.toFun', PartialEquiv.image_source_inter_eq', OpenPartialHomeomorph.toPartialEquiv