awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
⊢ NoetherianSpace α

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
⊢ ∀ (s : Opens α), IsCompact (↑s : Set α)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)

Tactic:
1 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)

Tactic:
tfae_have 1 ↔ 4 := noetherianSpace_iff_opens α

Premises used: TopologicalSpace.noetherianSpace_iff_opens
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
⊢ NoetherianSpace α

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
⊢ ∀ (s : Set α), IsCompact s

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
⊢ ∀ (a : NoetherianSpace α) (s : Set α), IsCompact s

Tactic:
1 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
⊢ ∀ (a : NoetherianSpace α) (s : Set α), IsCompact s

Tactic:
tfae_have 1 → 3 := @NoetherianSpace.isCompact α _

Premises used: TopologicalSpace.NoetherianSpace.isCompact
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
tfae_1_to_3 : ∀ (a : NoetherianSpace α) (s : Set α), IsCompact s
⊢ ∀ (s : Set α), IsCompact s

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
tfae_1_to_3 : ∀ (a : NoetherianSpace α) (s : Set α), IsCompact s
⊢ ∀ (s : Opens α), IsCompact (↑s : Set α)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
tfae_1_to_3 : ∀ (a : NoetherianSpace α) (s : Set α), IsCompact s
⊢ ∀ (a : ∀ (s : Set α), IsCompact s) (s : Opens α), IsCompact (↑s : Set α)

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
tfae_1_to_3 : ∀ (a : NoetherianSpace α) (s : Set α), IsCompact s
⊢ ∀ (a : ∀ (s : Set α), IsCompact s) (s : Opens α), IsCompact (↑s : Set α)

Tactic:
tfae_have 3 → 4 := fun h s => h s
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
tfae_1_to_3 : ∀ (a : NoetherianSpace α) (s : Set α), IsCompact s
tfae_3_to_4 : ∀ (a : ∀ (s : Set α), IsCompact s) (s : Opens α), IsCompact (↑s : Set α)
⊢ [NoetherianSpace α, WellFoundedLT.{u_1} (Closeds α), ∀ (s : Set α), IsCompact s,
      ∀ (s : Opens α), IsCompact (↑s : Set α)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ NoetherianSpace α ↔ ∀ (s : Set α), IsCompact s

Tactic:
(noetherianSpace_TFAE α).out 0 2

Premises used: TopologicalSpace.noetherianSpace_TFAE, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : NoetherianSpace α
⊢ WellFoundedLT.{u_1} (Closeds α)

Tactic:
Iff.mp ((noetherianSpace_TFAE α).out 0 1) ‹_›

Premises used: TopologicalSpace.noetherianSpace_TFAE, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α_1 : Type u_1
β : Type u_2
inst : TopologicalSpace α_1
inst_1 : TopologicalSpace β
α : Type u_3
simp :
  ∀ (s : Set (CofiniteTopology α)) (f : Ultrafilter (CofiniteTopology α)),
    s ∈ (↑f : Filter (CofiniteTopology α)) →
      ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
⊢ NoetherianSpace.{u_3} (CofiniteTopology α)

Tactic:
simp only [noetherianSpace_iff_isCompact, isCompact_iff_ultrafilter_le_nhds,
    CofiniteTopology.nhds_eq, Ultrafilter.le_sup_iff, Filter.le_principal_iff]

Premises used: Filter.le_principal_iff, Ultrafilter.le_sup_iff, CofiniteTopology.nhds_eq, isCompact_iff_ultrafilter_le_nhds, TopologicalSpace.noetherianSpace_iff_isCompact
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α_1 : Type u_1
β : Type u_2
inst : TopologicalSpace α_1
inst_1 : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ (↑f : Filter (CofiniteTopology α))
inl :
  ∀ (hf : (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite),
    ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
inr :
  ∀ (a : CofiniteTopology α) (hs : s ∈ (↑(pure a) : Filter (CofiniteTopology α))),
    ∃ x ∈ s,
      (↑(pure a) : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑(pure a) : Filter (CofiniteTopology α)) ≤ Filter.cofinite
⊢ ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite

Tactic:
rcases f.le_cofinite_or_eq_pure with (hf | ⟨a, rfl⟩)

Premises used: Ultrafilter.le_cofinite_or_eq_pure, rfl
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α_1 : Type u_1
β : Type u_2
inst : TopologicalSpace α_1
inst_1 : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ (↑f : Filter (CofiniteTopology α))
hf : (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
inl :
  ∀ (a : CofiniteTopology α) (ha : a ∈ s),
    ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
⊢ ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite

Tactic:
rcases Filter.nonempty_of_mem hs with ⟨a, ha⟩

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α_1 : Type u_1
β : Type u_2
inst : TopologicalSpace α_1
inst_1 : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ (↑f : Filter (CofiniteTopology α))
hf : (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
a : CofiniteTopology α
ha : a ∈ s
⊢ ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite

Tactic:
⟨a, ha, Or.inr hf⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α_1 : Type u_1
β : Type u_2
inst : TopologicalSpace α_1
inst_1 : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
f : Ultrafilter (CofiniteTopology α)
hs : s ∈ (↑f : Filter (CofiniteTopology α))
hf : (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
a : CofiniteTopology α
ha : a ∈ s
⊢ ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite

Tactic:
exact ⟨a, ha, Or.inr hf⟩
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α_1 : Type u_1
β : Type u_2
inst : TopologicalSpace α_1
inst_1 : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
a : CofiniteTopology α
hs : s ∈ (↑(pure a) : Filter (CofiniteTopology α))
⊢ ∃ x ∈ s,
    (↑(pure a) : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑(pure a) : Filter (CofiniteTopology α)) ≤ Filter.cofinite

Tactic:
⟨a, hs, Or.inl le_rfl⟩

Premises used: le_rfl, And.intro, Exists.intro, Or.inl
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α_1 : Type u_1
β : Type u_2
inst : TopologicalSpace α_1
inst_1 : TopologicalSpace β
α : Type u_3
s : Set (CofiniteTopology α)
a : CofiniteTopology α
hs : s ∈ (↑(pure a) : Filter (CofiniteTopology α))
⊢ ∃ x ∈ s,
    (↑(pure a) : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑(pure a) : Filter (CofiniteTopology α)) ≤ Filter.cofinite

Tactic:
exact ⟨a, hs, Or.inl le_rfl⟩
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : NoetherianSpace α
f : α → β
hf : Continuous[inst, inst_1] f
hf' : Function.Surjective f
⊢ NoetherianSpace β

Tactic:
noetherianSpace_iff_isCompact.2 <| (Set.image_surjective.mpr hf').forall.2 fun s =>
    (NoetherianSpace.isCompact s).image hf

Premises used: Iff.mpr, Function.Surjective.forall, Set.image_surjective, IsCompact.image, TopologicalSpace.noetherianSpace_iff_isCompact, TopologicalSpace.NoetherianSpace.isCompact
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
⊢ NoetherianSpace α ↔ NoetherianSpace β

Tactic:
⟨fun _ => noetherianSpace_of_surjective f f.continuous f.surjective,
    fun _ => noetherianSpace_of_surjective f.symm f.symm.continuous f.symm.surjective⟩

Premises used: Homeomorph.continuous, TopologicalSpace.noetherianSpace_of_surjective, Homeomorph.symm, Iff.intro, Homeomorph.surjective, DFunLike.coe
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : NoetherianSpace α
f : α → β
hf : Continuous[inst, inst_1] f
⊢ NoetherianSpace.{u_2} (↑(Set.range f) : Type u_2)

Tactic:
noetherianSpace_of_surjective (Set.rangeFactorization f) (hf.subtype_mk _)
    Set.rangeFactorization_surjective

Premises used: TopologicalSpace.noetherianSpace_of_surjective, Continuous.subtype_mk, Set.rangeFactorization_surjective, Set.rangeFactorization
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
⊢ NoetherianSpace.{u_1} (↑s : Type u_1) ↔ ∀ t ⊆ s, IsCompact t

Tactic:
simp only [noetherianSpace_iff_isCompact, IsEmbedding.subtypeVal.isCompact_iff,
    Subtype.forall_set_subtype]

Premises used: Topology.IsEmbedding.isCompact_iff, Subtype.forall_set_subtype, Topology.IsEmbedding.subtypeVal, TopologicalSpace.noetherianSpace_iff_isCompact
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ NoetherianSpace.{u_1} (↑Set.univ : Type u_1) ↔ NoetherianSpace α

Tactic:
noetherianSpace_iff_of_homeomorph (Homeomorph.Set.univ α)

Premises used: Homeomorph.Set.univ, TopologicalSpace.noetherianSpace_iff_of_homeomorph
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst_1 : Finite ι
hf : ∀ (i : ι), NoetherianSpace.{u_1} (↑(f i) : Type u_1)
simp_rw : ∀ (hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t), ∀ t ⊆ ⋃ (i : ι), f i, IsCompact t
⊢ NoetherianSpace.{u_1} (↑(⋃ (i : ι), f i) : Type u_1)

Tactic:
simp_rw [noetherianSpace_set_iff] at hf ⊢

Premises used: TopologicalSpace.noetherianSpace_set_iff
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst_1 : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ (i : ι), f i
rw : IsCompact.{u_1} (X := α) (⋃ (i : ι), t ∩ f i)
⊢ IsCompact t

Tactic:
rw [← Set.inter_eq_left.mpr ht, Set.inter_iUnion]

Premises used: Set.inter_eq_left, Iff.mpr, Set.inter_iUnion
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst_1 : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ (i : ι), f i
⊢ IsCompact.{u_1} (X := α) (⋃ (i : ι), t ∩ f i)

Tactic:
isCompact_iUnion fun i => hf i _ Set.inter_subset_right

Premises used: Inter.inter, isCompact_iUnion, Set.inter_subset_right
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst_1 : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ (i : ι), f i
⊢ IsCompact.{u_1} (X := α) (⋃ (i : ι), t ∩ f i)

Tactic:
exact isCompact_iUnion fun i => hf i _ Set.inter_subset_right

Premises used: Inter.inter, isCompact_iUnion, Set.inter_subset_right
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
inst_2 : T2Space α
⊢ DiscreteTopology α

Tactic:
⟨eq_bot_iff.mpr fun _ _ => isClosed_compl_iff.mp (NoetherianSpace.isCompact _).isClosed⟩

Premises used: Iff.mpr, Compl.compl, DiscreteTopology.mk, Iff.mp, eq_bot_iff, TopologicalSpace.NoetherianSpace.isCompact, IsCompact.isClosed, isClosed_compl_iff
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
inst_2 : T2Space α
⊢ Finite α

Tactic:
Finite.of_finite_univ (NoetherianSpace.isCompact Set.univ).finite_of_discrete

Premises used: Set.univ, IsCompact.finite_of_discrete, TopologicalSpace.NoetherianSpace.isCompact, Finite.of_finite_univ
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : Finite α
⊢ NoetherianSpace α

Tactic:
⟨Finite.wellFounded_of_trans_of_irrefl _⟩

Premises used: IsWellFounded.mk, Finite.wellFounded_of_trans_of_irrefl
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : IndiscreteTopology α
⊢ NoetherianSpace α

Tactic:
noetherianSpace_of_surjective CofiniteTopology.of.symm continuous_of_indiscreteTopology
    CofiniteTopology.of.symm.surjective

Premises used: TopologicalSpace.noetherianSpace_of_surjective, continuous_of_indiscreteTopology, CofiniteTopology.of, Equiv.surjective, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
apply :
  ∀ (x : Closeds α),
    (∀ y < x, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S) →
      ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ x = sSup S
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S

Tactic:
apply wellFounded_lt.induction s

Premises used: WellFounded.induction, wellFounded_lt
-- 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
inl :
  ∀ (H : ∀ y < ⊥, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S),
    ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ ⊥ = sSup S
inr : ∀ (h₀ : 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 eq_or_ne s ⊥ with rfl | h₀

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
H : ∀ y < ⊥, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
h :
  Set.Finite.{u_1} (α := Closeds α) ∅ ∧
    (∀ (t : Closeds α), Membership.mem (γ := Set (Closeds α)) ∅ t → IsIrreducible (↑t : Set α)) ∧
      Eq.{u_1 + 1} (α := Closeds α) ⊥ (sSup ∅)
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ ⊥ = sSup S

Tactic:
use ∅
-- Module: Mathlib.Topology.NoetherianSpace
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
H : ∀ y < ⊥, ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ y = sSup S
⊢ Set.Finite.{u_1} (α := Closeds α) ∅ ∧
    (∀ (t : Closeds α), Membership.mem (γ := Set (Closeds α)) ∅ t → IsIrreducible (↑t : Set α)) ∧
      Eq.{u_1 + 1} (α := Closeds α) ⊥ (sSup ∅)

Tactic:
simp
-- 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 ≠ ⊥
pos :
  ∀ (h₁ : IsPreirreducible (↑s : Set α)),
    ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
neg :
  ∀ (h₁ : ¬IsPreirreducible (↑s : Set α)),
    ∃ (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:
by_cases h₁ : IsPreirreducible (s : Set α)

Premises used: IsPreirreducible, SetLike.coe
-- 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 ≠ ⊥
h₁ : IsPreirreducible (↑s : Set α)
⊢ IsIrreducible (↑s : Set α)

Tactic:
replace h₁ : IsIrreducible (s : Set α) := ⟨Closeds.coe_nonempty.2 h₀, h₁⟩
-- 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 ≠ ⊥
h₁ : IsIrreducible (↑s : Set α)
h :
  Set.Finite (α := Closeds α) {s} ∧
    (∀ (t : Closeds α), Membership.mem (γ := Set (Closeds α)) {s} t → IsIrreducible (↑t : Set α)) ∧ s = sSup {s}
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S

Tactic:
use {s}
-- 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 ≠ ⊥
h₁ : IsIrreducible (↑s : Set α)
⊢ Set.Finite (α := Closeds α) {s} ∧
    (∀ (t : Closeds α), Membership.mem (γ := Set (Closeds α)) {s} t → IsIrreducible (↑t : Set α)) ∧ s = sSup {s}

Tactic:
simp [h₁]
-- 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 ≠ ⊥
h₁ : ¬IsPreirreducible (↑s : Set α)
⊢ ∃ (x : Set α) (x_1 : Set α) (_ : IsClosed[inst] x) (_ : IsClosed[inst] x_1) (_ : (↑s : Set α) ⊆ x ∪ x_1),
    ¬(↑s : Set α) ⊆ x ∧ ¬(↑s : Set α) ⊆ x_1

Tactic:
simp only [isPreirreducible_iff_isClosed_union_isClosed, not_forall, not_or] at h₁

Premises used: isPreirreducible_iff_isClosed_union_isClosed, not_or, Classical.not_forall
-- 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 ≠ ⊥
h₁ :
  ∃ (x : Set α) (x_1 : Set α) (_ : IsClosed[inst] x) (_ : IsClosed[inst] x_1) (_ : (↑s : Set α) ⊆ x ∪ x_1),
    ¬(↑s : Set α) ⊆ x ∧ ¬(↑s : Set α) ⊆ x_1
neg :
  ∀ (z₁ z₂ : Set α) (hz₁ : IsClosed[inst] z₁) (hz₂ : IsClosed[inst] z₂) (h : (↑s : Set α) ⊆ z₁ ∪ z₂)
    (hz₁' : ¬(↑s : Set α) ⊆ z₁) (hz₂' : ¬(↑s : Set α) ⊆ z₂),
    ∃ (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:
obtain ⟨z₁, z₂, hz₁, hz₂, h, hz₁', hz₂'⟩ := h₁
-- 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₁ z₂ : Set α
hz₁ : IsClosed[inst] z₁
hz₂ : IsClosed[inst] z₂
h : (↑s : Set α) ⊆ z₁ ∪ z₂
hz₁' : ¬(↑s : Set α) ⊆ z₁
hz₂' : ¬(↑s : Set α) ⊆ z₂
⊢ IsClosed[inst] z₁

Tactic:
hz₁
-- 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₁ z₂ : Set α
hz₁ : IsClosed[inst] z₁
hz₂ : IsClosed[inst] z₂
h : (↑s : Set α) ⊆ z₁ ∪ z₂
hz₁' : ¬(↑s : Set α) ⊆ z₁
hz₂' : ¬(↑s : Set α) ⊆ z₂
neg :
  ∀ (z₁ : Closeds α) (h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ z₂) (hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)),
    ∃ (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:
lift z₁ to Closeds α using hz₁

Premises used: TopologicalSpace.Closeds
-- 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₂ : Set α
hz₂ : IsClosed[inst] z₂
hz₂' : ¬(↑s : Set α) ⊆ z₂
z₁ : Closeds α
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ z₂
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
⊢ IsClosed[inst] z₂

Tactic:
hz₂
-- 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₂ : Set α
hz₂ : IsClosed[inst] z₂
hz₂' : ¬(↑s : Set α) ⊆ z₂
z₁ : Closeds α
h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ z₂
hz₁' : ¬(↑s : Set α) ⊆ (↑z₁ : Set α)
neg :
  ∀ (z₂ : Closeds α) (hz₂' : ¬(↑s : Set α) ⊆ (↑z₂ : Set α)) (h : (↑s : Set α) ⊆ (↑z₁ : Set α) ∪ (↑z₂ : Set α)),
    ∃ (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:
lift z₂ to Closeds α using hz₂

Premises used: TopologicalSpace.Closeds
-- 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 α)
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