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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
n : Type u_9
m : Type u_10
f : m → n
hf : Surjective f
⊢ IsEmbedding fun x ↦ x ∘ f

Tactic:
refine ⟨isInducing_iff_nhds.mpr fun x ↦ ?_, hf.injective_comp_right⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
n : Type u_9
m : Type u_10
f : m → n
hf : Surjective f
x : n → X
⊢ 𝓝 x = comap (fun x ↦ x ∘ f) (𝓝 (x ∘ f))
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology α
inst✝ : FirstCountableTopology β
x✝ : α × β
x : α
y : β
⊢ (𝓝 (x, y)).IsCountablyGenerated

Tactic:
rw [nhds_prod_eq]

Goal state after:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology α
inst✝ : FirstCountableTopology β
x✝ : α × β
x : α
y : β
⊢ (𝓝 x ×ˢ 𝓝 y).IsCountablyGenerated
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
⊢ IsOpen[inst✝¹] U ∧ K ⊆ U → ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U

Tactic:
⟨hU, h_KU⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝¹] U
h_KU : K ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a.h
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
i : Set α
⊢ i ∈ f u → IsOpen[generateFrom (⋃ u ∈ s', f u)] i

Tactic:
hi

Goal state after:
case a.h
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
i : Set α
hi : i ∈ f u
⊢ IsOpen[generateFrom (⋃ u ∈ s', f u)] i
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 y : X
hy : y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ
i : ι
⊢ i ∈ {i | y ∈ s i} → i ∈ {i | x ∈ s i}

Tactic:
hi

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x y : X
hy : y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ
i : ι
hi : i ∈ {i | y ∈ s i}
⊢ i ∈ {i | x ∈ s i}
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)
b : Set (Set ((i : ι) × E i)) := ⋃ i, (fun u ↦ Sigma.mk i '' u) '' countableBasis (E i)
A : IsTopologicalBasis b
B : b.Countable
⊢ SecondCountableTopology ((i : ι) × E i)

Tactic:
exact A.secondCountableTopology B

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_1
inst✝² : TopologicalSpace β
inst✝¹ : SecondCountableTopology α
inst✝ : SecondCountableTopology β
b : Set (Set (α ⊕ β)) := (fun u ↦ Sum.inl '' u) '' countableBasis α ∪ (fun u ↦ Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
B : b.Countable
⊢ SecondCountableTopology (α ⊕ β)

Tactic:
exact A.secondCountableTopology B

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 ∈ 𝓝[univ] x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = univ

Tactic:
rcases countable_cover_nhdsWithin_of_sigmaCompact isClosed_univ fun x _ => hf x with
    ⟨s, -, hsc, hsU⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
f : X → Set X
hf : ∀ (x : X), f x ∈ 𝓝[univ] x
s : Set X
hsc : s.Countable
hsU : univ ⊆ ⋃ x ∈ s, f x
⊢ ∃ s, s.Countable ∧ ⋃ x ∈ s, 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 Y
x : X
hf : Disjoint f (cocompact Y)
⊢ 𝓝 x ×ˢ f ≤ 𝓝ˢ ({x} ×ˢ univ)

Tactic:
by
  simpa using nhdsSet_prod_le_of_disjoint_cocompact isCompact_singleton hf

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 : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 (x, y)

Tactic:
rw [nhds_prod_eq]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 x ×ˢ 𝓝 y
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
r : X → X → Prop
inst✝ : CompactSpace X
⊢ IsCompact univ

Tactic:
← range_quot_mk

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
f : X → Y
r : X → X → Prop
inst✝ : CompactSpace X
⊢ IsCompact (range (mk r))
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 h ∅

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

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
⊢ (∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F) → ∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l

Tactic:
intro cond

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : Set X
cond : ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
⊢ ∀ x ∈ U, ∀ (l : Ultrafilter X), ↑l ≤ 𝓝 x → U ∈ l
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
l : Filter Y
inst✝ : l.NeBot
c d : X
⊢ Tendsto (fun x ↦ c) l (𝓝 d) ↔ c = d

Tactic:
Tendsto,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
l : Filter Y
inst✝ : l.NeBot
c d : X
⊢ map (fun x ↦ c) l ≤ 𝓝 d ↔ c = d
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : PredOrder α
a : α
⊢ 𝓝[>] a = 𝓝[≠] a

Tactic:
by
  rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]

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

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
i : ι
t : Set (X i)
ht : IsConnected t
⊢ IsConnected (mk i '' t)

Tactic:
exact ht.image _ continuous_sigmaMk.continuousOn

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

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
a : ι
t : Set (X a)
ht : IsPreconnected t
⊢ IsPreconnected (mk a '' t)

Tactic:
exact ht.image _ continuous_sigmaMk.continuousOn

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

Goal state before:
pp: case mp.sInter
α : Type u_2
g : Set (Set α)
s : Set α
S : Set (Set α)
Sct : S.Countable
a✝ : ∀ s ∈ S, CountableGenerateSets g s
ih : ∀ s ∈ S, ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ ∃ S_1 ⊆ g, S_1.Countable ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Tactic:
choose T Tg Tct hT using ih
      refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, ?_⟩
      apply subset_sInter
      intro s H
      exact subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

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 ∩ closure[inst✝] u = v ∩ u

Tactic:
rw [closure_eq_self_union_frontier, inter_union_distrib_left, inter_comm _ (frontier u),
    huv.inter_eq, union_empty]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y ∧ P y x
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ P x y

Tactic:
let Q : s → s → Prop := fun a b ↦ P a b
  change Q ⟨x, hx⟩ ⟨y, hy⟩
  have : PreconnectedSpace s := Subtype.preconnectedSpace hs
  apply PreconnectedSpace.induction₂'
  · rintro ⟨x, hx⟩
    have Z := h x hx
    rwa [nhdsWithin_eq_map_subtype_coe] at Z
  · exact ⟨fun ⟨a, ha⟩ ⟨b, hb⟩ ⟨c, hc⟩ ↦ h' a b c ha hb hc⟩

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

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s

Tactic:
intro u v hu hv hs hsu hsv

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hs : IsPreconnected s
hinj : Injective f
hf : IsOpenMap f
u v : Set α
hu : IsOpen[inst✝¹] u
hv : IsOpen[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
· simpa only [image_preimage_inter] using hsv.image f

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

Goal state before:
pp: case refine_3
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set β
hs : IsPreconnected s
f : α → β
hinj : Injective f
hf : IsClosedMap f
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
hsuv : f ⁻¹' s ⊆ u ∪ v
hsu : (f ⁻¹' s ∩ u).Nonempty
hsv : (f ⁻¹' s ∩ v).Nonempty
hsf : f '' f ⁻¹' s = s
⊢ (s ∩ f '' v).Nonempty

Tactic:
· simpa only [image_preimage_inter] using hsv.image f

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

Goal state before:
pp: case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
i : ↑s
⊢ i ∈ r → interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯

Tactic:
hi

Goal state after:
case right
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsLindelof s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
r : Set ↑s
hr : r.Countable
hs : s ⊆ ⋃ i ∈ r, interior (U ↑i ⋯)
i : ↑s
hi : i ∈ r
⊢ interior (U ↑i ⋯) ⊆ ⋃ x ∈ r, U ↑x ⋯
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty

Tactic:
intro u v hu hv hs hsu hsv

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty
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
U : Set X
⊢ IsOpen[inst✝²] U ∧ K ⊆ U → ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ U

Tactic:
⟨hU, h_KU⟩

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : LocallyCompactSpace X
inst✝ : RegularSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝²] U
h_KU : K ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, (IsCompact r ∧ IsClosed[inst✝²] r) ∧ r ⊆ U
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
⊢ i ∈ t → (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i

Tactic:
hi

Goal state after:
case mp.refine_1
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
Y : Type u
f' : Y → ι
h₁ : IsLindelof (⋃ i, (b ∘ f') i)
h₂ : IsOpen[inst✝] (⋃ i, (b ∘ f') i)
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Set Y
ht : t.Countable ∧ ⋃ i, (b ∘ f') i ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ i ∈ f' '' t, b i
Module: Mathlib.Topology.Compactness.Lindelof

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 : IsLindelof (K ∩ range f)
⊢ IsLindelof (f ⁻¹' K)

Tactic:
rwa [hf.isLindelof_iff, image_preimage_eq_inter_range]

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

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
r : X → X → Prop
inst✝ : LindelofSpace X
⊢ IsLindelof univ

Tactic:
← range_quot_mk

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s t : Set X
r : X → X → Prop
inst✝ : LindelofSpace X
⊢ IsLindelof (range (mk r))
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : connectedComponent a ≠ connectedComponent b
h : connectedComponent a ∩ ⋂ s, ↑s = ∅
V : Set (ConnectedComponents X)
hU : IsClopen V
ha : connectedComponent a ∩ mk ⁻¹' V = ∅
hb : connectedComponent b ⊆ mk ⁻¹' V
⊢ mk a ∈ Vᶜ

Tactic:
exact fun h => flip Set.Nonempty.ne_empty ha ⟨a, mem_connectedComponent, h⟩

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
⊢ (∃ t ⊆ s, IsGδ t ∧ Dense t) → s ∈ residual X

Tactic:
rintro ⟨t, ts, ho, hd⟩

Goal state after:
case mpr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
ts : t ⊆ s
ho : IsGδ t
hd : Dense t
⊢ s ∈ residual X
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)

Tactic:
rw [preimage_subtype_coe_eq_compl hsuv H]
      exact (v_op.preimage continuous_subtype_val).isClosed_compl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case right
α : Type ua
inst✝ : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : SetRel.symmetrize w ⊆ w
⊢ SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ s

Tactic:
calc SetRel.symmetrize w ○ SetRel.symmetrize w
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformlyOn F f p univ ↔ TendstoUniformly F f p

Tactic:
by
  simp [TendstoUniformlyOn, TendstoUniformly]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ (𝓝 (x, y)).HasBasis (fun s ↦ s ∈ 𝓤 α ∧ SetRel.IsSymm s) fun s ↦ ball x s ×ˢ ball y s

Tactic:
rw [nhds_prod_eq]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x y : α
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun s ↦ s ∈ 𝓤 α ∧ SetRel.IsSymm s) fun s ↦ ball x s ×ˢ ball y s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 (x, x)

Tactic:
rw [nhds_prod_eq]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : LinearOrder ι
B : ι → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
s t : Set α
hSt : Disjoint (closure[inst✝¹.toTopologicalSpace] s) t
hsT : Disjoint s (closure[inst✝¹.toTopologicalSpace] t)
S : Bool → Set α := fun b ↦ Bool.casesOn b s t
b : Bool
x : ↑(S b)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
i : ι
hi : B i ⊆ V
⊢ (B i).comp (B i).inv ⊆ U

Tactic:
exact subset_trans (SetRel.comp_subset_comp hi (V.inv_eq_self ▸ (SetRel.inv_mono hi))) hVU

Goal state after:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
f : ι → Filter α
this : Finite ↑I
⊢ (⨆ i ∈ I, f i).TotallyBounded ↔ ∀ i ∈ I, (f i).TotallyBounded

Tactic:
rw [iSup_subtype', totallyBounded_iSup, Subtype.forall]

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

Goal state before:
pp: α✝ : Type ua
β✝ : Type ub
γ✝ : Type uc
δ : Type ud
ι : Sort u_1
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β✝
inst✝ : UniformSpace γ✝
α : Type ?u.21
β : Type ?u.25
γ : Type ?u.29
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
⊢ Sort ?u.31

Tactic:
haveI := ua1 ⊓ ua2; haveI := ub1 ⊓ ub2
      exact UniformContinuous fun p : α × β => f p.1 p.2

Goal state after:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Ultrafilter α), ↑f ≤ g → Cauchy ↑f
⊢ ∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c

Tactic:
intro f hf hfs

Goal state after:
α : Type u
uniformSpace : UniformSpace α
g : Filter α
H : ∀ (f : Ultrafilter α), ↑f ≤ g → Cauchy ↑f
f : Filter α
hf : f.NeBot
hfs : f ≤ g
⊢ ∃ c ≤ f, Cauchy c
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : DiscreteUniformity β
f : α → β
hf : IsUniformEmbedding f
⊢ DiscreteUniformity α

Tactic:
by
  simp_rw [discreteUniformity_iff_eq_principal_setRelId, ← hf.comap_uniformity,
    DiscreteUniformity.eq_principal_setRelId, comap_principal, SetRel.id, preimage_ofPred_eq,
    hf.injective.eq_iff]

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)
ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)

Tactic:
have : b ∈ closure (e '' { x | p x }) :=
    (closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)
ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst✝².toTopologicalSpace] (e '' {x | p x})
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x • 0 x = 0 x

Tactic:
Pi.zero_apply,

Goal state after:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝² : TopologicalSpace α
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : α → R
f' : α → M
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x • 0 = 0
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ 0 x • f' x = 0 x

Tactic:
Pi.zero_apply,

Goal state after:
α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ 0 • f' x = 0
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
M : Type u_7
R : Type u_8
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
hf : HasCompactSupport f
⊢ HasCompactSupport (f • f')

Tactic:
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
  exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]

Goal state after:
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ 0 x * f' x = 0 x

Tactic:
Pi.zero_apply,

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ 0 * f' x = 0
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x * 0 x = 0 x

Tactic:
Pi.zero_apply,

Goal state after:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = 0 x
⊢ f x * 0 = 0