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

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
e : ι' ≃ ι
h : LocallyFinite (f ∘ ⇑e)
⊢ LocallyFinite f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι ⊕ ι' → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
s : Set X
hs : IsLocallyClosed s
⊢ IsLocallyClosed (range Subtype.val)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : Option ι → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ some)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
s : Set X
f : ι → Set X
hf : LocallyFinite f
hs : IsCompact s
⊢ {i | (f i ∩ s).Nonempty}.Finite

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : ι → Set X
hf : LocallyFinite f
⊢ {i | (f i).Nonempty}.Finite

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
⊢ univ.Finite

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ ⋃ i, s i = ⋃ i, ⋃ n, K i n

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ ⋃ i, ⋃ n, K i n = ⋃ i, ⋃ n, Function.uncurry K (i, n)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp✝ : ∀ (i : ι), IsSigmaCompact (s i)
K : ι → ℕ → Set X
hcomp : ∀ (i : ι) (n : ℕ), IsCompact (K i n)
hcov : ∀ (i : ι), ⋃ n, K i n = s i
⊢ ⋃ i, ⋃ n, Function.uncurry K (i, n) = ⋃ x, Function.uncurry K x

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsSigmaCompact (s i)
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x : X
⊢ ∀ᶠ (y : X) in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (E i)
s : (i : ι) → Set (Set (E i))
hs : ∀ (i : ι), IsTopologicalBasis (s i)
⊢ IsTopologicalBasis (⋃ i, (fun u ↦ Sigma.mk i '' u) '' s i)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
⊢ IsSigmaCompact (⋃ i ∈ s, S i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
ι : Type u_1
E : ι → Type u_2
inst✝² : (i : ι) → TopologicalSpace (E i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), SecondCountableTopology (E i)
⊢ SecondCountableTopology ((i : ι) × E i)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : IsSigmaCompact t
hs : IsClosed[inst✝] s
h : s ⊆ t
⊢ IsSigmaCompact s

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f
⊢ sᶜ ∈ f

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsSigmaCompact s
hf : ContinuousOn f s
⊢ IsSigmaCompact (f '' s)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
n : ℕ
⊢ f '' (f ⁻¹' L n ∩ s) = L n

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
⊢ sᶜ ∈ f

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ ⋃ n, f ⁻¹' L n ∩ s = (f ⁻¹' ⋃ n, L n) ∩ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
⊢ IsTopologicalBasis ((fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
L : ℕ → Set Y
hcomp : ∀ (n : ℕ), IsCompact (L n)
hcov : ⋃ n, L n = f '' s
⊢ (f ⁻¹' ⋃ n, L n) ∩ s = f ⁻¹' f '' s ∩ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
⊢ SecondCountableTopology (α ⊕ β)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hf : IsInducing f
⊢ IsSigmaCompact s ↔ IsSigmaCompact (f '' s)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ SigmaCompactSpace X ↔ ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = univ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsSigmaCompact s ↔ IsSigmaCompact univ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology X
⊢ SigmaCompactSpace X

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
⊢ ⋃ n, compactCovering X n = univ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
inst✝¹ : SigmaCompactSpace X
inst✝ : SigmaCompactSpace Y
⊢ ⋃ n, (fun n ↦ compactCovering X n ×ˢ compactCovering Y n) n = univ

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f

Tactic:
by

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ SigmaCompactSpace ((i : ι) → X i)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
inst✝¹ : SigmaCompactSpace X
inst✝ : SigmaCompactSpace Y
⊢ ⋃ n, (fun n ↦ Sum.inl '' compactCovering X n ∪ Sum.inr '' compactCovering Y n) n = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
⊢ IsTopologicalBasis (image π '' V)

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
⊢ p s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
hf : IsInducing f
⊢ SecondCountableTopology α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
hf : IsEmbedding f
⊢ SeparableSpace α

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 : IsClosed[inst✝] t
⊢ IsCompact (s ∩ t)

Tactic:
by

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : SigmaCompactSpace X
e : Y → X
he : IsClosedEmbedding e
⊢ ⋃ n, (fun n ↦ e ⁻¹' compactCovering X n) n = univ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : ι → Set X
hf : LocallyFinite f
hne : ∀ (i : ι), (f i).Nonempty
⊢ univ.Countable

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst✝¹] s
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x

Tactic:
simp only [nhdsWithin, mem_inf_principal] at hf
  choose t ht hsub using fun n =>
    ((isCompact_compactCovering X n).inter_right hs).elim_nhds_subcover _ fun x hx => hf x hx.right
  refine
    ⟨⋃ n, (t n : Set X), iUnion_subset fun n x hx => (ht n x hx).2,
      countable_iUnion fun n => (t n).countable_toSet, fun x hx => mem_iUnion₂.2 ?_⟩
  rcases exists_mem_compactCovering x with ⟨n, hn⟩
  rcases mem_iUnion₂.1 (hsub n ⟨hn, hx⟩) with ⟨y, hyt : y ∈ t n, hyf : x ∈ s → x ∈ f y⟩
  exact ⟨y, mem_iUnion.2 ⟨n, hyt⟩, hyf hx⟩

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
s : Set X
hs : IsClosed[inst✝¹] s
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f 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
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this✝ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝 x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ∃ n, K n ∈ 𝓝 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
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
⊢ IsCompact (f '' s)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ ∃ n, s ⊆ K n

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ x ∈ K (K.find x)

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
n : ℕ
⊢ x ∈ K n ↔ K.find x ≤ n

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ K.shiftr.find x = K.find x + 1

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ¬K.shiftr.find x ≤ K.find x

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 ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x

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 ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
by

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
K : CompactExhaustion X✝
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : WeaklyLocallyCompactSpace X
inst✝ : SigmaCompactSpace X
⊢ CompactExhaustion X

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
⊢ l ≤ 𝓝ˢ s'

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝 y

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝 y)

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ t, ⋃ x ∈ t, U ↑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
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset ↑s
ht : ⋃ x ∈ t, U ↑x ∈ 𝓝ˢ s
⊢ ⋃ x ∈ Finset.image Subtype.val t, U 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
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U 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
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
⊢ ∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
by

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

Goal state before:
pp: α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = f <$> s <*> t

Tactic:
by

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

Goal state before:
pp: α β : Type u
s : Set α
f : α → Set β
α✝ β✝ : Type u_1
x✝¹ : Set α✝
x✝ : Set β✝
⊢ x✝¹ <* x✝ = const β✝ <$> x✝¹ <*> x✝

Tactic:
by

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

Goal state before:
pp: α β : Type u
s✝ : Set α
f : α → Set β
α✝ β✝ : Type u_1
s : Set α✝
t : Set β✝
⊢ s *> t = const α✝ id <$> s <*> t

Tactic:
by

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

Goal state before:
pp: α β : Type u
s : Set α
f : α → Set β
α✝ β✝ γ✝ : Type u_1
x✝² : Set α✝
x✝¹ : α✝ → Set β✝
x✝ : β✝ → Set γ✝
⊢ x✝² >>= x✝¹ >>= x✝ = x✝² >>= fun x ↦ x✝¹ x >>= x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
⊢ (do
      let a ← γ
      pure ↑a) ⊆
    β

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
a : α
ha :
  a ∈ do
    let a ← γ
    pure ↑a
⊢ ⟨a, ⋯⟩ ∈ γ

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
t : Set ↑s
⊢ Lean.Internal.coeM t = Subtype.val '' t

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝¹] (t i)
hst : s ∩ ⋂ i, t i = ∅
hdt : Directed (fun x1 x2 ↦ x1 ⊇ x2) t
⊢ s ⊆ ⋃ i, (compl ∘ t) i

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
a : α
ha : a ∈ Subtype.val '' γ
⊢ ⟨a, ⋯⟩ ∈ γ

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsCompact s
t✝ : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝¹] (t✝ i)
hst : s ∩ ⋂ i, t✝ i = ∅
hdt : Directed (fun x1 x2 ↦ x1 ⊇ x2) t✝
t : ι
ht : s ⊆ (compl ∘ t✝) t
⊢ s ∩ t✝ t = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Set α
γ : Set ↑β
δ : Type u_1
f : α → δ
⊢ f '' Subtype.val '' γ = β.domRestrict f '' γ

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ s ∩ ⋂ i, ⋂ i_1 ∈ i, t i_1 = ∅

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : ∀ (u : Finset ι), (s ∩ ⋂ i ∈ u, t i).Nonempty
⊢ (s ∩ ⋂ i, t i).Nonempty

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst✝] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
a : Finset ↑t
⊢ Subtype.val '' ↑a ⊆ t

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
t : Set (Set X)
ht : ∀ a ∈ t, IsClosed[inst✝] a
h : ∀ a ⊆ t, a.Finite → (s ∩ ⋂₀ a).Nonempty
⊢ (s ∩ ⋂₀ t).Nonempty

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
s : Set (Set X)
hsc : ∀ t ∈ s, IsClosed[inst✝¹] t
hs : ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
⊢ ∀ a ⊆ s, a.Finite → (univ ∩ ⋂₀ a).Nonempty

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
s : Set (Set X)
hsc : ∀ t ∈ s, IsClosed[inst✝¹] t
hs : ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
⊢ (⋂₀ s).Nonempty

Tactic:
by

Goal state after: