awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
s : Set α
hs : IsIrreducible s
hs' : IsClosed s
t : Set α
ht : IsIrreducible t
ht' : IsClosed t
⊢ LE.le (α := α)
      (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
              invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : TopologicalSpace.IrreducibleCloseds α) → α)
          { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } :
        α)
      (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
              invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : TopologicalSpace.IrreducibleCloseds α) → α)
          { carrier := t, isIrreducible' := ht, isClosed' := ht' : TopologicalSpace.IrreducibleCloseds α } :
        α) ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
      { carrier := t, isIrreducible' := ht, isClosed' := ht' }
have refine : Subset (α := Set α)
    (closure
      (singleton (α := α)
        (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ sorry.genericPoint (S := s.carrier),
                invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := sorry, isClosed' := sorry }, left_inv := sorry,
                right_inv := sorry } :
              (a : TopologicalSpace.IrreducibleCloseds α) → α)
            { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } :
          α)))
    (closure
      (singleton (α := α)
        (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ sorry.genericPoint (S := s.carrier),
                invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := sorry, isClosed' := sorry }, left_inv := sorry,
                right_inv := sorry } :
              (a : TopologicalSpace.IrreducibleCloseds α) → α)
            { carrier := t, isIrreducible' := ht, isClosed' := ht' : TopologicalSpace.IrreducibleCloseds α } :
          α))) ↔
  { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
    { carrier := t, isIrreducible' := ht, isClosed' := ht' }
Tactic: refine specializes_iff_closure_subset.trans ?_
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : QuasiSober α
inst_3 : T0Space α
s : Set α
hs : IsIrreducible s
hs' : IsClosed s
t : Set α
ht : IsIrreducible t
ht' : IsClosed t
⊢ Subset (α := Set α)
      (closure
        (singleton (α := α)
          (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
                  invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ },
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : TopologicalSpace.IrreducibleCloseds α) → α)
              { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } :
            α)))
      (closure
        (singleton (α := α)
          (({ toFun := fun (s : TopologicalSpace.IrreducibleCloseds α) ↦ ⋯.genericPoint (S := s.carrier),
                  invFun := fun (x : α) ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ },
                  left_inv := ⋯, right_inv := ⋯ } :
                (a : TopologicalSpace.IrreducibleCloseds α) → α)
              { carrier := t, isIrreducible' := ht, isClosed' := ht' : TopologicalSpace.IrreducibleCloseds α } :
            α))) ↔
    { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
      { carrier := t, isIrreducible' := ht, isClosed' := ht' }
have simp : s ⊆ t ↔
  { carrier := s, isIrreducible' := hs, isClosed' := hs' : TopologicalSpace.IrreducibleCloseds α } ≤
    { carrier := t, isIrreducible' := ht, isClosed' := ht' }
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Sober (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
⊢ ∃ (x : α), IsGenericPoint x S
have hS'' : IsIrreducible (f '' S)
Tactic: have hS'' := hS.image f hf.continuous.continuousOn
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
⊢ ∃ (x : α), IsGenericPoint x S
have obtain : ∀ (x : β) (hx : IsGenericPoint x (f '' S)), ∃ (x : α), IsGenericPoint x S
Tactic: obtain ⟨x, hx⟩ := QuasiSober.sober hS'' (hf.isClosedMap _ hS')
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
x : β
hx : IsGenericPoint x (f '' S)
⊢ ∃ (x : α), IsGenericPoint x S
have obtain : ∀ (y : α) (hx : IsGenericPoint (f y) (f '' S)), ∃ (x : α), IsGenericPoint x S
Tactic: obtain ⟨y, -, rfl⟩ := hx.mem
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
y : α
hx : IsGenericPoint (f y) (f '' S)
⊢ ∃ (x : α), IsGenericPoint x S
have h : IsGenericPoint y S
Tactic: use y
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
y : α
hx : IsGenericPoint (f y) (f '' S)
⊢ IsGenericPoint y S
have h : f '' closure[inst] {y} = f '' S
Tactic: apply image_injective.mpr hf.injective
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
y : α
hx : IsGenericPoint (f y) (f '' S)
⊢ f '' closure[inst] {y} = f '' S
have h : f '' closure[inst] {y} = closure[inst_1] {f y}
Tactic: rw [← hx.def, ← hf.closure_image_eq, image_singleton]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
y : α
hx : IsGenericPoint (f y) (f '' S)
h : f '' closure[inst] {y} = closure[inst_1] {f y}
⊢ f '' closure[inst] {y} = f '' S
have h₁ : closure[inst_1] (f '' {y}) = closure[inst_1] {f y}
Tactic: rw [← hx.def, ← hf.closure_image_eq, image_singleton]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
y : α
hx : IsGenericPoint (f y) (f '' S)
h : f '' closure[inst] {y} = closure[inst_1] {f y}
h₁ : closure[inst_1] (f '' {y}) = closure[inst_1] {f y}
⊢ f '' closure[inst] {y} = f '' S
have h₂ : Eq (α := Set β) (closure[inst_1] {f y}) (closure[inst_1] {f y})
Tactic: rw [← hx.def, ← hf.closure_image_eq, image_singleton]
-- Lean 4 proof step from Mathlib.Topology.Sober (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
⊢ ∃ (x : α), IsGenericPoint x S
have hS'' : IsIrreducible (f '' S)
Tactic: have hS'' := hS.image f hf.continuous.continuousOn
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
⊢ ∃ (x : α), IsGenericPoint x S
have obtain : ∀ (x : β) (hx : IsGenericPoint x (closure[inst_1] (f '' S))), ∃ (x : α), IsGenericPoint x S
Tactic: obtain ⟨x, hx⟩ := QuasiSober.sober hS''.closure isClosed_closure
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
S : Set α
hS : IsIrreducible S
hS' : IsClosed[inst] S
hS'' : IsIrreducible (f '' S)
x : β
hx : IsGenericPoint x (closure[inst_1] (f '' S))
⊢ ∃ (x : α), IsGenericPoint x S
have obtain : ∀ (T : Set β) (hT : IsClosed[inst_1] T) (hS : IsIrreducible (f ⁻¹' T)) (hS' : IsClosed[inst] (f ⁻¹' T))
  (hS'' : IsIrreducible (f '' f ⁻¹' T)) (hx : IsGenericPoint x (closure[inst_1] (f '' f ⁻¹' T))),
  ∃ (x : α), IsGenericPoint x (f ⁻¹' T)
Tactic: obtain ⟨T, hT, rfl⟩ := hf.isInducing.isClosed_iff.mp hS'
Cleared hypotheses: S, hS, hS', hS'', hx
-- Lean 4 proof step from Mathlib.Topology.Sober (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (f '' f ⁻¹' T)
hx : IsGenericPoint x (closure[inst_1] (f '' f ⁻¹' T))
⊢ ∃ (x : α), IsGenericPoint x (f ⁻¹' T)
have hS''₁ : IsIrreducible (T ∩ range f)
Tactic: rw [image_preimage_eq_inter_range] at hx hS''
Cleared hypotheses: hS'', hx
-- Lean 4 proof step from Mathlib.Topology.Sober (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (f '' f ⁻¹' T)
hx : IsGenericPoint x (closure[inst_1] (f '' f ⁻¹' T))
hS''₁ : IsIrreducible (T ∩ range f)
⊢ ∃ (x : α), IsGenericPoint x (f ⁻¹' T)
have hx₁ : IsGenericPoint x (closure[inst_1] (T ∩ range f))
Tactic: rw [image_preimage_eq_inter_range] at hx hS''
Cleared hypotheses: hS'', hx
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
⊢ x ∈ T
have rw : x ∈ closure[inst_1] T
Tactic: rw [← hT.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sober (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
⊢ ∃ (x : α), IsGenericPoint x (f ⁻¹' T)
have hxT : x ∈ T
Tactic: have hxT : x ∈ T := by
      rw [← hT.closure_eq]
      exact closure_mono inter_subset_left hx.mem
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
hxT : x ∈ T
⊢ x ∈ range f
have rw : (closure[inst_1] (T ∩ range f) ∩ range f).Nonempty
Tactic: rw [hx.mem_open_set_iff hf.isOpen_range]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
hxT : x ∈ T
⊢ (closure[inst_1] (T ∩ range f) ∩ range f).Nonempty
have refine : T ∩ range f ⊆ closure[inst_1] (T ∩ range f) ∩ range f
Tactic: refine Nonempty.mono ?_ hS''.1
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst_1] (T ∩ range f))
hxT : x ∈ T
⊢ ∃ (x : α), IsGenericPoint x (f ⁻¹' T)
have obtain : ∀ (y : α) (hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))) (hxT : f y ∈ T),
  ∃ (x : α), IsGenericPoint x (f ⁻¹' T)
Tactic: obtain ⟨y, rfl⟩ : x ∈ range f := by
      rw [hx.mem_open_set_iff hf.isOpen_range]
      refine Nonempty.mono ?_ hS''.1
      simpa using subset_closure
Cleared hypotheses: x, hx, hxT
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
⊢ ∃ (x : α), IsGenericPoint x (f ⁻¹' T)
have h : IsGenericPoint y (f ⁻¹' T)
Tactic: use y
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
⊢ closure[inst] {y} = f ⁻¹' T
have h : f ⁻¹' closure[inst_1] (T ∩ range f) = f ⁻¹' T
Tactic: rw [hf.isEmbedding.closure_eq_preimage_closure_image, image_singleton, show _ = _ from hx]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
⊢ f ⁻¹' closure[inst_1] (T ∩ range f) = f ⁻¹' T
have h : f '' f ⁻¹' closure[inst_1] (T ∩ range f) = f '' f ⁻¹' T
Tactic: apply image_injective.mpr hf.injective
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
⊢ f '' f ⁻¹' closure[inst_1] (T ∩ range f) = f '' f ⁻¹' T
have h : ∀ (z : β), z ∈ f '' f ⁻¹' closure[inst_1] (T ∩ range f) ↔ z ∈ f '' f ⁻¹' T
Tactic: ext z
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst_2 : QuasiSober β
T : Set β
hT : IsClosed[inst_1] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
y : α
hx : IsGenericPoint (f y) (closure[inst_1] (T ∩ range f))
hxT : f y ∈ T
z : β
⊢ z ∈ f '' f ⁻¹' closure[inst_1] (T ∩ range f) ↔ z ∈ f '' f ⁻¹' T
have h : z ∈ range f → (z ∈ closure[inst_1] (T ∩ range f) ↔ z ∈ T)
Tactic: simp only [image_preimage_eq_inter_range, mem_inter_iff, and_congr_left_iff]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
⊢ QuasiSober α ↔ ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
have refine : ∀ (hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)) {S : Set α}, IsIrreducible S → IsClosed S → ∃ (x : α), IsGenericPoint x S
Tactic: refine ⟨fun h i ↦ (U i).isOpenEmbedding'.quasiSober, fun hU' ↦ (quasiSober_iff _).mpr ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
⊢ ∃ (x : α), IsGenericPoint x t
have obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (x : α), IsGenericPoint x t
Tactic: obtain ⟨i, hi⟩ := hU.exists_mem x
-- Lean 4 proof step from Mathlib.Topology.Sober (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
⊢ ∃ (x : α), IsGenericPoint x t
have H : IsIrreducible (X := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)
Tactic: have H : IsIrreducible ((↑) ⁻¹' t : Set (U i)) :=
      ⟨⟨⟨x, hi⟩, hx⟩, h.preimage (U i).isOpenEmbedding'⟩
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (X := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)
⊢ ∃ (x : α), IsGenericPoint x t
have h₁ : IsGenericPoint (↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α) t
Tactic: use H.genericPoint
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (X := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)
⊢ IsGenericPoint (↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α) t
have h₁ : closure {(↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α)} ≤ t
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (X := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)
h₁ : closure {(↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α)} ≤ t
⊢ IsGenericPoint (↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α) t
have h₂ : t ≤ closure {(↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α)}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (X := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)
⊢ t ≤ closure {(↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α)}
have h₁ : t ≤
  closure
    (image (α := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i))
      (closure (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)))
Tactic: rw [← image_singleton, ← closure_image_closure continuous_subtype_val,
      H.isGenericPoint_genericPoint_closure.def]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
hU' : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
t : Set α
h : IsPreirreducible t
x : α
hx : x ∈ t
h' : IsClosed t
i : ι
hi : x ∈ U i
H : IsIrreducible (X := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)
⊢ t ≤
    closure
      (image (α := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (closure (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)))
have h₁ : t ∩ (↑(U i) : Set α) ⊆
  image (α := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i))
    (closure (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t))
Tactic: refine (subset_closure_inter_of_isPreirreducible_of_isOpen h (U i).isOpen ⟨x, ⟨hx, hi⟩⟩).trans
      (closure_mono ?_)
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : R1Space α
S : Set α
h : IsIrreducible S
hs : IsClosed S
⊢ ∃ (x : α), IsGenericPoint x S
have obtain : ∀ (x : α) (hx : x ∈ S), ∃ (x : α), IsGenericPoint x S
Tactic: obtain ⟨x, hx⟩ := h.nonempty
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : R1Space α
S : Set α
h : IsIrreducible S
hs : IsClosed S
x : α
hx : x ∈ S
⊢ ∃ (x : α), IsGenericPoint x S
have h₁ : IsGenericPoint x S
Tactic: use x
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : R1Space α
S : Set α
h : IsIrreducible S
hs : IsClosed S
x : α
hx : x ∈ S
⊢ IsGenericPoint x S
have h₁ : closure {x} ⊆ S
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : R1Space α
S : Set α
h : IsIrreducible S
hs : IsClosed S
x : α
hx : x ∈ S
h₁ : closure {x} ⊆ S
⊢ IsGenericPoint x S
have h₂ : S ⊆ closure {x}
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : R1Space α
S : Set α
h : IsIrreducible S
hs : IsClosed S
x : α
hx : x ∈ S
⊢ closure {x} ⊆ S
have h₁ : closure {x} ⊆ closure S
Tactic: rw [← hs.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
V W : Set α
inst_1 : QuasiSober.{u_1} (↑W : Type u_1)
hV : IsClosed V
⊢ QuasiSober.{u_1} (↑(W ∩ V) : Type u_1)
have refine : IsClosed (X := (↑W : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ W) ⁻¹' (W ∩ V))
Tactic: refine QuasiSober.of_subset ?_ (Set.inter_subset_left : W ∩ V ⊆ W)
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
V W : Set α
inst_1 : QuasiSober.{u_1} (↑W : Type u_1)
hV : IsClosed V
⊢ IsClosed (X := (↑W : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ W) ⁻¹' (W ∩ V))
have rw : IsClosed (X := (↑W : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ W) ⁻¹' V)
Tactic: rw [Subtype.preimage_coe_self_inter W V]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
V W : Set α
inst_1 : QuasiSober.{u_1} (↑V : Type u_1)
hW : IsClosed W
⊢ QuasiSober.{u_1} (↑(W ∩ V) : Type u_1)
have rw : QuasiSober.{u_1} (↑(V ∩ W) : Type u_1)
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Sober (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
⊢ _root_.closure (genericPoints α) = univ
have refine : ∀ (x : α), irreducibleComponent x ⊆ _root_.closure (genericPoints α)
Tactic: refine Set.eq_univ_iff_forall.mpr fun x ↦ Set.subset_def.mp ?_ x mem_irreducibleComponent