mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : UpperSet α
⊢ Codisjoint ↑s ↑t ↔ Disjoint s t

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:
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : LE α
S : Set (UpperSet α)
⊢ ↑(sSup S).compl = ↑(⨆ s ∈ S, s.compl)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
S : Set (UpperSet α)
⊢ ↑(sInf S).compl = ↑(⨅ s ∈ S, s.compl)

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).compl = ↑(⨆ i, (f i).compl)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
x : α
inst✝ : DecidableEq α
y : β
⊢ ContinuousWithinAt (update f x y) s x ↔ Tendsto (update f x y) (𝓝[s \ {x}] x) (𝓝 y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
x : α
inst✝ : DecidableEq α
y : β
⊢ ContinuousAt (update f x y) x ↔ Tendsto f (𝓝[≠] x) (𝓝 y)

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).compl = ↑(⨅ i, (f i).compl)

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsBounded s ↔ ∃ t, IsCompact t ∧ s ⊆ t

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).compl = ⨆ i, ⨆ j, (f i j).compl

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).compl = ⨅ i, ⨅ j, (f i j).compl

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
I : Finset X
hI : (∀ x ∈ I, x ∈ s) ∧ s ⊆ ⋃ x ∈ I, U x
⊢ f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x

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✝ : LinearOrder α
⊢ LinearOrder (UpperSet α)

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✝ : LinearOrder α
⊢ LinearOrder (LowerSet α)

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
hf : ∀ (x : X), ∃ t ∈ 𝓝 x, IsBounded (f '' t)
⊢ IsBounded (f '' s)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ b ∈ (map f) s ↔ f.symm b ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ map (OrderIso.refl α) = OrderIso.refl (UpperSet α)

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
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ (s ×ˢ t) = 𝓝ˢ s ×ˢ 𝓝ˢ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
⊢ (map g) ((map f) s) = (map (f.trans g)) 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
s : Set X
f : Filter Y
hs : IsCompact s
hf : Disjoint f (cocompact Y)
⊢ 𝓝ˢ s ×ˢ f ≤ 𝓝ˢ (s ×ˢ univ)

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
t : Set Y
f : Filter X
ht : IsCompact t
hf : Disjoint f (cocompact X)
⊢ f ×ˢ 𝓝ˢ t ≤ 𝓝ˢ (univ ×ˢ 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 : Filter Y
x : X
hf : Disjoint f (cocompact Y)
⊢ 𝓝 x ×ˢ f ≤ 𝓝ˢ ({x} ×ˢ univ)

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 : Filter X
y : Y
hf : Disjoint f (cocompact X)
⊢ f ×ˢ 𝓝 y ≤ 𝓝ˢ (univ ×ˢ {y})

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
s : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : IsOpen[instTopologicalSpaceProd] n
hp : s ×ˢ t ⊆ n
⊢ ∃ u v, IsOpen[inst✝¹] u ∧ IsOpen[inst✝] v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

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
s s' : Set X
t t' : Set Y
hs : IsCompact s
ht : IsCompact t
⊢ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t) = 𝓝ˢ[s'] s ×ˢ 𝓝ˢ[t'] 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
s s' : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t'] (s ×ˢ t)
⊢ ∃ u ∈ 𝓝ˢ[s'] s, ∃ v ∈ 𝓝ˢ[t'] t, u ×ˢ v ⊆ n

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
s s' : Set X
hs : IsCompact s
t : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s' ×ˢ t] (s ×ˢ t)
⊢ ∃ u ∈ 𝓝ˢ[s'] s, u ×ˢ t ⊆ n

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
s : Set X
hs : IsCompact s
t t' : Set Y
ht : IsCompact t
n : Set (X × Y)
hn : n ∈ 𝓝ˢ[s ×ˢ t'] (s ×ˢ t)
⊢ ∃ u ∈ 𝓝ˢ[t'] t, s ×ˢ u ⊆ n

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
f : Filter X
inst✝ : f.NeBot
⊢ ∃ x, ClusterPt x f

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
F : Ultrafilter X
⊢ ↑F ≤ 𝓟 univ

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Type v
inst✝ : CompactSpace X
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝¹] (t i)
hst : ∀ (s : Finset ι), (⋂ i ∈ s, t i).Nonempty
⊢ ∀ (u : Finset ι), (univ ∩ ⋂ i ∈ u, 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
inst✝ : CompactSpace X
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝¹] (t i)
hst : ∀ (s : Finset ι), (⋂ i ∈ s, t i).Nonempty
⊢ (⋂ i, t i).Nonempty

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
h : ∀ P ⊆ S, ⋃₀ P = univ → ∃ Q ⊆ P, Q.Finite ∧ ⋃₀ Q = univ
⊢ ∀ P ⊆ S, univ ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ univ ⊆ ⋃₀ Q

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
h : ∀ (ι : Type u) (U : ι → ↑S), ⋃ i, ↑(U i) = univ → ∃ J, J.Finite ∧ ⋃ i ∈ J, ↑(U i) = univ
⊢ ∀ (ι : Type u) (U : ι → ↑S), univ ⊆ ⋃ i, ↑(U i) → ∃ J, J.Finite ∧ univ ⊆ ⋃ i ∈ J, ↑(U i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
h : x ∈ closure[inst✝²] {a | p a}ᶜ
⊢ x ∉ interior {a | p a}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
⊢ y ∈ closure[inst✝] {x} ↔ ClusterPt y (pure x)

Tactic:
by

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

Goal state before:
pp: X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋂₀ (compl '' Q)).Nonempty
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
⊢ Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty

Tactic:
by

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

Goal state before:
pp: X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
⊢ CompactSpace X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
tfae_1_to_2 : x ⤳ y → pure x ≤ 𝓝 y
tfae_2_to_3 : pure x ≤ 𝓝 y → ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s
tfae_3_to_4 : (∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s) → ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s
tfae_4_to_5 : (∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s) → y ∈ closure[inst✝] {x}
tfae_6_iff_5 : closure[inst✝] {y} ⊆ closure[inst✝] {x} ↔ y ∈ closure[inst✝] {x}
tfae_5_iff_7 : y ∈ closure[inst✝] {x} ↔ ClusterPt y (pure x)
⊢ y ∈ closure[inst✝] {x} → x ⤳ y

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝ : NoncompactSpace X
⊢ (cocompact X).NeBot

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
f : X → Y
⊢ (cocompact ℤ).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ [x ⤳ y, pure x ≤ 𝓝 y, ∀ (s : Set X), IsOpen[inst✝] s → y ∈ s → x ∈ s,
      ∀ (s : Set X), IsClosed[inst✝] s → x ∈ s → y ∈ s, y ∈ closure[inst✝] {x}, closure[inst✝] {y} ⊆ closure[inst✝] {x},
      ClusterPt y (pure x)].TFAE

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
h : x ⤳ y
hd : Disjoint (𝓝 x) (𝓝 y)
⊢ ¬Disjoint (𝓝 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✝ : CompactSpace X
hs : s.Infinite
⊢ ∃ x, AccPt x (cofinite ⊓ 𝓟 s)

Tactic:
by

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

Goal state before:
pp: X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : Infinite X
⊢ ∃ z, (𝓝[≠] z).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ (𝓝 x).ker = {y | y ⤳ 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
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ comap f (cocompact Y) ≤ cocompact X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f g : X → Y
l : Filter X
y : Y
h : Tendsto g l (𝓝 y)
hl : ∀ (x : X), f x ⤳ g x
⊢ Tendsto f l (𝓝 y)

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
g : X → Y
f : Filter X
hg : Continuous[inst✝¹, inst✝] g
hf : Disjoint f (cocompact X)
⊢ Disjoint (map g f) (cocompact Y)

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
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
s : Set X
h : x ⤳ y
hf : ContinuousWithinAt f s y
hx : x ∈ s
⊢ f x ⤳ f y

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
hf : Continuous[inst✝², inst✝¹] f
inst✝ : CompactSpace X
hf' : Surjective f
⊢ IsCompact univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
hf : IsInducing f
⊢ f x ⤳ f y ↔ x ⤳ y

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
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsCompact s ↔ IsCompact (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₁ x₂ : X
y₁ y₂ : Y
⊢ (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂

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
hf : IsInducing f
hf' : IsClosed[inst✝] (range f)
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (A i)
f g : (i : ι) → A i
⊢ f ⤳ g ↔ ∀ (i : ι), f i ⤳ g i

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
hf : IsInducing f
K : Set Y
Kf : K ⊆ range f
⊢ IsCompact (f ⁻¹' K) ↔ IsCompact K

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsOpen[inst✝] S ∧ y ∈ S ∧ x ∉ S

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ IsCompact univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬x ⤳ y ↔ ∃ S, IsClosed[inst✝] S ∧ x ∈ S ∧ y ∉ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
⊢ ContinuousOn (fun a ↦ if p a then f a else g a) s

Tactic:
by

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
this : univ ∩ ⋂ i, (fun i ↦ s ↓∩ t ↑i) i = ∅
⊢ ∃ u, s ∩ ⋂ i ∈ u, t ↑i = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
⊢ Continuous[inst✝², inst✝¹] (s.piecewise f g)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsClosed[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), g x ⤳ f x
⊢ Continuous[inst✝², inst✝¹] (s.piecewise f g)

Tactic:
by

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

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
⊢ ∃ u, s ∩ ⋂ i ∈ u, t ↑i = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
hts : t ⊆ s
h : ∀ x ∈ s, ∃ y ∈ t, x ⤳ y
⊢ IsCompact 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
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderSpecialization s ↔ ∃ S, (∀ s ∈ S, IsClosed[inst✝] s) ∧ ⋃₀ S = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s ↔ ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s

Tactic:
refine ⟨?_, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderGeneralization_sInter S (fun x hx ↦ (hS x hx).stableUnderGeneralization)⟩
  rw [← stableUnderSpecialization_compl_iff, stableUnderSpecialization_iff_exists_sUnion_eq]
  exact fun ⟨S, h₁, h₂⟩ ↦ ⟨(·ᶜ) '' S, fun s ⟨t, ht, e⟩ ↦ e ▸ (h₁ t ht).isOpen_compl,
    compl_injective ((sUnion_eq_compl_sInter_compl S).symm.trans h₂)⟩

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ StableUnderGeneralization s ↔ ∃ S, (∀ s ∈ S, IsOpen[inst✝] s) ∧ ⋂₀ S = s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ SpecializingMap f ↔ ∀ (x : X), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ SpecializingMap f ↔ ∀ (x : X), StableUnderSpecialization (f '' closure[inst✝¹] {x})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ SpecializingMap f ↔ ∀ (x : X), f '' closure[inst✝¹] {x} = closure[inst✝] {f x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ SpecializingMap f ↔ ∀ (x : X), IsClosed[inst✝] (f '' closure[inst✝¹] {x})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : SpecializingMap f
hg : SpecializingMap g
⊢ SpecializingMap (g ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderSpecialization (range f)
⊢ SpecializingMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
h : StableUnderGeneralization (range f)
⊢ GeneralizingMap f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
hf : GeneralizingMap f
hg : GeneralizingMap g
⊢ GeneralizingMap (g ∘ f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsOpen[inst✝] s → (x ∈ s ↔ y ∈ s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ ¬(x ~ᵢ y) ↔ ∃ s, IsOpen[inst✝] s ∧ Xor (x ∈ s) (y ∈ s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsClosed[inst✝] s → (x ∈ s ↔ y ∈ s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ x ⤳ y ∧ y ⤳ x ↔ x ∈ closure[inst✝] {y} ∧ y ∈ closure[inst✝] {x}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ closure[inst✝] {x} = closure[inst✝] {y}

Tactic:
by

Goal state after: