awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sober
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₁ : IsGenericPoint (↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α) t
⊢ ∃ (x : α), IsGenericPoint x t

Tactic:
use H.genericPoint

Premises used: IsIrreducible.genericPoint
-- Module: Mathlib.Topology.Sober
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
h₂ : t ≤ closure {(↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α)}
⊢ IsGenericPoint (↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α) t

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Sober
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)
⊢ closure {(↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α)} ≤ t

Tactic:
simpa [h'.closure_subset_iff, h'.closure_eq] using
        continuous_subtype_val.closure_preimage_subset _ H.isGenericPoint_genericPoint_closure.mem

Premises used: continuous_subtype_val, IsIrreducible.isGenericPoint_genericPoint_closure, IsClosed.closure_eq, IsClosed.closure_subset_iff, IsGenericPoint.mem, Continuous.closure_preimage_subset
-- Module: Mathlib.Topology.Sober
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₁ :
  t ≤
    closure
      (image (α := ↥(U i)) (Subtype.val (p := fun (x : α) ↦ x ∈ U i))
        (closure (Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)))
⊢ t ≤ closure {(↑(H.genericPoint (S := Subtype.val (p := fun (x : α) ↦ x ∈ U i) ⁻¹' t)) : α)}

Tactic:
rw [← image_singleton, ← closure_image_closure continuous_subtype_val,
      H.isGenericPoint_genericPoint_closure.def]

Premises used: IsGenericPoint.def, Set.image_singleton, continuous_subtype_val, IsIrreducible.isGenericPoint_genericPoint_closure, closure_image_closure
-- Module: Mathlib.Topology.Sober
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)))

Tactic:
(subset_closure_inter_of_isPreirreducible_of_isOpen h (U i).isOpen ⟨x, ⟨hx, hi⟩⟩).trans
      (closure_mono ?_)

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen, HasSubset.Subset.trans, closure_mono, TopologicalSpace.Opens.isOpen, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sober
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₁ :
  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))
⊢ t ≤
    closure
      (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 ?_)

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen, HasSubset.Subset.trans, closure_mono, TopologicalSpace.Opens.isOpen, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sober
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 ∩ (↑(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:
simpa only [inter_comm t, ← Subtype.image_preimage_coe] using Set.image_mono subset_closure

Premises used: subset_closure, Set.image_mono, Subtype.image_preimage_coe, Set.inter_comm
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
inst_1 : ∀ (i : ι), QuasiSober.{u_1} ↥(U i)
⊢ QuasiSober α

Tactic:
hU.quasiSober_iff_forall.mpr ‹_›

Premises used: Iff.mpr, TopologicalSpace.IsOpenCover.quasiSober_iff_forall
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Set α)
hS : ∀ (s : (↑S : Type u_1)), IsOpen (↑s : Set α)
inst_1 : ∀ (s : (↑S : Type u_1)), QuasiSober.{u_1} (↑(↑s : Set α) : Type u_1)
hS' : ⋃₀ S = ⊤
⊢ TopologicalSpace.IsOpenCover (X := α) fun (s : (↑S : Type u_1)) ↦ { carrier := (↑s : Set α), is_open' := ⋯ }

Tactic:
simpa [TopologicalSpace.IsOpenCover, ← SetLike.coe_set_eq, sUnion_eq_iUnion] using hS'

Premises used: Set.sUnion_eq_iUnion, TopologicalSpace.IsOpenCover, SetLike.coe_set_eq
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : R1Space α
S : Set α
h : IsIrreducible S
hs : IsClosed S
obtain : ∀ (x : α) (hx : x ∈ S), ∃ (x : α), IsGenericPoint x S
⊢ ∃ (x : α), IsGenericPoint x S

Tactic:
obtain ⟨x, hx⟩ := h.nonempty

Premises used: IsIrreducible.nonempty
-- Module: Mathlib.Topology.Sober
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₁ : IsGenericPoint x S
⊢ ∃ (x : α), IsGenericPoint x S

Tactic:
use x
-- Module: Mathlib.Topology.Sober
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
h₂ : S ⊆ closure {x}
⊢ IsGenericPoint x S

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.Topology.Sober
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} ⊆ closure S
⊢ closure {x} ⊆ S

Tactic:
rw [← hs.closure_eq]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.Sober
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} ⊆ closure S

Tactic:
closure_mono (singleton_subset_iff.mpr hx)

Premises used: Iff.mpr, Set.singleton_subset_iff, closure_mono
-- Module: Mathlib.Topology.Sober
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} ⊆ closure S

Tactic:
exact closure_mono (singleton_subset_iff.mpr hx)

Premises used: Iff.mpr, Set.singleton_subset_iff, closure_mono
-- Module: Mathlib.Topology.Sober
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
⊢ S ⊆ closure {x}

Tactic:
isPreirreducible_iff_forall_mem_subset_closure_singleton.mp h.isPreirreducible x hx

Premises used: IsIrreducible.isPreirreducible, Iff.mp, isPreirreducible_iff_forall_mem_subset_closure_singleton
-- Module: Mathlib.Topology.Sober
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
⊢ S ⊆ closure {x}

Tactic:
exact isPreirreducible_iff_forall_mem_subset_closure_singleton.mp h.isPreirreducible x hx

Premises used: IsIrreducible.isPreirreducible, Iff.mp, isPreirreducible_iff_forall_mem_subset_closure_singleton
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
V W : Set α
inst_1 : QuasiSober.{u_1} (↑W : Type u_1)
hV : IsClosed (X := (↑W : Type u_1)) (W ↓∩ V)
h : V ⊆ W
⊢ QuasiSober.{u_1} (↑V : Type u_1)

Tactic:
Topology.IsClosedEmbedding.quasiSober <| .inclusion h hV

Premises used: Topology.IsClosedEmbedding.inclusion, Topology.IsClosedEmbedding.quasiSober
-- Module: Mathlib.Topology.Sober
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)

Tactic:
QuasiSober.of_subset ?_ (Set.inter_subset_left : W ∩ V ⊆ W)

Premises used: Set.inter_subset_left, QuasiSober.of_subset
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
V W : Set α
inst_1 : QuasiSober.{u_1} (↑W : Type u_1)
hV : IsClosed V
refine : IsClosed (X := (↑W : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ W) ⁻¹' (W ∩ V))
⊢ QuasiSober.{u_1} (↑(W ∩ V) : Type u_1)

Tactic:
refine QuasiSober.of_subset ?_ (Set.inter_subset_left : W ∩ V ⊆ W)

Premises used: Set.inter_subset_left, QuasiSober.of_subset
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
V W : Set α
inst_1 : QuasiSober.{u_1} (↑W : Type u_1)
hV : IsClosed V
rw : IsClosed (X := (↑W : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ W) ⁻¹' V)
⊢ IsClosed (X := (↑W : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ W) ⁻¹' (W ∩ V))

Tactic:
rw [Subtype.preimage_coe_self_inter W V]

Premises used: Subtype.preimage_coe_self_inter
-- Module: Mathlib.Topology.Sober
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) ⁻¹' V)

Tactic:
IsClosed.preimage_val hV

Premises used: IsClosed.preimage_val
-- Module: Mathlib.Topology.Sober
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) ⁻¹' V)

Tactic:
exact IsClosed.preimage_val hV

Premises used: IsClosed.preimage_val
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
V W : Set α
inst_1 : QuasiSober.{u_1} (↑V : Type u_1)
hW : IsClosed W
rw : QuasiSober.{u_1} (↑(V ∩ W) : Type u_1)
⊢ QuasiSober.{u_1} (↑(W ∩ V) : Type u_1)

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
V W : Set α
inst_1 : QuasiSober.{u_1} (↑V : Type u_1)
hW : IsClosed W
⊢ QuasiSober.{u_1} (↑(V ∩ W) : Type u_1)

Tactic:
.inter_of_isClosed_of_quasiSober_left V hW

Premises used: QuasiSober.inter_of_isClosed_of_quasiSober_left
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
V W : Set α
inst_1 : QuasiSober.{u_1} (↑V : Type u_1)
hW : IsClosed W
⊢ QuasiSober.{u_1} (↑(V ∩ W) : Type u_1)

Tactic:
exact .inter_of_isClosed_of_quasiSober_left V hW
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
x : (↑(genericPoints α) : Type u_1)
⊢ IsGenericPoint (↑x : α) (↑(component x) : Set α)

Tactic:
rfl

Premises used: IsGenericPoint, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T0Space α
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := (↑(genericPoints α) : Type u_1)) component

Tactic:
fun x y e ↦ Subtype.ext ((isGenericPoint x).eq (e ▸ isGenericPoint y))

Premises used: Eq.rec, genericPoints.isGenericPoint, IsGenericPoint.eq, Function.Injective, Eq.symm, Subtype.ext
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
x : (↑(irreducibleComponents α) : Type u_1)
⊢ IsGenericPoint (↑(ofComponent x) : α) (↑x : Set α)

Tactic:
x.2.1.isGenericPoint_genericPoint (isClosed_of_mem_irreducibleComponents x.1 x.2)

Premises used: isClosed_of_mem_irreducibleComponents, irreducibleComponents, IsIrreducible.genericPoint, Set.Mem, IsGenericPoint, setOf, IsIrreducible.isGenericPoint_genericPoint, genericPoints, And.left, Classical.choose, Maximal, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
x : (↑(irreducibleComponents α) : Type u_1)
⊢ component (ofComponent x) = x

Tactic:
Subtype.ext (isGenericPoint_ofComponent x)

Premises used: genericPoints.isGenericPoint_ofComponent, Subtype.ext
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T0Space α
inst_2 : QuasiSober α
x : (↑(genericPoints α) : Type u_1)
⊢ ofComponent (component x) = x

Tactic:
component_injective (component_ofComponent _)

Premises used: genericPoints.component_injective, genericPoints.component_ofComponent
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := (↑(genericPoints α) : Type u_1)) component

Tactic:
Function.HasRightInverse.surjective ⟨ofComponent, component_ofComponent⟩

Premises used: genericPoints.ofComponent, Function.HasRightInverse.surjective, genericPoints.component_ofComponent, Exists.intro
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T0Space α
h : (irreducibleComponents α).Finite
⊢ (genericPoints α).Finite

Tactic:
@Finite.of_injective _ _ h _ component_injective

Premises used: genericPoints.component_injective, Set.Finite, Finite.of_injective
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
⊢ _root_.closure (genericPoints α) = univ

Tactic:
Set.eq_univ_iff_forall.mpr fun x ↦ Set.subset_def.mp ?_ x mem_irreducibleComponent

Premises used: Iff.mpr, Set.subset_def, Set.eq_univ_iff_forall, Eq.mp, mem_irreducibleComponent
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
refine : ∀ (x : α), irreducibleComponent x ⊆ _root_.closure (genericPoints α)
⊢ _root_.closure (genericPoints α) = univ

Tactic:
refine Set.eq_univ_iff_forall.mpr fun x ↦ Set.subset_def.mp ?_ x mem_irreducibleComponent

Premises used: Iff.mpr, Set.subset_def, Set.eq_univ_iff_forall, Eq.mp, mem_irreducibleComponent
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
x : α
⊢ irreducibleComponent x ⊆ _root_.closure (genericPoints α)

Tactic:
(isGenericPoint_ofComponent
    ⟨_, irreducibleComponent_mem_irreducibleComponents x⟩).symm.trans_subset (closure_mono ?_)

Premises used: irreducibleComponent_mem_irreducibleComponents, genericPoints.isGenericPoint_ofComponent, closure_mono, Subtype.mk, Classical.choose, Eq.symm, Eq.trans_subset, irreducibleComponent
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
x : α
refine :
  {(↑(ofComponent (Subtype.mk (p := fun (x : Set α) ↦ x ∈ irreducibleComponents α) (irreducibleComponent x) ⋯)) : α)} ⊆
    genericPoints α
⊢ irreducibleComponent x ⊆ _root_.closure (genericPoints α)

Tactic:
refine (isGenericPoint_ofComponent
    ⟨_, irreducibleComponent_mem_irreducibleComponents x⟩).symm.trans_subset (closure_mono ?_)

Premises used: irreducibleComponent_mem_irreducibleComponents, genericPoints.isGenericPoint_ofComponent, closure_mono, Subtype.mk, Eq.symm, Eq.trans_subset
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
x : α
⊢ {(↑(ofComponent (Subtype.mk (p := fun (x : Set α) ↦ x ∈ irreducibleComponents α) (irreducibleComponent x) ⋯)) : α)} ⊆
    genericPoints α

Tactic:
Set.singleton_subset_iff.mpr (ofComponent _).2

Premises used: Iff.mpr, Set.singleton_subset_iff, genericPoints.ofComponent, Subtype.property
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
x : α
⊢ {(↑(ofComponent (Subtype.mk (p := fun (x : Set α) ↦ x ∈ irreducibleComponents α) (irreducibleComponent x) ⋯)) : α)} ⊆
    genericPoints α

Tactic:
exact Set.singleton_subset_iff.mpr (ofComponent _).2

Premises used: Iff.mpr, Set.singleton_subset_iff, genericPoints.ofComponent, Subtype.property
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : IrreducibleSpace α
inst_3 : T0Space α
h : ∀ (x : α), x ∈ genericPoints α ↔ Membership.mem (γ := Set α) {genericPoint α} x
⊢ genericPoints α = {genericPoint α}

Tactic:
ext x
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : IrreducibleSpace α
inst_3 : T0Space α
x : α
h :
  Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Set (Set α)) {univ} (closure {x})} x ↔
    Membership.mem (γ := Set α) {genericPoint α} x
⊢ x ∈ genericPoints α ↔ Membership.mem (γ := Set α) {genericPoint α} x

Tactic:
rw [genericPoints, irreducibleComponents_eq_singleton]

Premises used: irreducibleComponents_eq_singleton, genericPoints
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : IrreducibleSpace α
inst_3 : T0Space α
x : α
⊢ Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Set (Set α)) {univ} (closure {x})} x ↔
    Membership.mem (γ := Set α) {genericPoint α} x

Tactic:
⟨((genericPoint_spec α).eq · |>.symm), (· ▸ genericPoint_spec α)⟩

Premises used: Eq.rec, genericPoint_spec, IsGenericPoint.eq, Iff.intro, Eq.symm
-- Module: Mathlib.Topology.Sober
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : QuasiSober α
inst_2 : IrreducibleSpace α
inst_3 : T0Space α
x : α
⊢ Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Set (Set α)) {univ} (closure {x})} x ↔
    Membership.mem (γ := Set α) {genericPoint α} x

Tactic:
exact ⟨((genericPoint_spec α).eq · |>.symm), (· ▸ genericPoint_spec α)⟩
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Specialization α ≃ α) (Equiv.symm toEquiv) ofEquiv

Tactic:
rfl

Premises used: Specialization, Equiv.symm, Equiv.refl, rfl, Specialization.ofEquiv
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ Specialization α) (Equiv.symm ofEquiv) toEquiv

Tactic:
rfl

Premises used: Specialization.toEquiv, Specialization, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
a : Specialization α
⊢ (toEquiv : (a : α) → Specialization α) ((ofEquiv : (a : Specialization α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
a : α
⊢ (ofEquiv : (a : Specialization α) → α) ((toEquiv : (a : α) → Specialization α) a : Specialization α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
a b : α
⊢ Eq (α := Specialization α) ((toEquiv : (a : α) → Specialization α) a : Specialization α)
      ((toEquiv : (a : α) → Specialization α) b : Specialization α) ↔
    a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Specialization
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
a b : Specialization α
⊢ Eq (α := α) ((ofEquiv : (a : Specialization α) → α) a : α) ((ofEquiv : (a : Specialization α) → α) b : α) ↔ a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Specialization
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
inst : TopologicalSpace α
a b : α
⊢ LE.le (α := Specialization α) ((toEquiv : (a : α) → Specialization α) a : Specialization α)
      ((toEquiv : (a : α) → Specialization α) b : Specialization α) ↔
    b ⤳ a

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
inst : TopologicalSpace α
a b : Specialization α
⊢ Specializes (X := α) ((ofEquiv : (a : Specialization α) → α) a : α) ((ofEquiv : (a : Specialization α) → α) b : α) ↔
    b ≤ a

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set (Specialization α)
⊢ IsOpen[inst] ((⇑toEquiv : (a : α) → Specialization α) ⁻¹' s) ↔ IsUpperSet s

Tactic:
isOpen_iff_forall_specializes.trans forall_comm

Premises used: forall_comm, Iff.trans, isOpen_iff_forall_specializes
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set α
⊢ IsUpperSet (α := Specialization α) ((⇑ofEquiv : (a : Specialization α) → α) ⁻¹' s) ↔ IsOpen[inst] s

Tactic:
isOpen_toEquiv_preimage.symm

Premises used: Specialization.isOpen_toEquiv_preimage, Set.Mem, setOf, Set.preimage, Iff.symm
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq (α := Specialization α →o Specialization α) (map (ContinuousMap.id α)) OrderHom.id

Tactic:
rfl

Premises used: OrderHom.id, Specialization.map, rfl
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
⊢ map (g.comp f) = (map g).comp (map f)

Tactic:
rfl

Premises used: OrderHom.comp, Specialization.map, rfl
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
inst : Preorder α
⊢ ∀ {a b : α},
    LE.le (α := Specialization (WithUpperSet α))
        ((Equiv.trans toUpperSet toEquiv : (a : α) → Specialization (WithUpperSet α)) a :
          Specialization (WithUpperSet α))
        ((Equiv.trans toUpperSet toEquiv : (a : α) → Specialization (WithUpperSet α)) b :
          Specialization (WithUpperSet α)) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Topology.Specialization
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : AlexandrovDiscrete α
s : Set (WithUpperSet (Specialization α))
⊢ IsOpen[inst] ((⇑(Equiv.trans toEquiv toUpperSet) : (a : α) → WithUpperSet (Specialization α)) ⁻¹' s) ↔
    IsOpen[instTopologicalSpace] s

Tactic:
simp [Set.preimage_comp]

Premises used: Set.preimage_comp
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
ho : IsOpen[inst] s
hs₁ : s ∈ constructibleTopologySubbasis X
⊢ IsOpen[constructibleTopology X] s

Tactic:
apply TopologicalSpace.isOpen_generateFrom_of_mem

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
ho : IsOpen[inst] s
⊢ s ∈ constructibleTopologySubbasis X

Tactic:
simp [constructibleTopologySubbasis, ho, hs]

Premises used: constructibleTopologySubbasis
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsCompact sᶜ
ho : IsClosed[inst] s
hs₁ : s ∈ constructibleTopologySubbasis X
⊢ IsOpen[constructibleTopology X] s

Tactic:
apply TopologicalSpace.isOpen_generateFrom_of_mem

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsCompact sᶜ
ho : IsClosed[inst] s
⊢ s ∈ constructibleTopologySubbasis X

Tactic:
simp [constructibleTopologySubbasis, ho, hs]

Premises used: constructibleTopologySubbasis
-- Module: Mathlib.Topology.Spectral.ConstructibleTopology
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ constructibleTopologySubbasis X ↔ s ∈ constructibleTopologySubbasis X

Tactic:
grind [constructibleTopologySubbasis, isClosed_compl_iff, compl_compl]

Premises used: compl_compl, constructibleTopologySubbasis, isClosed_compl_iff