mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simpa using

Goal state after:
ι : Type u_1
ι' : Type u_2
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
e : ι' ≃ ι
h : LocallyFinite (f ∘ ⇑e)
⊢ LocallyFinite f
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:
simpa using

Goal state after:
X : Type u_1
ι : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : ι → Set X
hf : LocallyFinite f
⊢ {i | (f i).Nonempty}.Finite
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:
simpa using

Goal state after:
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, p t
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:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint l (𝓝ˢ s) ↔ ∀ x ∈ s, Disjoint l (𝓝 x)
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
⊢ (s ∩ ⋂ i ∈ a, ↑i).Nonempty

Tactic:
simpa using

Goal state after:
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
⊢ (s ∩ ⋂ i, ⋂ (x : i ∈ t), ⋂ (_ : ⟨i, ⋯⟩ ∈ a), i).Nonempty
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:
simpa using

Goal state after:
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, ∀ b ∈ s, a ∈ b
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:
simpa using

Goal state after:
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 → ∃ a_3, ∀ b ∈ a, a_3 ∈ b
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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
⊢ ∀ i ∈ K, s ∈ l ×ˢ 𝓝 i
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:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ x ∈ K, s ∈ 𝓝 x ⊓ l
⊢ ∀ i ∈ K, s ∈ 𝓝 i ⊓ l
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:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
K : Set X
l : Filter X
s : Set X
hK : IsCompact K
hs : ∀ y ∈ K, s ∈ l ⊓ 𝓝 y
⊢ ∀ i ∈ K, s ∈ l ⊓ 𝓝 i
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:
simpa using

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
x✝ : Filter X
hf : x✝.NeBot
hfa : x✝ ≤ 𝓟 {x}
⊢ pure x ≤ 𝓝 x
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
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
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:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
s t : Set α
hs : IsLowerSet s
⊢ Disjoint s ↑(upperClosure t) ↔ Disjoint s t
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:
hasBasis_cocompact.disjoint_iff_right,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ (∃ i, IsCompact i ∧ iᶜᶜ ∈ f) ↔ ∃ K ∈ f, IsCompact K
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:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : NoMinOrder α
s : Set α
h₁ : upperClosure s = ⊥
h₂ : BddBelow s
⊢ False
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:
simpa using

Goal state after:
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)
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:
simpa using

Goal state after:
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})
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:
simpa using

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
f : Filter X
inst✝ : f.NeBot
⊢ ∃ x, ClusterPt x f
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:
simpa using

Goal state after:
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)) → ⋂ i, t i = ∅ → ∃ u, ⋂ i ∈ u, t i = ∅
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:
simpa using

Goal state after:
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
⊢ ∃ x, ∀ (i : ι), x ∈ t i
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:
simpa using

Goal state after:
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 ι), ∃ x, ∀ i ∈ u, x ∈ t i
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:
simpa using

Goal state after:
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 → ∃ a, ∀ b ∈ Q, a ∈ b
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:
simpa using

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : CompactSpace X
hs : s.Infinite
⊢ ∃ x, AccPt x (cofinite ⊓ 𝓟 s)
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:
simpa using

Goal state after:
X : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompactSpace X
inst✝ : Infinite X
⊢ ∃ z, (𝓝[≠] z).NeBot
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
t : Set X
ht : IsCompact t
⊢ f ⁻¹' (f '' t)ᶜ ⊆ tᶜ

Tactic:
simpa using

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
t : Set X
ht : IsCompact t
⊢ t ⊆ f ⁻¹' f '' t
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:
simpa using

Goal state after:
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, ∀ x ∈ s, ∃ x_1, (∃ (x : x_1 ∈ I), ⟨x_1, ⋯⟩ ∈ u) ∧ x ∉ t x_1
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:
simpa using

Goal state after:
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)
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 = ∅
⊢ univ ∩ ⋂ i, (fun i ↦ s ↓∩ t ↑i) i = ∅

Tactic:
simpa using

Goal state after:
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 = ∅
⊢ ∀ a ∈ s, ∃ x ∈ I, a ∉ t x
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: α : Type u_4
inst✝ : TopologicalSpace α
⊢ Nontrivial (SeparationQuotient α) ↔ NontrivialTopology α

Tactic:
simpa using

Goal state after:
α : Type u_4
inst✝ : TopologicalSpace α
⊢ Nontrivial (SeparationQuotient α) ↔ NontrivialTopology α
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
hs : IsOpen[inst✝] s
hs' : IsOpen[inst✝] s'
ht : s ∩ frontier t = s' ∩ frontier t
x : α
hx : x ∈ frontier t
⊢ x ∈ s ↔ x ∈ s'

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
hs : IsOpen[inst✝] s
hs' : IsOpen[inst✝] s'
ht : s ∩ frontier t = s' ∩ frontier t
x : α
hx : x ∈ frontier t
⊢ x ∈ s ↔ x ∈ s'
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
E : Set X
h : ∀ x ∈ E, ¬AccPt x (𝓟 E)
⊢ DiscreteTopology ↑E

Tactic:
simpa using

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
E : Set X
h : ∀ x ∈ E, ¬AccPt x (𝓟 E)
⊢ ∀ x ∈ E, 𝓝[≠] x ⊓ 𝓟 E = ⊥
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : PreirreducibleSpace X
⊢ IsOpen[inst✝¹] s → IsOpen[inst✝¹] t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
s t : Set X
inst✝ : PreirreducibleSpace X
⊢ IsOpen[inst✝¹] s → IsOpen[inst✝¹] t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : IsOpenMap f
⊢ IsDiscrete (range f)

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : IsOpenMap f
⊢ IsDiscrete (range f)
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : DiscreteTopology X
hf : IsInducing f
⊢ IsDiscrete (range f)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : R0Space X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
a b : Y
⊢ a ⤳ b → b ⤳ a

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : R0Space X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
a b : Y
⊢ f a ⤳ f b → f b ⤳ f a
Module: Mathlib.Topology.Irreducible

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

Tactic:
by
  rintro u v hu hv ⟨_, ⟨⟨x, hx, rfl⟩, hxu⟩⟩ ⟨_, ⟨⟨y, hy, rfl⟩, hyv⟩⟩
  rw [← mem_preimage] at hxu hyv
  rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
  rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩
  have := H u' v' hu' hv'
  rw [inter_comm s u', ← u'_eq] at this
  rw [inter_comm s v', ← v'_eq] at this
  rcases this ⟨x, hxu, hx⟩ ⟨y, hyv, hy⟩ with ⟨x, hxs, hxu', hxv'⟩
  refine ⟨f x, mem_image_of_mem f hxs, ?_, ?_⟩
  all_goals
    rw [← mem_preimage]
    apply mem_of_mem_inter_left
    show x ∈ _ ∩ s
    simp [*]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
inst✝ : IndiscreteTopology X
u v : Set X
⊢ IsOpen[inst✝²] u → IsOpen[inst✝²] v → (univ ∩ u).Nonempty → (univ ∩ v).Nonempty → (univ ∩ (u ∩ v)).Nonempty

Tactic:
simp only [IndiscreteTopology.isOpen_iff, univ_inter]
    rintro ⟨h | h⟩ <;> simp_all

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
⊢ (u.Nonempty → uᶜ.Finite) → (v.Nonempty → vᶜ.Finite) → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty

Tactic:
intro hu

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
hu : u.Nonempty → uᶜ.Finite
⊢ (v.Nonempty → vᶜ.Finite) → u.Nonempty → v.Nonempty → (u ∩ v).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
hu : u.Nonempty → uᶜ.Finite
hv : v.Nonempty → vᶜ.Finite
hu' : u.Nonempty
hv' : v.Nonempty
⊢ (u ∩ v).Nonempty

Tactic:
simpa using

Goal state after:
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
inst✝¹ : TopologicalSpace Y
s t : Set X✝
X : Type u_3
inst✝ : Infinite X
u v : Set (CofiniteTopology X)
hu : u.Nonempty → uᶜ.Finite
hv : v.Nonempty → vᶜ.Finite
hu' : u.Nonempty
hv' : v.Nonempty
⊢ (u ∩ v).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hxU : closure[inst✝¹] {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
y : X
hy : y ⤳ x
⊢ y ∈ ⋃ i_1 ∈ {i}, U i_1

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x : X
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hxU : closure[inst✝¹] {x} ⊆ ⋃ i, U i
i : ι✝
hi : x ∈ U i
y : X
hy : y ⤳ x
⊢ y ∈ U i
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_1.empty
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
hu : ∀ u ∈ ∅, IsOpen[inst✝] u
hU : ∀ u ∈ ∅, (s ∩ u).Nonempty
⊢ (s ∩ ⋂₀ ↑∅).Nonempty

Tactic:
simpa using

Goal state after:
case refine_1.empty
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsIrreducible s
hu : ∀ u ∈ ∅, IsOpen[inst✝] u
hU : ∀ u ∈ ∅, (s ∩ u).Nonempty
⊢ s.Nonempty
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
a b : X
hab : a ⤳ b
ha : a ∈ s
hb : b ∈ s
this : DiscreteTopology ↑s := hs.to_subtype
⊢ a = b

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
a b : X
hab : a ⤳ b
ha : a ∈ s
hb : b ∈ s
this : DiscreteTopology ↑s := hs.to_subtype
⊢ a = b
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
⊢ s.Nonempty

Tactic:
simpa using

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
⊢ s.Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hu' : (s ∩ u).Nonempty
hv' : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
simpa using

Goal state after:
case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hu' : (s ∩ u).Nonempty
hv' : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
b : Set (Set X)
hb : IsTopologicalBasis b
x y : X
h : x ≠ y
⊢ ∃ a ∈ b, x ∈ a ∧ y ∉ a

Tactic:
by
  rcases hb.isOpen_iff.1 isOpen_ne x h with ⟨a, ab, xa, ha⟩
  exact ⟨a, ab, xa, fun h => ha h rfl⟩

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
hx : x ∉ S
⊢ Disjoint (𝓝 x) (𝓟 S)

Tactic:
simpa using

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
hx : x ∉ S
⊢ 𝓝 x ⊓ 𝓟 S = ⊥
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
x y : X
h : x ≠ y
⊢ ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : T2Space X
x y : X
h : x ≠ y
⊢ ∃ u v, IsCompact u ∧ IsCompact v ∧ Disjoint u v ∧ u ∈ 𝓝 x ∧ v ∈ 𝓝 y
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ ∃ U V, IsOpen[inst✝¹] U ∧ IsOpen[inst✝¹] V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ ∃ U, IsOpen[inst✝¹] U ∧ ∃ x_1, IsOpen[inst✝¹] x_1 ∧ t ⊆ U ∧ x ∈ x_1 ∧ Disjoint U x_1
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ Disjoint (𝓝ˢ t) (𝓝 x)

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
x : X
t : Set X
H1 : IsCompact t
H2 : x ∉ t
⊢ Disjoint (𝓝ˢ t) (𝓝 x)