awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) ↔
    ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
have refine_1 : (∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) →
  ∀ (v : Set α) (v' : Set β) (hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v) (hv : s ⊆ v ∧ v ⊆ u),
    ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
Tactic: refine ⟨fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_, fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
refine_1 :
  (∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) →
    ∀ (v : Set α) (v' : Set β) (hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v) (hv : s ⊆ v ∧ v ⊆ u),
      ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
⊢ (∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) ↔
    ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
have refine_2 : (∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u) →
  ∀ (v v' : Set β) (hv' : IsOpen[t] v' ∧ f '' s ⊆ v' ∧ v' ⊆ v) (hv : f ⁻¹' v ⊆ u),
    ∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
Tactic: refine ⟨fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_, fun ⟨v, ⟨v', hv'⟩, hv⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
h : ∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u
v : Set α
v' : Set β
hv' : IsOpen[t] v' ∧ f ⁻¹' v' = v
hv : s ⊆ v ∧ v ⊆ u
⊢ ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
have refine_1 : f '' s ⊆ v'
Tactic: refine ⟨v', ⟨v', hv'.1, ?_, subset_rfl⟩, hv'.2.trans_subset hv.2⟩
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
⊢ 𝓝ˢ s = comap f (𝓝ˢ (f '' s))
have h : ∀ (s_1 : Set α), s_1 ∈ 𝓝ˢ s ↔ s_1 ∈ comap f (𝓝ˢ (f '' s))
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s_1 s : Set α
⊢ s ∈ 𝓝ˢ s_1 ↔ s ∈ comap f (𝓝ˢ (f '' s_1))
have h : (∃ v ∈ 𝓝ˢ (f '' s_1), f ⁻¹' v ⊆ s) ↔ s ∈ comap f (𝓝ˢ (f '' s_1))
Tactic: rw [mem_nhdsSet_induced, mem_comap]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s_1 s : Set α
h : (∃ v ∈ 𝓝ˢ (f '' s_1), f ⁻¹' v ⊆ s) ↔ s ∈ comap f (𝓝ˢ (f '' s_1))
⊢ s ∈ 𝓝ˢ s_1 ↔ s ∈ comap f (𝓝ˢ (f '' s_1))
have h₁ : (∃ v ∈ 𝓝ˢ (f '' s_1), f ⁻¹' v ⊆ s) ↔ ∃ t_1 ∈ 𝓝ˢ (f '' s_1), f ⁻¹' t_1 ⊆ s
Tactic: rw [mem_nhdsSet_induced, mem_comap]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
⊢ map f (𝓝ˢ s) = 𝓝ˢ[range f] (f '' s)
have rw : map f (comap f (𝓝ˢ (f '' s))) = 𝓝ˢ[range f] (f '' s)
Tactic: rw [nhdsSet_induced, Filter.map_comap, nhdsSetWithin]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
rw : map f (comap f (𝓝ˢ (f '' s))) = 𝓝ˢ[range f] (f '' s)
⊢ map f (𝓝ˢ s) = 𝓝ˢ[range f] (f '' s)
have rw₁ : 𝓝ˢ (f '' s) ⊓ 𝓟 (range f) = 𝓝ˢ[range f] (f '' s)
Tactic: rw [nhdsSet_induced, Filter.map_comap, nhdsSetWithin]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
rw : map f (comap f (𝓝ˢ (f '' s))) = 𝓝ˢ[range f] (f '' s)
rw₁ : 𝓝ˢ (f '' s) ⊓ 𝓟 (range f) = 𝓝ˢ[range f] (f '' s)
⊢ map f (𝓝ˢ s) = 𝓝ˢ[range f] (f '' s)
have rw₂ : 𝓝ˢ (f '' s) ⊓ 𝓟 (range f) = 𝓝ˢ (f '' s) ⊓ 𝓟 (range f)
Tactic: rw [nhdsSet_induced, Filter.map_comap, nhdsSetWithin]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
t : Set (↑s : Type u_1)
⊢ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝ˢ t) = 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
have rw : 𝓝ˢ[range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))]
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) =
  𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
Tactic: rw [IsInducing.subtypeVal.map_nhdsSet_eq, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
t : Set (↑s : Type u_1)
rw :
  𝓝ˢ[range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))]
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) =
    𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝ˢ t) = 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
have rw₁ : 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) = 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
Tactic: rw [IsInducing.subtypeVal.map_nhdsSet_eq, Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
t u : Set (↑s : Type u_1)
⊢ u ∈ 𝓝ˢ t ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u ∈ 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
have rw : u ∈ 𝓝ˢ t ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝ˢ t)
Tactic: rw [← map_nhdsSet_subtype_val, image_mem_map_iff Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
t u : Set (↑s : Type u_1)
rw : u ∈ 𝓝ˢ t ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝ˢ t)
⊢ u ∈ 𝓝ˢ t ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u ∈ 𝓝ˢ[s] (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
have rw₁ : u ∈ 𝓝ˢ t ↔ u ∈ 𝓝ˢ t
Tactic: rw [← map_nhdsSet_subtype_val, image_mem_map_iff Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
have rw : (∀ (k : Opens α), IsCompactElement k) ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
Tactic: rw [NoetherianSpace, CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact,
    CompleteLattice.isSupFiniteCompact_iff_all_elements_compact]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
⊢ IsCompact s
have refine : ∀ {ι : Type u_1} (U : ι → Set α) (hUo : ∀ (i : ι), IsOpen[inst] (U i)) (hs : s ⊆ ⋃ (i : ι), U i),
  ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
Tactic: refine isCompact_iff_finite_subcover.2 fun U hUo hs => ?_
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Set α
ι : Type u_1
U : ι → Set α
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hs : s ⊆ ⋃ (i : ι), U i
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
have rcases : ∀ (t : Finset ι) (ht : (↑{ carrier := ⋃ (i : ι), U i, is_open' := sorry : Opens α } : Set α) ⊆ ⋃ i ∈ t, U i),
  ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i
Tactic: rcases ((noetherianSpace_iff_opens α).mp ‹_› ⟨⋃ i, U i, isOpen_iUnion hUo⟩).elim_finite_subcover U
    hUo Set.Subset.rfl with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
have simp_rw : (WellFounded fun (x1 x2 : Opens α) ↦ x2 < x1) ↔ WellFounded fun (x1 x2 : Closeds α) ↦ x1 < x2
Tactic: simp_rw [isWellFounded_iff]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ [NoetherianSpace α, WellFoundedLT.{u_1} (Closeds α), ∀ (s : Set α), IsCompact s,
      ∀ (s : Opens α), IsCompact (↑s : Set α)].TFAE
have tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
Tactic: tfae_have 1 ↔ 2 := by
    simp_rw [isWellFounded_iff]
    exact Opens.compl_bijective.2.wellFounded_iff (@OrderIso.compl (Set α)).lt_iff_lt.symm
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
tfae_1_iff_2 : NoetherianSpace α ↔ WellFoundedLT.{u_1} (Closeds α)
⊢ [NoetherianSpace α, WellFoundedLT.{u_1} (Closeds α), ∀ (s : Set α), IsCompact s,
      ∀ (s : Opens α), IsCompact (↑s : Set α)].TFAE
have tfae_1_iff_4 : NoetherianSpace α ↔ ∀ (s : Opens α), IsCompact (↑s : Set α)
Tactic: tfae_have 1 ↔ 4 := noetherianSpace_iff_opens α
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (hypothesis)
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 α, WellFoundedLT.{u_1} (Closeds α), ∀ (s : Set α), IsCompact s,
      ∀ (s : Opens α), IsCompact (↑s : Set α)].TFAE
have tfae_1_to_3 : ∀ (a : NoetherianSpace α) (s : Set α), IsCompact s
Tactic: tfae_have 1 → 3 := @NoetherianSpace.isCompact α _
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (hypothesis)
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
⊢ [NoetherianSpace α, WellFoundedLT.{u_1} (Closeds α), ∀ (s : Set α), IsCompact s,
      ∀ (s : Opens α), IsCompact (↑s : Set α)].TFAE
have tfae_3_to_4 : ∀ (a : ∀ (s : Set α), IsCompact s) (s : Opens α), IsCompact (↑s : Set α)
Tactic: tfae_have 3 → 4 := fun h s => h s
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α_1 : Type u_1
β : Type u_2
inst : TopologicalSpace α_1
inst_1 : TopologicalSpace β
α : Type u_3
⊢ NoetherianSpace.{u_3} (CofiniteTopology α)
have simp : ∀ (s : Set (CofiniteTopology α)) (f : Ultrafilter (CofiniteTopology α)),
  s ∈ (↑f : Filter (CofiniteTopology α)) →
    ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
Tactic: simp only [noetherianSpace_iff_isCompact, isCompact_iff_ultrafilter_le_nhds,
    CofiniteTopology.nhds_eq, Ultrafilter.le_sup_iff, Filter.le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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 α))
⊢ ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
have inl : ∀ (hf : (↑f : 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⟩)
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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
⊢ ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
have inr : ∀ (a : CofiniteTopology α) (hs : s ∈ (↑(pure a) : Filter (CofiniteTopology α))),
  ∃ x ∈ s,
    (↑(pure a) : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑(pure a) : Filter (CofiniteTopology α)) ≤ Filter.cofinite
Tactic: rcases f.le_cofinite_or_eq_pure with (hf | ⟨a, rfl⟩)
Cleared hypotheses: f, hs
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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
⊢ ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
have inl : ∀ (a : CofiniteTopology α) (ha : a ∈ s),
  ∃ x ∈ s, (↑f : Filter (CofiniteTopology α)) ≤ pure x ∨ (↑f : Filter (CofiniteTopology α)) ≤ Filter.cofinite
Tactic: rcases Filter.nonempty_of_mem hs with ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst_1 : Finite ι
hf : ∀ (i : ι), NoetherianSpace.{u_1} (↑(f i) : Type u_1)
⊢ NoetherianSpace.{u_1} (↑(⋃ (i : ι), f i) : Type u_1)
have simp_rw : ∀ (hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t), ∀ t ⊆ ⋃ (i : ι), f i, IsCompact t
Tactic: simp_rw [noetherianSpace_set_iff] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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 t
have rw : IsCompact.{u_1} (X := α) (⋃ (i : ι), t ∩ f i)
Tactic: rw [← Set.inter_eq_left.mpr ht, Set.inter_iUnion]
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
s : Closeds α
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have 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
Tactic: apply wellFounded_lt.induction s
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have 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
Tactic: rcases eq_or_ne s ⊥ with rfl | h₀
Cleared hypotheses: s, H
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have inr : ∀ (h₀ : s ≠ ⊥), ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
Tactic: rcases eq_or_ne s ⊥ with rfl | h₀
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : NoetherianSpace α
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
have h : Set.Finite.{u_1} (α := Closeds α) ∅ ∧
  (∀ (t : Closeds α), Membership.mem (γ := Set (Closeds α)) ∅ t → IsIrreducible (↑t : Set α)) ∧
    Eq.{u_1 + 1} (α := Closeds α) ⊥ (sSup ∅)
Tactic: use ∅
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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 ≠ ⊥
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have pos : ∀ (h₁ : IsPreirreducible (↑s : Set α)),
  ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
Tactic: by_cases h₁ : IsPreirreducible (s : Set α)
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have neg : ∀ (h₁ : ¬IsPreirreducible (↑s : Set α)),
  ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
Tactic: by_cases h₁ : IsPreirreducible (s : Set α)
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (hypothesis)
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 α)
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have h₂ : IsIrreducible (↑s : Set α)
Tactic: replace h₁ : IsIrreducible (s : Set α) := ⟨Closeds.coe_nonempty.2 h₀, h₁⟩
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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 α)
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have h : Set.Finite (α := Closeds α) {s} ∧
  (∀ (t : Closeds α), Membership.mem (γ := Set (Closeds α)) {s} t → IsIrreducible (↑t : Set α)) ∧ s = sSup {s}
Tactic: use {s}
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (hypothesis)
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 α)
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have 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
Tactic: simp only [isPreirreducible_iff_isClosed_union_isClosed, not_forall, not_or] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have 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
Tactic: obtain ⟨z₁, z₂, hz₁, hz₂, h, hz₁', hz₂'⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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₂
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have 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
Tactic: lift z₁ to Closeds α using hz₁
Cleared hypotheses: z₁, hz₁, h, hz₁'
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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 α)
⊢ ∃ (S : Set (Closeds α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have 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
Tactic: lift z₂ to Closeds α using hz₂
Cleared hypotheses: z₂, hz₂, hz₂', h
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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 α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have 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
Tactic: rcases H (s ⊓ z₁) (inf_lt_left.2 hz₁') with ⟨S₁, hSf₁, hS₁, h₁⟩
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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 α)), S.Finite ∧ (∀ t ∈ S, IsIrreducible (↑t : Set α)) ∧ s = sSup S
have 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
Tactic: rcases H (s ⊓ z₂) (inf_lt_left.2 hz₂') with ⟨S₂, hSf₂, hS₂, h₂⟩
-- Lean 4 proof step from Mathlib.Topology.NoetherianSpace (goal)
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
have neg : s = sSup (S₁ ∪ S₂)
Tactic: refine ⟨S₁ ∪ S₂, hSf₁.union hSf₂, Set.union_subset_iff.2 ⟨hS₁, hS₂⟩, ?_⟩