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

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) = ⨆ x ∈ s, 𝓝 x ×ˢ 𝓝ˢ t

Tactic:
ht.prod_nhdsSet_eq_biSup,

Goal state after:
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) = ⨆ x ∈ s, ⨆ y ∈ t, 𝓝 x ×ˢ 𝓝 y
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:
refine fun h => (nhds_basis_opens _).ge_iff.2 ?_

Goal state after:
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)
h : y ∈ closure[inst✝] {x}
⊢ ∀ (i' : Set X), y ∈ i' ∧ IsOpen[inst✝] i' → i' ∈ 𝓝 x
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:
← image_univ

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (f '' univ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case left
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
u : Set ((i : ι) × X i)
hu : IsCompact u
s : Finset ι
hs : u ⊆ ⋃ i ∈ s, Sigma.mk i '' Sigma.mk i ⁻¹' univ
i : ι
⊢ IsCompact (Sigma.mk i ⁻¹' u)

Tactic:
exact Topology.IsClosedEmbedding.sigmaMk.isCompact_preimage hu

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f g : α → β
p : α → Prop
inst✝ : (a : α) → Decidable (p a)
hp : ∀ a ∈ frontier {x | p x}, f a = g a
hf : ContinuousOn f (closure[inst✝²] {x | p x})
hg : ContinuousOn g (closure[inst✝²] {x | ¬p x})
⊢ Continuous[inst✝², inst✝¹] fun a ↦ if p a then f a else g a

Tactic:
rw [← continuousOn_univ]
  apply ContinuousOn.if <;> simpa

Goal state after:
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space X ↔ IsClosed[instTopologicalSpaceProd] (diagonal X)

Tactic:
by
  simp only [t2Space_iff_disjoint_nhds, ← isOpen_compl_iff, isOpen_iff_mem_nhds, Prod.forall,
    nhds_prod_eq, compl_diagonal_mem_prod, mem_compl_iff, mem_diagonal_iff, Pairwise]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst✝] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst✝] V
hVy : V ∩ s = {y}
⊢ x ∈ s ∩ U

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst✝] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst✝] V
hVy : V ∩ s = {y}
⊢ y ∈ s ∩ V

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst✝] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst✝] V
hVy : V ∩ s = {y}
z : X
hz : z ∈ s ∩ (U ∩ V)
⊢ z ∈ U ∩ s

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
hs' : IsPreirreducible s
x : X
hxs : x ∈ s
y : X
hys : y ∈ s
U : Set X
hU : IsOpen[inst✝] U
hUx : U ∩ s = {x}
V : Set X
hV : IsOpen[inst✝] V
hVy : V ∩ s = {y}
z : X
hz : z ∈ s ∩ (U ∩ V)
⊢ z ∈ V ∩ s

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
H1 : IsClosed[inst✝¹] s
H2 : IsCompact (closure[inst✝¹] sᶜ)
H3 : IsClosed[inst✝¹] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s ∩ closure[inst✝¹] sᶜ) t

Tactic:
refine .of_isCompact_isCompact_isClosed ?_ ht H3 (disjoint_of_subset_left inter_subset_left H4)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
H1 : IsClosed[inst✝¹] s
H2 : IsCompact (closure[inst✝¹] sᶜ)
H3 : IsClosed[inst✝¹] t
H4 : Disjoint s t
ht : IsCompact t
⊢ IsCompact (s ∩ closure[inst✝¹] sᶜ)
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
s : Set X
x✝ : IsClosed[inst✝²] s
h2s : s.Nonempty
⊢ IsClosed[inst✝¹] {y}

Tactic:
isClosed_singleton

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case empty
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ ∅ᶜ ∈ codiscreteWithin s

pp: case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ ∀ {a : X} {s_1 : Set X}, a ∉ s_1 → s_1.Finite → s_1ᶜ ∈ codiscreteWithin s → (insert a s_1)ᶜ ∈ codiscreteWithin s

Tactic:
· simp

Goal state after:
case insert
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ ∀ {a : X} {s_1 : Set X}, a ∉ s_1 → s_1.Finite → s_1ᶜ ∈ codiscreteWithin s → (insert a s_1)ᶜ ∈ codiscreteWithin s
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
t : Set X
h₁t : t ∈ 𝓝[s] p
h₂t : t.Finite
S : Set X := {y | y ∈ t ∩ s ∧ ¬y ⤳ p}
hS_nhds : ∀ y ∈ S, (closure[inst✝] {y})ᶜ ∈ 𝓝 p
⊢ S ⊆ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClopen s ↔ frontier s = ∅

Tactic:
by
  rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, sdiff_eq_empty]
  refine ⟨fun h => (h.1.trans h.2.symm).subset, fun h => ?_⟩
  exact ⟨(h.trans interior_subset).antisymm subset_closure,
    interior_subset.antisymm (subset_closure.trans h)⟩

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
cases hs xs with
  | inl xu =>
    rcases H y ys with ⟨t, ts, xt, yt, ht⟩
    have := ht u v hu hv (ts.trans hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩
    exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩
  | inr xv =>
    rcases H z zs with ⟨t, ts, xt, zt, ht⟩
    have := ht v u hv hu (ts.trans <| by rwa [union_comm]) ⟨x, xt, xv⟩ ⟨z, zt, zu⟩
    exact this.imp fun _ h => ⟨ts h.1, h.2.2, h.2.1⟩

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝¹ x✝ : β
⊢ ∀ i ∈ Ico x✝ x✝¹, (s (succ i) ∩ s i).Nonempty

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder β
inst✝² : SuccOrder β
inst✝¹ : IsSuccArchimedean β
inst✝ : Nonempty β
s : β → Set α
H : ∀ (n : β), IsConnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝¹ x✝ : β
⊢ ∀ i ∈ Ico x✝ x✝¹, (s (succ i) ∩ s i).Nonempty

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mpr.superset
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s s✝ t✝ : Set α
a✝ : CountableGenerateSets g s✝
st : s✝ ⊆ t✝
ih : s✝ ∈ f
⊢ t✝ ∈ f

Tactic:
exact mem_of_superset ih st

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen[inst✝] u
huv : Disjoint (frontier u) v
⊢ v ∩ u ∪ v ∩ frontier u = v ∩ u

Tactic:
inter_comm _ (frontier u),

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
u v : Set X
hu : IsOpen[inst✝] u
huv : Disjoint (frontier u) v
⊢ v ∩ u ∪ frontier u ∩ v = v ∩ u
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inl
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsOpen[inst✝¹] (s i \ s i)

pp: case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsOpen[inst✝¹] (s j \ s i)

Tactic:
· simp

Goal state after:
case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_open : ∀ (i : ι), IsOpen[inst✝¹] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsOpen[inst✝¹] (s j \ s i)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inl
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i : ι
⊢ IsClosed[inst✝²] (s i \ s i)

pp: case inr
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsClosed[inst✝²] (s j \ s i)

Tactic:
· simp

Goal state after:
case inr
α : Type u
ι : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
inst✝ : Finite ι
h_closed : ∀ (i : ι), IsClosed[inst✝²] (s i)
h_Union : ⋃ i, s i = univ
i j : ι
h_ne : i ≠ j
⊢ IsClosed[inst✝²] (s j \ s i)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
B : IsOpen[inst✝¹] u
C : u.Nonempty
D : u = univ
⊢ P x y

Tactic:
change y ∈ u

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
P : α → α → Prop
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y ∧ P y x
h' : IsTrans α P
x y : α
u : Set α := {z | P x z}
A : IsClosed[inst✝¹] u
B : IsOpen[inst✝¹] u
C : u.Nonempty
D : u = univ
⊢ y ∈ u
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
s : Set α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
⊢ Disjoint (Ioi b) (Iio b)

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
s : Set α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
⊢ f '' s ⊆ Ioi b ∪ Iio b

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
s : Set α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
hfx : ∃ x ∈ s, b < f x
x : α
hx : x ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), f x ∉ Iio b

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
s : Set α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
b : β
hs : IsPreconnected s
hf : ContinuousOn f s
hfb : ∀ x ∈ s, f x ≠ b
hfx : ∃ x ∈ s, f x < b
x : α
hx : x ∈ s
⊢ ∃ x, ∃ (_ : x ∈ s), f x ∉ Ioi b

Tactic:
by grind

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
c_nonempty : c.Nonempty
f : ℕ → ↑c
f_surj : Function.Surjective f
x : ι
hx : x ∈ c
n : ℕ
hn : f n = ⟨x, hx⟩
⊢ U x = U ↑(f n)

Tactic:
by rw [hn]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ s ⊆ ⋃ i, (t i)ᶜ

Tactic:
← compl_iInter

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
⊢ s ⊆ (⋂ i, t i)ᶜ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
⊢ ∀ ⦃s t : Set X⦄,
    s ⊆ t →
      (∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ s) → ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X → Y
hf : IsClosedEmbedding f
s t : Set X
hs : IsClosed[inst✝²] s
ht : IsClosed[inst✝²] t
hst : Disjoint s t
H : SeparatedNhds (f '' s) (f '' t)
⊢ SeparatedNhds s t

Tactic:
exact (H.preimage hf.continuous).mono (subset_preimage_image _ _) (subset_preimage_image _ _)

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
hs : IsClopen (a ∪ b)
H : IsPreconnected (a ∪ b)
⊢ (a ∪ b) ∩ (a ∩ b) = ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s ∩ a ∩ b = ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s ⊆ b ∪ a

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s ∩ b ∩ a = ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsClopen s
H : ∀ (a b : Set α), IsClopen a → IsClopen b → a.Nonempty → b.Nonempty → Disjoint a b → s ≠ a ∪ b
a b : Set α
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hsab : s ⊆ a ∪ b
hsa : (s ∩ a).Nonempty
hsb : (s ∩ b).Nonempty
h : s ∩ (a ∩ b) = ∅
⊢ s = s ∩ a ∪ s ∩ b

Tactic:
by grind

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsLindelof (range f)

Tactic:
← image_univ

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsLindelof (f '' univ)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst✝²] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
⊢ φ x ∈ V'

Tactic:
have hV₂x : V₂ ∈ 𝓝 x := IsOpen.mem_nhds V₂_op x_in₂

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen[inst✝²] V₂
hV₂ : ∀ x ∈ i ⁻¹' V₂, f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ φ x ∈ V'
Module: Mathlib.Topology.Connected.TotallyDisconnected

Goal state before:
pp: case mp.a
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ connectedComponent x ⊆ univ

pp: case mp.a
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ IsPreconnected (connectedComponent x)

Tactic:
· exact subset_univ _

Goal state after:
case mp.a
α : Type u
inst✝ : TopologicalSpace α
h : TotallyDisconnectedSpace α
x : α
⊢ IsPreconnected (connectedComponent x)
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Finite X
f : ℕ → Set X
x✝¹ : ∀ (n : ℕ), IsOpen[inst✝¹] (f n)
x✝ : ∀ (n : ℕ), Dense (f n)
⊢ ∀ t ∈ range f, IsOpen[inst✝¹] t

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Finite X
f : ℕ → Set X
x✝¹ : ∀ (n : ℕ), IsOpen[inst✝¹] (f n)
x✝ : ∀ (n : ℕ), Dense (f n)
⊢ ∀ t ∈ range f, Dense t

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
have H2 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hv hu huv.symm

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ univ ⊆ interior (closure[inst✝²] s) ∪ (interior (closure[inst✝²] s))ᶜ

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := range p
c : ℕ → Set X := fun n ↦ p '' f n ∪ (closure[inst✝²] s)ᶜ
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
c_dense : ∀ (n : ℕ), Dense (c n)
c_inter_dense : Dense (⋂ n, c n)
x : Y
h : ∀ (i : ℕ), x ∈ f i
i : ℕ
⊢ p x ∈ p '' f i ∨ p x ∉ closure[inst✝²] s

Tactic:
by grind

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst✝¹] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ Dense (⋂ s ∈ S, f s)

Tactic:
by
  rw [← sInter_image]
  refine dense_sInter_of_isOpen ?_ (hS.image _) ?_ <;> rwa [forall_mem_image]

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i j : ι
x : ↑(U i)
y : ↑(U j)
hxy : mk ↑x = mk ↑y
⊢ ⟨i, mk x⟩ = ⟨j, mk y⟩

Tactic:
ConnectedComponents.coe_eq_coe

Goal state after:
case refine_1
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i j : ι
x : ↑(U i)
y : ↑(U j)
hxy : connectedComponent ↑x = connectedComponent ↑y
⊢ ⟨i, mk x⟩ = ⟨j, mk y⟩