mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ IsCompact W₂ᶜᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Nontrivial (NonemptyCompacts α) ↔ Nontrivial α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝² : PartialOrder P
inst✝¹ : OrderTop P
inst✝ : Nontrivial P
⊢ ∃ I, I.IsMaximal

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : NonemptyCompacts α
⊢ NonemptyCompacts.map id ⋯ K = K

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ x₁ ∈ Z ∩ W₁ᶜᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ IsRetrocompact s ↔ IsSpectralMap Subtype.val

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
K : NonemptyCompacts α
⊢ NonemptyCompacts.map (f ∘ g) ⋯ K = NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
x : α
⊢ NonemptyCompacts.map f hf {x} = {f x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (NonemptyCompacts.map f hf)
x✝² x✝¹ : α
x✝ : ((fun x ↦ {x}) ∘ f) x✝² = ((fun x ↦ {x}) ∘ f) x✝¹
⊢ NonemptyCompacts.map f hf ((fun x ↦ {x}) x✝²) = NonemptyCompacts.map f hf ((fun x ↦ {x}) x✝¹)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : T2Space α
inst✝ : T2Space β
K : NonemptyCompacts α
L : NonemptyCompacts β
⊢ (K ×ˢ L).toCloseds = K.toCloseds ×ˢ L.toCloseds

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ x₂ ∈ Z ∩ W₂ᶜᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : PositiveCompacts α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
⊢ IsGenericPoint x S ↔ ∀ (y : α), x ⤳ y ↔ y ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S U : Set α
h : IsGenericPoint x S
hU : IsOpen U
⊢ Disjoint S U ↔ x ∉ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S Z : Set α
h : IsGenericPoint x S
hZ : IsClosed Z
⊢ x ∈ Z ↔ S ⊆ Z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
x : α
S : Set α
h : IsGenericPoint x S
f : α → β
hf : Continuous f
⊢ IsGenericPoint (f x) (closure (f '' S))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ S ⊆ ⋂₀ {t | IsClosed t ∧ {x} ⊆ t} ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
subset_sInter_iff,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
this : closure {x} ⊆ S
⊢ (∀ t' ∈ {t | IsClosed t ∧ {x} ⊆ t}, S ⊆ t') ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
S : Set α
hS : IsClosed S
hxS : x ∈ S
⊢ IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : WeaklyLocallyCompactSpace α
inst✝ : Nonempty α
⊢ Nonempty (PositiveCompacts α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ IsGenericPoint hS.genericPoint S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
K : PositiveCompacts α
L : PositiveCompacts β
⊢ (interior (K.toCompacts ×ˢ L.toCompacts).carrier).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
⊢ IsGenericPoint (genericPoint α) univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsRetrocompact s
hfemb : IsEmbedding f
hfcomp : IsRetrocompact (range f)
⊢ IsRetrocompact (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
x : α
⊢ x ∈ closure univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s t : CompactOpens α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
s : TopologicalSpace.IrreducibleCloseds α
⊢ (fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }) ((fun s ↦ ⋯.genericPoint) s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
x : α
⊢ IsGenericPoint x (closure (closure {x}))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hs : IsRetrocompact s
⊢ IsRetrocompact (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
f : ι → CompactOpens α
s : Finset ι
⊢ ↑(s.sup f) = ⋃ i ∈ s, ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : QuasiSober α
inst✝ : T0Space α
⊢ ∀ {a b : TopologicalSpace.IrreducibleCloseds α},
    { toFun := fun s ↦ ⋯.genericPoint,
            invFun := fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          a ≤
        { toFun := fun s ↦ ⋯.genericPoint,
            invFun := fun x ↦ { carrier := closure {x}, isIrreducible' := ⋯, isClosed' := ⋯ }, left_inv := ⋯,
            right_inv := ⋯ }
          b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
U : Set X
hUcomp : IsCompact U
hUopen : IsOpen[inst✝¹] U
⊢ IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace α
inst✝ : T2Space α
s t : CompactOpens α
⊢ IsClosed (↑s ⇨ ↑t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z : Set X
hZ : ¬IsPreirreducible Z
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace α
inst✝ : T2Space α
s t : CompactOpens α
⊢ IsOpen { carrier := ↑s ⇨ ↑t, isCompact' := ⋯ }.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
⊢ IsRetrocompact (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsClosedEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed[inst✝²] S✝
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ topologicalKrullDim X ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
Z : IrreducibleCloseds X
⊢ coheight (map f ⋯ Z) = coheight Z

Tactic:
by

Goal state after:
Module: Mathlib.Topology.KrullDimension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : QuasiSober Y
inst✝² : T0Space Y
inst✝¹ : QuasiSober X
inst✝ : T0Space X
x : X
f : X → Y
hf : IsOpenEmbedding f
⊢ coheight (f x) = coheight x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
⊢ x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
p : (s : Set X) → IsConstructible s → Prop
open_retrocompact : ∀ (U : Set X) (hUopen : IsOpen[inst✝] U) (hUcomp : IsRetrocompact U), p U ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), p s hs → p t ht → p (s ∪ t) ⋯
compl : ∀ (s : Set X) (hs : IsConstructible s), p s hs → p sᶜ ⋯
s : Set X
hs : IsConstructible s
⊢ p s hs

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
x : β
T : Set β
hT : IsClosed[inst✝¹] T
hS : IsIrreducible (f ⁻¹' T)
hS' : IsClosed[inst✝²] (f ⁻¹' T)
hS'' : IsIrreducible (T ∩ range f)
hx : IsGenericPoint x (closure[inst✝¹] (T ∩ range f))
hxT : x ∈ T
⊢ x ∈ range f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
inst✝ : QuasiSober β
S✝ : Set α
hS : IsIrreducible S✝
hS' : IsClosed[inst✝²] S✝
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hfcont : Continuous[inst✝¹, inst✝] f
hf : ∀ (s : Set Y), IsOpen[inst✝] s → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
hs : IsConstructible s
⊢ IsConstructible (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Opens α
hU : IsOpenCover U
⊢ QuasiSober α ↔ ∀ (i : ι), QuasiSober ↥(U i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hfopen : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hs : IsConstructible s
⊢ IsConstructible (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
⊢ IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
inst✝ : ∀ (s : ↑S), QuasiSober ↑↑s
hS' : ⋃₀ S = ⊤
⊢ TopologicalSpace.IsOpenCover fun s ↦ { carrier := ↑s, is_open' := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
U : Set X
hUopen : IsOpen[inst✝¹] U
hUcomp : IsRetrocompact U
hfU : IsOpen[inst✝] (f '' U ∪ (range f)ᶜ)
h : IsRetrocompact (f '' U ∪ (range f)ᶜ)
⊢ IsConstructible (f '' U)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
⊢ ∃ x, IsGenericPoint x S✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑W
hV : IsClosed V
⊢ QuasiSober ↑(W ∩ V)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
V W : Set α
inst✝ : QuasiSober ↑V
hW : IsClosed W
⊢ QuasiSober ↑(W ∩ V)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
⊢ _root_.closure (genericPoints α) = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : QuasiSober α
inst✝¹ : IrreducibleSpace α
inst✝ : T0Space α
⊢ genericPoints α = {genericPoint α}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsClosedEmbedding f
hfcomp : IsRetrocompact (range f)ᶜ
hs : IsConstructible s
⊢ IsConstructible (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsOpenEmbedding f
hfcomp : IsRetrocompact (range f)
hsf : s ⊆ range f
hs : IsConstructible (f ⁻¹' s)
⊢ IsConstructible s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
⊢ V₁ ⊆ ⋃ i, (U i).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
x : X
hx₁ : x ∈ V₁
hx₂ : x ∈ V₂
i : ι
hi : i ∈ t
hxi : x ∈ (U i).carrier
⊢ x ∈ ↑(U i) ∩ V₁ ∩ (↑(U i) ∩ V₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
⊢ IsCompact (V₁ ∩ V₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : CompactSpace X
hs : IsRetrocompact s
⊢ IsCompact s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s : Set X
hs : IsConstructible s
⊢ P s hs

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ univ ∈ 𝓝 x✝

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ IsOpen[inst✝] univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ IsRetrocompact (range Subtype.val)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsConstructible s
x✝ : X
⊢ s ⊆ range Subtype.val

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
⊢ IsLocallyConstructible (s ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
t : ι → Set X
i : ι
s : Finset ι
ih : i ∉ s
hi : (∀ i ∈ s, IsLocallyConstructible (t i)) → IsLocallyConstructible (s.inf t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsLocallyConstructible (t i_1)
⊢ i ∈ Finset.cons i s ih

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf' hs t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝] U
hsU : IsConstructible (U ↓∩ s)
V : Set X
hxV : V ∈ 𝓝 x
hV : IsOpen[inst✝] V
htV : IsConstructible (V ↓∩ t)
⊢ (U ∩ V) ↓∩ (s ∪ t) = inclusion ⋯ ⁻¹' U ↓∩ s ∪ inclusion ⋯ ⁻¹' V ↓∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLocallyConstructible s
ht : IsLocallyConstructible t
⊢ IsLocallyConstructible (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsLocallyConstructible s
hf : IsOpenEmbedding f
⊢ IsLocallyConstructible (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝²] U
hUs : IsConstructible (U ↓∩ s)
V : Set X
hV₁ : IsOpen[inst✝²] V
hV₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ U
this : IsConstructible (V ↓∩ s)
⊢ IsRetrocompact (range Subtype.val)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
x : X
U : Set X
hxU : U ∈ 𝓝 x
hU : IsOpen[inst✝²] U
hUs : IsConstructible (U ↓∩ s)
V : Set X
hV₁ : IsOpen[inst✝²] V
hV₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ U
this : IsConstructible (V ↓∩ s)
⊢ IsConstructible (V ∩ s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
this : ∀ (x : X), ∃ U, IsOpen[inst✝²] U ∧ IsCompact U ∧ x ∈ U ∧ IsConstructible (U ∩ s)
⊢ IsConstructible s

Tactic:
choose U hU hU' hxU hUs using this

Goal state after:
X : Type u_2
inst✝² : TopologicalSpace X
s t : Set X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
hs : IsLocallyConstructible s
hst : s ⊆ t
ht : IsCompact t
U : X → Set X
hU : ∀ (x : X), IsOpen[inst✝²] (U x)
hU' : ∀ (x : X), IsCompact (U x)
hxU : ∀ (x : X), x ∈ U x
hUs : ∀ (x : X), IsConstructible (U x ∩ s)
⊢ IsConstructible s