mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst✝] (t i)
i₀ : ι := hι.some
this : (t i₀ ∩ ⋂ i, t i).Nonempty
⊢ (⋂ i, t i).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst✝] (t i)
⊢ (⋂ i, t i).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type v
hι : Nonempty ι
t : ι → Set X
htd : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
htn : ∀ (i : ι), (t i).Nonempty
htc : ∀ (i : ι), IsCompact (t i)
htcl : ∀ (i : ι), IsClosed[inst✝] (t i)
⊢ (⋂ i, t i).Nonempty

Tactic:
by
  let i₀ := hι.some
  suffices (t i₀ ∩ ⋂ i, t i).Nonempty by
    rwa [inter_eq_right.mpr (iInter_subset _ i₀)] at this
  simp only [nonempty_iff_ne_empty] at htn ⊢
  apply mt ((htc i₀).elim_directed_family_closed t htcl)
  push Not
  simp only [← nonempty_iff_ne_empty] at htn ⊢
  refine ⟨htd, fun i => ?_⟩
  rcases htd i₀ i with ⟨j, hji₀, hji⟩
  exact (htn j).mono (subset_inter hji₀ hji)

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : Nonempty ↑S
hSd : DirectedOn (fun x1 x2 ↦ x1 ⊇ x2) S
hSn : ∀ U ∈ S, U.Nonempty
hSc : ∀ U ∈ S, IsCompact U
hScl : ∀ U ∈ S, IsClosed[inst✝] U
⊢ (⋂₀ S).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set X
b : Set ι
c : ι → Set X
hs : IsCompact s
hc₁ : ∀ i ∈ b, IsOpen[inst✝] (c i)
hc₂ : s ⊆ ⋃ i ∈ b, c i
⊢ ∃ b' ⊆ b, b'.Finite ∧ s ⊆ ⋃ i ∈ b', c i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen[inst✝] (U i)) → s ⊆ ⋃ i, U i → ∃ t, s ⊆ ⋃ i ∈ t, U i
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
⊢ s ∈ 𝓝ˢ ∅ ×ˢ l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
⊢ s ∈ 𝓝ˢ K ×ˢ l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hs : s ∈ ⨆ x ∈ K, 𝓝 x ×ˢ l
⊢ ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: Y : Type v
inst✝ : TopologicalSpace Y
K : Set Y
hK : IsCompact K
X : Type u_2
l : Filter X
⊢ l ×ˢ 𝓝ˢ K = ⨆ y ∈ K, l ×ˢ 𝓝 y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: Y : Type v
inst✝ : TopologicalSpace Y
K : Set Y
X : Type u_2
l : Filter X
s : Set (X × Y)
hK : IsCompact K
hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y
⊢ s ∈ ⨆ y ∈ K, l ×ˢ 𝓝 y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l f : Filter X
⊢ f ⊓ l = comap Function.diag (f ×ˢ l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A B : Set α
h : A ⊆ B
⊢ A ↓∩ B = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
⊢ 𝓝ˢ K ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
⊢ l ⊓ 𝓝ˢ K = ⨆ x ∈ K, l ⊓ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l
⊢ s ∈ ⨆ x ∈ K, 𝓝 x ⊓ l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋃₀ S = ⋃₀ {x | ∃ B ∈ S, A ↓∩ B = x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ y ∈ K, s ∈ l ⊓ 𝓝 y
⊢ s ∈ ⨆ x ∈ K, l ⊓ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ : X
K : Set Y
hK : IsCompact K
P : X → Y → Prop
hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in 𝓝 (x₀, y), P z.1 z.2
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂₀ {x | ∃ B ∈ S, A ↓∩ B = x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
x✝ : Filter X
hf : x✝.NeBot
hfa : x✝ ≤ 𝓟 {x}
⊢ 𝓟 {x} ≤ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Ici a) = Ici (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
S : Set (Set α)
⊢ A ↓∩ ⋂₀ S = ⋂₀ ((fun x ↦ A ↓∩ x) '' S)

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Ioi a) = Ioi (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
a : α
⊢ Ioi a = ⊤ ↔ a = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
S : Set α
c : α
⊢ c ∈ Ici (sSup S) ↔ c ∈ ⨆ a ∈ S, Ici a

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A B C : Set α
hB : B ⊆ A
hC : C ⊆ A
h : A ↓∩ B = A ↓∩ C
⊢ B = C

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ⋃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
rw [Ultrafilter.finite_biUnion_mem_iff hs] at hl

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ∃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
ι : Sort u_3
inst✝ : CompleteLattice α
f : ι → α
c : α
⊢ c ∈ Ici (⨆ i, f i) ↔ c ∈ ⨆ i, Ici (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Principal

Goal state before:
pp: α : Type u_1
ι : Sort u_3
κ : ι → Sort u_4
inst✝ : CompleteLattice α
f : (i : ι) → κ i → α
⊢ Ici (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, Ici (f i j)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ⋃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
D : Set ↑A
⊢ Subtype.val '' Dᶜ = A \ Subtype.val '' D

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsCompact s
⊢ IsCompact (⋃₀ S)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
T : Set (Set ↑A)
⊢ Subtype.val '' ⋃₀ T = ⋃₀ {x | ∃ B ∈ T, Subtype.val '' B = x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ {x} ∈ {s | IsCompact s} ∧ x ∈ {x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsCompact s
⊢ ∀ (x : X), {x} ∈ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
T : Set (Set ↑A)
hT : T.Nonempty
⊢ Subtype.val '' ⋂₀ T = ⋂₀ {x | ∃ B ∈ T, Subtype.val '' B = x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsCompact s
⊢ s.Finite

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
D E : Set ↑A
⊢ D ⊆ A ↓∩ Subtype.val '' E ↔ D ⊆ E

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
b : Bool
⊢ IsCompact (bif b then s else t)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

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

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Fibration

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 ↦ x1 ≤ x2) (fun x1 x2 ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
⊢ IsLowerSet (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
⊢ (⋂ i, V i ∩ Wᶜ).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
this : (⋂ i, V i ∩ Wᶜ).Nonempty
⊢ ¬⋂ i, V i ⊆ W

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
⊢ ∃ i, V i ⊆ U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, ↑F ≤ 𝓝 x
⊢ ∀ x ∈ s, ∃ t, x ∈ t ∧ t ∈ S ∧ t ∉ F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, ↑F ≤ 𝓝 x
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
⊢ U '' s ⊆ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, ↑F ≤ 𝓝 x
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
x : X
hx : x ∈ s
⊢ U x ∈ U '' s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, ↑F ≤ 𝓝 x
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
Q : Set (Set X)
hQU : Q ⊆ U '' s
hQ : Q.Finite
hsQ : s ⊆ ⋃₀ Q
this : ∀ s ∈ Q, s ∉ F
⊢ ⋂₀ (compl '' Q) ∈ (↑F).sets

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ↑(upperClosure s) = ⋃ a ∈ s, Ici a

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ upperClosure (⇑f '' s) = (UpperSet.map f) (upperClosure s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ⨅ a ∈ s, Ici a = upperClosure s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, ↑F ≤ 𝓝 x
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
Q : Set (Set X)
hQU : Q ⊆ U '' s
hQ : Q.Finite
hsQ : s ⊆ ⋃₀ Q
this : ∀ s ∈ Q, s ∉ F
hQF : ⋂₀ (compl '' Q) ∈ (↑F).sets
⊢ ⋃₀ Q ∉ F

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ upperClosure s = ⊤ ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ upperClosure {a} = UpperSet.Ici a

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
S : Set (Set α)
⊢ upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ BddBelow ↑(upperClosure s) ↔ BddBelow s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
⊢ IsCompact s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint (↑(upperClosure s)) t ↔ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : IsLowerSet s
⊢ Disjoint s ↑(upperClosure t) ↔ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ (ι : Type u) (U : ι → ↑S), s ⊆ ⋃ i, ↑(U i) → ∃ J, J.Finite ∧ s ⊆ ⋃ i ∈ J, ↑(U i)
P : Set (Set X)
hP : P ⊆ S
hs : s ⊆ ⋃₀ P
J : Set ↑P
hJ : J.Finite
cover : s ⊆ ⋃ i ∈ J, ↑⟨↑i, ⋯⟩
⊢ (fun x ↦ ↑x) '' J ⊆ P

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ (ι : Type u) (U : ι → ↑S), s ⊆ ⋃ i, ↑(U i) → ∃ J, J.Finite ∧ s ⊆ ⋃ i ∈ J, ↑(U i)
P : Set (Set X)
hP : P ⊆ S
hs : s ⊆ ⋃₀ P
J : Set ↑P
hJ : J.Finite
cover : s ⊆ ⋃ i ∈ J, ↑⟨↑i, ⋯⟩
⊢ s ⊆ ⋃₀ ((fun x ↦ ↑x) '' J)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ cocompact X = cofinite

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ Disjoint (cocompact X) f ↔ ∃ K ∈ f, IsCompact K

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ Disjoint f (cocompact X) ↔ ∃ K ∈ f, IsCompact K

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
⊢ Minimal (fun x ↦ x ∈ upperClosure s) x ↔ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMinOrder α
s : Set α
h₁ : upperClosure s = ⊥
h₂ : BddBelow s
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.sdiff {a} = s.erase a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
⊢ l ≤ 𝓟 (insert y (range f)) → ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
hle

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
⊢ s.sdiff t = s ↔ Disjoint (↑s) t

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
⊢ s.erase a = s ↔ a ∉ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
s t : UpperSet α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
K : Set X
hKc : IsCompact K
hKs : Kᶜ ⊆ f ⁻¹' s
⊢ f '' K ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : UpperSet α
⊢ ↑s = univ ↔ s = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ s.sdiff t ⊓ upperClosure t = s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : UpperSet α
⊢ ↑s = ∅ ↔ s = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨆ i, f i) = ⋂ i, ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨅ i, f i) = ⋃ i, ↑(f i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨅ i, f i) = ⋃ i, ↑(f i)

Tactic:
by simp [iInf]

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ ↑(⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, ↑(f i j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ upperClosure t ⊓ s.sdiff t = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
⊢ IsCompact (insert y (range f))

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
f : (i : ι) → κ i → UpperSet α
⊢ ↑(⨅ i, ⨅ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : LE α
S : Set (UpperSet α)
a : α
⊢ (∃ i, ∃ (_ : i ∈ S), a ∈ ↑i) ↔ ∃ s ∈ S, a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
f : ι → X
x : X
hf : Tendsto f cofinite (𝓝 x)
⊢ IsCompact (insert x (range f))

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⨆ i, f i ↔ ∀ (i : ι), a ∈ f i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ (coclosedCompact X).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) compl

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ s.erase a ⊓ Ici a = s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → UpperSet α
⊢ a ∈ ⨅ i, f i ↔ ∃ i, a ∈ f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ a ∈ ⨆ i, ⨆ j, f i j ↔ ∀ (i : ι) (j : κ i), a ∈ f i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ a ∈ ⨅ i, ⨅ j, f i j ↔ ∃ i j, a ∈ f i j

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ Ici a ⊓ s.erase a = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedCompact X ↔ IsCompact (closure[inst✝] sᶜ)

Tactic:
by

Goal state after: