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

Goal state before:
pp: case insert
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
hsub : S ⊆ univ.pi s
hconn : IsPreconnected S
hSu : (S ∩ u).Nonempty
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty

Tactic:
have hSv : (S ∩ v).Nonempty := ⟨_, ⟨_, this _ trivial, update_eq_self _ _⟩, h⟩

Goal state after:
case insert
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → X i)
uo : IsOpen[Pi.topologicalSpace] u
vo : IsOpen[Pi.topologicalSpace] v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → X i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → X i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → X a) := update (I.piecewise f g) i '' s i
hsub : S ⊆ univ.pi s
hconn : IsPreconnected S
hSu : (S ∩ u).Nonempty
hSv : (S ∩ v).Nonempty
⊢ (univ.pi s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case pos
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
h✝ : x ∈ F
⊢ Subtype.val '' connectedComponent ⟨x, h✝⟩ ⊆ F

Tactic:
simp

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

Goal state before:
pp: case neg
α : Type u
inst✝ : TopologicalSpace α
F : Set α
x : α
h✝ : x ∉ F
⊢ ∅ ⊆ F

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝³ : TopologicalSpace X
inst✝² : LindelofSpace X
f : Filter X
inst✝¹ : f.NeBot
inst✝ : CountableInterFilter f
⊢ f ≤ 𝓟 univ

Tactic:
simp

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (C i)
t : Set ι
| (⋂ i ∈ t, C i)ᶜ = (⋂ i, C i)ᶜ

Tactic:
simp

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : HereditarilyLindelofSpace X
ι : Type u_2
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (C i)
t : Set ι
| ⋃ i ∈ t, (C i)ᶜ = ⋃ i, (C i)ᶜ
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
k : ℕ → ι
| (⋂ n, C (k n))ᶜ = (⋂ i, C i)ᶜ

Tactic:
simp

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
C : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝²] (C i)
k : ℕ → ι
| ⋃ i, (C (k i))ᶜ = ⋃ i, (C i)ᶜ
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hT : ∀ t ∈ ∅, IsOpen[inst✝] t
T_count : ∅.Countable
⊢ ⋂₀ ∅ = ⋂ n, (fun _n ↦ univ) n

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hf : IsEmbedding f
hs : IsTotallyDisconnected s
u : Set β
hus : u ⊆ f '' s
hu : IsPreconnected u
⊢ f '' (f ⁻¹' u ∩ s) = u

Tactic:
rwa [image_preimage_inter, inter_eq_left]

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

Goal state before:
pp: case empty
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
h : ∀ s ∈ ∅, IsGδ s
⊢ IsGδ (⋃₀ ∅)

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ {s}.Countable

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : IsNowhereDense s
⊢ s ⊆ ⋃₀ {s}

Tactic:
simp

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)
n : ℕ
⊢ closure[inst✝²] (p '' f n) ⊆ closure[inst✝²] (p '' f n)

Tactic:
simp

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)
n : ℕ
⊢ (interior (closure[inst✝²] s))ᶜ ⊆ closure[inst✝²] (closure[inst✝²] s)ᶜ

Tactic:
simp

Goal state after:
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 : Disjoint (connectedComponent a) (connectedComponent b)
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v

Tactic:
rw [connectedComponent_eq_iInter_isClopen b, disjoint_iff_inter_eq_empty] at h

Goal state after:
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 = ∅
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ mk a ∈ u ∧ mk b ∈ v ∧ Disjoint u v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
i : ι
x : α
hx : x ∈ U i
⊢ (equivOfIsClopen hclopen hdisj hunion).symm ((equivOfIsClopen hclopen hdisj hunion) (mk x)) =
    (equivOfIsClopen hclopen hdisj hunion).symm ⟨i, mk ⟨x, hx⟩⟩

Tactic:
simp

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

Goal state before:
pp: case fst
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x : Fin (m + n) → X
i : Fin m
⊢ ((Fin.appendEquiv m n).symm x).1 i =
    ((sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).symm x).1 i

Tactic:
simp

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

Goal state before:
pp: case snd
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
x : Fin (m + n) → X
i : Fin n
⊢ ((Fin.appendEquiv m n).symm x).2 i =
    ((sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).symm x).2 i

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
f : X → Y
hf : IsEmbedding f
x : X
⊢ f x ∈ range f

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsEmbedding f
x : X
⊢ ↑(hf.toHomeomorph (hf.toHomeomorph.symm ⟨f x, ⋯⟩)) = ↑(hf.toHomeomorph x)

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
x : X
⊢ (hf.connectedComponentsHomeomorph hf') ((hf.connectedComponentsHomeomorph hf').symm (ConnectedComponents.mk (f x))) =
    (hf.connectedComponentsHomeomorph hf') (ConnectedComponents.mk x)

Tactic:
simp

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
fst✝ : α
snd✝ : γ
⊢ (fst✝, snd✝) ∈ s ○ t ↔ (fst✝, snd✝) ∈ ⋃ b, (fun p ↦ (p.1, b)) ⁻¹' s ∩ (fun p ↦ (b, p.2)) ⁻¹' t

Tactic:
simp

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 : α → β
s : Set α
p : Filter ι
⊢ ∀ a ∈ 𝓤 β, True

Tactic:
simp

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 : α → β
s : Set α
p : Filter ι
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u) ↔
    ∀ᶠ (n : ι) in p, ∀ (x : ↑s), ((f ∘ Subtype.val) x, (fun i x ↦ F i ↑x) n x) ∈ u

Tactic:
simp

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 ι
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ ∅, (f x, F n x) ∈ u

Tactic:
simp

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
x : α
⊢ 𝓝 x = Filter.comap (Prod.mk x) (Filter.comap (fun p ↦ (f p.1, f p.2)) (𝓤 β))

Tactic:
simp only [nhds_induced, nhds_eq_comap_uniformity, comap_comap, Function.comp_def]

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

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ 𝓝 a ≤ 𝓝 a

Tactic:
@nhds_eq_uniformity α u₁ a,

Goal state after:
α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ (𝓤 α).lift' (ball a) ≤ 𝓝 a
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
map_swap4_eq_comap,

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = Filter.comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ᶠ (x : ι × ι) in p ×ˢ p, (fun x ↦ True) x

Tactic:
simp

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 ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
h✝ : p.NeBot
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
⊢ ∀ {x : ι × ι},
    (fun x ↦ True) x →
      ∀ {y : α}, Tendsto (fun n ↦ F n y) p (𝓝 (f y)) → Tendsto (fun n ↦ F n (x, y).2) p (𝓝 (f (x, y).2))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology α
x : α × α
⊢ Inseparable x.1 x.2 ↔ x ∈ univ

Tactic:
simp

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

Goal state before:
pp: β : Type v
inst✝¹ : UniformSpace β
α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) ⊤

Tactic:
exact Filter.tendsto_top

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.22
β : Type ?u.25
γ : Type ?u.31
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p ↦ f p.1 p.2
⊢ Sort ?u.48

Tactic:
haveI := sInf uas; haveI := sInf ubs
      exact @UniformContinuous _ _ _ uc fun p : α × β => f p.1 p.2

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ IsUniformInducing f ↔ UniformSpace.comap f inst✝ = inst✝¹

Tactic:
rw [isUniformInducing_iff, UniformSpace.ext_iff, Filter.ext_iff]

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ (∀ (s : Set (α × α)), s ∈ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ↔ s ∈ 𝓤 α) ↔ ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ s ∈ 𝓤 α
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
p : Filter ι
p' p'' : Filter α
hf : UniformCauchySeqOnFilter F p p'
hp : p'' ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
this : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p'', (F x.1.1 x.2, F x.1.2 x.2) ∈ u
⊢ ∀ (x : (ι × ι) × α), (F x.1.1 x.2, F x.1.2 x.2) ∈ u → (F x.1.1 x.2, F x.1.2 x.2) ∈ u

Tactic:
simp

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
g : Filter α
d : SetRel α α
hd : d ∈ 𝓤 α
hd_cover : ∀ (t : Set α), t.Finite → d.preimage t ∉ g
f : Filter α := ⨅ t, g ⊓ 𝓟 (d.preimage ↑t)ᶜ
hb : Antitone fun t ↦ g ⊓ 𝓟 (d.preimage ↑t)ᶜ
this : f.NeBot
⊢ g ⊓ 𝓟 (d.preimage ↑∅)ᶜ ≤ g

Tactic:
simp

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:
hf

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
⊢ IsComplete (m '' s) ↔ IsComplete s

Tactic:
by
  have fact1 : SurjOn (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := surjOn_image .. |>.filter_map_Iic
  have fact2 : MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := mapsTo_image .. |>.filter_map_Iic
  simp_rw [IsComplete, imp.swap (a := Cauchy _), ← mem_Iic (b := 𝓟 _), fact1.forall fact2,
    hm.cauchy_map_iff, exists_mem_image, map_le_iff_le_comap, hm.isInducing.nhds_eq_comap]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
⊢ a ∈ s

Tactic:
let f := 𝓝[s] a

Goal state after:
α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
⊢ a ∈ s
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝² : One α
inst✝¹ : TopologicalSpace X
Y : Type u_9
inst✝ : TopologicalSpace Y
g : Y → α
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ mulTSupport (g ∘ f) ⊆ f ⁻¹' mulTSupport g

Tactic:
rw [mulTSupport, mulTSupport, mulSupport_comp_eq_preimage]
  exact hf.closure_preimage_subset _

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

Goal state before:
pp: case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ x, interior U
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U := by
        simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU

Goal state after:
case mp
α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ x, interior U
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ interior U
⊢ ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : MulOneClass α
f g : X → α
⊢ 1 * 1 = 1

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DivisionMonoid α
f g : X → α
⊢ 1 * 1⁻¹ = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
h : α ≃ᵤ β
⊢ range ⇑h = univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
hg : UniformContinuous g
hf : TendstoLocallyUniformly F f p
⊢ ∀ (x : α), f x ∈ univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
g : β → γ
hg : UniformContinuous g
hf : TendstoLocallyUniformly F f p
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ p ∈ univ, ∀ x ∈ ∅, (f p x, f q x) ∈ u

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous[inst✝¹.toTopologicalSpace, UniformFun.topologicalSpace ι α] (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformEquicontinuous F

Tactic:
uniformEquicontinuous_iff_uniformContinuous

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
ι : Type u_4
F : ι → β → α
inst✝ : CompactSpace β
h : Continuous[inst✝¹.toTopologicalSpace, UniformFun.topologicalSpace ι α] (⇑UniformFun.ofFun ∘ Function.swap F)
⊢ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
U : Set (α × α)
| 𝓤 β ⊓ 𝓟 (S ×ˢ S)

Tactic:
← Subtype.range_val (s := S),

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
F : ι → β → α
S : Set β
U : Set (α × α)
| 𝓤 β ⊓ 𝓟 (range Subtype.val ×ˢ range Subtype.val)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (𝓤 γ) = 𝓤 (α →ᵤ γ)

Tactic:
rw [iInf_uniformity, iInf_uniformity]

Goal state after:
α : Type u_1
γ : Type u_3
ι : Type u_4
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ i, 𝓤 γ) = ⨅ i, 𝓤 (α →ᵤ γ)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (⇑ofFun ∘ (fun x ↦ f ∘ x) ∘ ⇑toFun)

Tactic:
refine uniformContinuous_iff_le_comap.mpr ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ ≤ UniformSpace.comap (⇑ofFun ∘ (fun x ↦ f ∘ x) ∘ ⇑toFun) (uniformSpace α β)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map (fun x ↦ m x.swap.1 x.swap.2) (g ×ˢ f) = map (fun p ↦ m p.2 p.1) (g ×ˢ f)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : univ ∈ 𝔖
U : Set (β × β)
hU : U ∈ 𝓤 β
f : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
⊢ f ∈ UniformOnFun.gen 𝔖 univ U →
    (UniformFun.ofFun ((toFun 𝔖) f.1), UniformFun.ofFun ((toFun 𝔖) f.2)) ∈ UniformFun.gen α β U

Tactic:
hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : univ ∈ 𝔖
U : Set (β × β)
hU : U ∈ 𝓤 β
f : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
hf : f ∈ UniformOnFun.gen 𝔖 univ U
⊢ (UniformFun.ofFun ((toFun 𝔖) f.1), UniformFun.ofFun ((toFun 𝔖) f.2)) ∈ UniformFun.gen α β U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
⊢ UniformContinuous (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖))

Tactic:
simp only [UniformContinuous, UniformOnFun.uniformity_eq, iInf₂_comm (ι₂ := Set (β × β))]
  refine tendsto_iInf_iInf fun V ↦ tendsto_iInf_iInf fun hV ↦ ?_
  simp only [tendsto_iInf, tendsto_principal, Filter.Eventually, mem_biInf_principal]
  intro s hs
  obtain ⟨T, hT𝔗, hT, hsT⟩ := h s hs
  refine ⟨T, hT, hT𝔗, fun f hf ↦ ?_⟩
  simp only [UniformOnFun.gen, Set.mem_iInter, Set.mem_ofPred_eq] at hf ⊢
  intro x hx
  obtain ⟨t, ht, hxt⟩ := Set.mem_sUnion.mp <| hsT hx
  exact hf t ht x hxt

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : 𝔖 ⊆ 𝔗
s : Set α
x✝ : s ∈ 𝔖
⊢ {s}.Finite ∧ s ⊆ ⋃₀ {s}

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
f : α →ᵤ[𝔖] β
⊢ f ∈ V → ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) f x) ∈ id U

Tactic:
hf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
s : Set α
hs : s ∈ 𝔖
U : SetRel β β
hU : U ∈ 𝓤 β
hUc : IsClosed[instTopologicalSpaceProd] U
V : Set (α →ᵤ[𝔖] β)
hV : V ∈ F
hVU : V ×ˢ V ⊆ UniformOnFun.gen 𝔖 s U
f : α →ᵤ[𝔖] β
hf : f ∈ V
⊢ ∀ x ∈ s, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) f x) ∈ id U
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : One α
inst✝² : One β
inst✝¹ : FunLike F α β
inst✝ : OneHomClass F α β
φ : F
⊢ map (⇑φ) 1 = 1

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a b : α
⊢ pure a * pure b = pure (a * b)

Tactic:
simp

Goal state after: