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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace Y
f : X → Y
hf : IsOpenEmbedding f
⊢ IsTopologicalBasis {U | IsOpen[inst✝²] U ∧ IsCompact U}

Tactic:
by

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
ι : Type u_3
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), PrespectralSpace (X i)
U : Set ((i : ι) × X i)
hU : U ∈ ⋃ i, (fun u ↦ Sigma.mk i '' u) '' {U | IsOpen[inst✝¹ i] U ∧ IsCompact U}
⊢ IsCompact U

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
⊢ Opens.IsBasis {U | IsCompact ↑U}

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
⊢ ⊥ ∈ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯ }.carrier

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
U₁ : CompactOpens X
h₁ : U₁ ∈ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯ }.carrier
U₂ : CompactOpens X
h₂ : U₂ ∈ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯ }.carrier
⊢ U₁ ⊔ U₂ ∈ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯ }.carrier

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a = ∅
⊢ ∀ t ∈ b, IsClosed[inst✝¹] t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a = ∅
⊢ ⋂₀ b ⊆ t

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
⊢ (fun I ↦ ⨆ U ∈ I, U.toOpens) ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U) =
    U

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : ↑U.toOpens ⊆ ⋃ i ∈ I, ↑i.toOpens
s : Set (CompactOpens X)
hsI : s ⊆ ↑I
hs : s.Finite
hU : ↑U ⊆ ⋃ i ∈ s, ↑i.toOpens
⊢ U ≤ hs.toFinset.sup fun i ↦ i

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
U : CompactOpens X
H : ↑U.toOpens ⊆ ⋃ i ∈ I, ↑i.toOpens
s : Set (CompactOpens X)
hsI : s ⊆ ↑I
hs : s.Finite
hU : ↑U ⊆ ⋃ i ∈ s, ↑i.toOpens
⊢ (hs.toFinset.sup fun i ↦ i) ∈ ↑I

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
I : Order.Ideal (CompactOpens X)
⊢ (fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) ((fun I ↦ ⨆ U ∈ I, U.toOpens) I) =
    I

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ a ⊆ s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U V : Opens X
⊢ { toFun := fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ },
          invFun := fun I ↦ ⨆ U ∈ I, U.toOpens, left_inv := ⋯, right_inv := ⋯ }
        U ≤
      { toFun := fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ },
          invFun := fun I ↦ ⨆ U ∈ I, U.toOpens, left_inv := ⋯, right_inv := ⋯ }
        V ↔
    U ≤ V

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
x : X
hx : f x ∈ U
⊢ ?m.109 ∈ sSup ?m.108

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : LE P
s t : Ideal P
x✝ : s.toLowerSet = t.toLowerSet
⊢ s = t

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
⊢ ?m.62

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : LE P
I : Ideal P
p : P
notMem : p ∉ I
hp : ↑I = univ
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : IsCodirectedOrder P
I J : Ideal P
⊢ (↑I ∩ ↑J).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝² : LE P
inst✝¹ : IsDirectedOrder P
inst✝ : Nonempty P
I : Ideal P
hI : IsCoatom I
x✝ : Ideal P
hJ : I < x✝
⊢ ↑x✝ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
t : Set α
ht : t ∈ s
hno : ¬IsOpen[inst✝¹] t
ha : a.Nonempty
⊢ ∀ t ∈ b, IsClosed[inst✝¹] t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
⊢ I.IsProper ↔ ⊤ ∉ I

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : Preorder P
inst✝ : OrderBot P
⊢ ∀ (a : Ideal P), principal ⊥ ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : PartialOrder P
inst✝ : OrderTop P
a : P
⊢ (principal a).IsProper ↔ a ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_2
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
s : Finset ι
⊢ s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
⊢ IsCompact (⋂₀ s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x✝ : P
I✝ J✝ s t I J : Ideal P
x : P
hx : x ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
y : P
hy : y ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
⊢ (fun x1 x2 ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun x1 x2 ↦ x1 ≤ x2) y (x ⊔ y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I✝ J✝ s t I J : Ideal P
⊢ {x | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSeparatedSpace α
inst✝ : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t
hc : ∀ t ∈ s, IsCompact t
⊢ IsCompact (⋂₀ s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : IsCodirectedOrder P
x : P
I : Ideal P
hx : x ∉ I
h : I = I ⊔ principal x
⊢ x ∈ I

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
⊢ ∃ V, IsCompact V.carrier ∧ f '' ↑V = U

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ ⊥ ∈ (⨅ s ∈ S, s.toLowerSet).carrier

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ IsCompact ∅ ∧ IsOpen[inst✝¹] ∅ ∧ ∅ ⊆ ∅ ∧ ∅ ⊆ U

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
a : P
ha : a ∈ (⨅ s ∈ S, s.toLowerSet).carrier
b : P
hb : b ∈ (⨅ s ∈ S, s.toLowerSet).carrier
⊢ a ⊔ b ∈ (⨅ s ∈ S, s.toLowerSet).carrier

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 : Compacts α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S : Set (Ideal P)
⊢ x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
K U : Set X
hK : IsCompact K
hU : IsOpen[inst✝¹] U
hKU : K ⊆ U
⊢ ∃ W, IsCompact W ∧ IsOpen[inst✝¹] W ∧ K ⊆ W ∧ W ⊆ U

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S✝ S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
⊢ s ≤ sInf S

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : SemilatticeSup P
inst✝ : OrderBot P
x : P
S✝ S : Set (Ideal P)
⊢ IsGLB S (sInf S)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_4
s : Finset ι
f : ι → Compacts α
⊢ ↑(s.sup f) = s.sup fun i ↦ ↑(f i)

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₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
⊢ ∃ x₁ ∈ U₁, x₁ ∈ Z ∧ x₁ ∉ U₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K L : Compacts α
h : Disjoint K L
⊢ Disjoint ↑K ↑L

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✝ : Nonempty α
⊢ Nontrivial (Compacts α)

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₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] 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₂ ∈ U₂, x₂ ∈ Z ∧ x₂ ∉ U₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
⊢ x ∉ I

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ Subsingleton (Compacts α) ↔ IsEmpty α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
⊢ x ∉ I ∨ xᶜ ∉ I

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
hs : s.Finite
⊢ ⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : CompleteLattice P
I : Ideal P
α : Sort u_2
inst✝ : Finite α
f : α → P
⊢ ⨆ i, f i ∈ I ↔ ∀ (i : α), f i ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : CompleteLattice P
I : Ideal P
α : Sort u_2
inst✝ : Finite α
f : α → P
⊢ ⨆ i, f i ∈ I ↔ ∀ (i : α), f i ∈ I

Tactic:
by
  simpa [← Equiv.plift.symm.iSup_comp, Equiv.plift.forall_congr_left]
    using biSup_mem_iff (f := f ∘ PLift.down) Set.finite_univ

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
⊢ Function.Injective (Compacts.map f hf) ↔ Function.Injective 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 γ
f : α ≃ₜ β
s : Compacts α
⊢ Compacts.map ⇑f.symm ⋯ (Compacts.map ⇑f ⋯ s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
⊢ Monotone (sequenceOfCofinals p 𝒟)

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 : α ≃ₜ β
s : Compacts β
⊢ Compacts.map ⇑f ⋯ (Compacts.map ⇑f.symm ⋯ s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : Preorder P
p : P
ι : Type u_2
inst✝ : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i

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 : Compacts α
L : Compacts β
⊢ (K ×ˢ L).toCloseds = K.toCloseds ×ˢ L.toCloseds

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) C
hNe : C.Nonempty
⊢ IsIdeal (⋃₀ C)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
L : ↑K.compactNhds
⊢ ∃ U, ↑K ⊆ ↑U ∧ ↑U ⊆ ↑↑L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
⊢ IsRetrocompact ∅

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
⊢ IsRetrocompact Set.univ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
U : Opens α
h : U ∈ K.openRcNhds
x : ↥K
⊢ ↑x ∈ ↑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₂
⊢ IsClosed[inst✝¹] W₁ᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : Compacts α
U : Opens α
h : U ∈ K.openRcNhds
⊢ { carrier := closure[inst✝] ↑U, isCompact' := ⋯ } ∈ K.compactNhds

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, IsRetrocompact (t i)) → IsRetrocompact (s.sup t)
ht : ∀ i_1 ∈ Finset.cons i s ih, IsRetrocompact (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, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup t)

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 : NonemptyCompacts α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ 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
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.sup' hs 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 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₂
⊢ IsClosed[inst✝¹] W₂ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ range toCompacts = {⊥}ᶜ

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₂
⊢ IsCompact W₁ᶜᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
⊢ IsCoatomic (Ideal P)

Tactic:
by

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

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

Tactic:
simp_rw [← not_isEmpty_iff, isEmpty_iff]

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Constructible

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

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✝ : Subsingleton α
⊢ Subsingleton (NonemptyCompacts α)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
I : Ideal P
hI : I.IsProper
⊢ ∃ J, I ≤ J ∧ J.IsMaximal

Tactic:
by

Goal state after: