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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
⊢ (𝓟 s).TotallyBounded ↔ TotallyBounded s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
⊢ UniformSpace.comap id = id

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
uγ : UniformSpace γ
f : α → β
g : β → γ
⊢ comap (g ∘ f) uγ = comap f (comap g uγ)

Tactic:
by

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

Goal state before:
pp: ι : Sort u_2
α : Type u_3
γ : Type u_4
u : ι → UniformSpace γ
f : α → γ
⊢ comap f (⨅ i, u i) = ⨅ i, comap f (u i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace β
x : α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
⊢ UniformContinuousOn (↿f) (univ ×ˢ univ)

Tactic:
by

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

Goal state before:
pp: α : Type ua
u v : UniformSpace α
⊢ u ≤ v ↔ UniformContinuous id

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type ua
ι : Sort u_2
p : ι → Prop
s : ι → SetRel α α
u : UniformSpace α
h : (𝓤 α).HasBasis p s
⊢ u = ⊥ ↔ ∃ i, p i ∧ Pairwise fun x y ↦ (x, y) ∉ s i

Tactic:
by

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

Goal state before:
pp: α : Type ua
ι : Sort u_2
u : ι → UniformSpace α
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
by

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

Goal state before:
pp: α : Type ua
s : Set (UniformSpace α)
⊢ (sInf s).toTopologicalSpace = ⨅ i ∈ s, i.toTopologicalSpace

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s t : Set α
hf : UniformContinuousOn f s
ht : t ⊆ s
⊢ 𝓟 (t ×ˢ t) ≤ 𝓟 (s ×ˢ s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
l' : Filter α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOnFilter F f l l' ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
a b : α
ha : (a, b).1 ∈ s
hb : (a, b).2 ∈ s
⊢ (f (a, b).1, f (a, b).2) = (g (a, b).1, g (a, b).2)

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f g : α → β
s : Set α
hf : UniformContinuousOn f s
h : EqOn f g s
⊢ UniformContinuousOn g s

Tactic:
by

Goal state after:
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
U : (b : Bool) → ↑(S b) → ι
hU : ∀ (b : Bool) (x : ↑(S b)), Disjoint (ball (↑x) ((B (U b x)).comp (B (U b x)).inv)) (S !b)
hUS : ∀ (b : Bool), ⋃ x, ball (↑x) (B (U b x)) ∈ 𝓝ˢ (S b)
b : Bool
x : ↑(S b)
y : ↑(S !b)
hxy : U b x ≤ U (!b) y
⊢ Disjoint (ball (↑x) (B (U b x))) (ball (↑y) (B (U (!b) y)))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιX : Type u_6
ια : Type u_7
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
l' : Filter α
pX : ιX → Prop
sX : ιX → Set X
pα : ια → Prop
sα : ια → Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hl : l.HasBasis pX sX
hl' : l'.HasBasis pα sα
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOnFilter F f l l' ↔
    ∀ (i : ιβ), pβ i → ∃ j k, (pX j ∧ pα k) ∧ ∀ (x : X) (a : α), x ∈ sX j → a ∈ sα k → (f a, F x a) ∈ sβ i

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set α
g : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : UniformContinuousOn f s
hst : MapsTo f s t
⊢ UniformContinuousOn (g ∘ f) s

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ UniformContinuous f

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ UniformContinuous f ↔ ∀ u ∈ u₂, UniformContinuous f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ UniformContinuous f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιX : Type u_6
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pX : ιX → Prop
sX : ιX → Set X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hl : l.HasBasis pX sX
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∃ j, pX j ∧ ∀ ⦃x : X⦄, x ∈ sX j → ∀ a ∈ s, (f a, F x a) ∈ sβ i

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
⊢ UniformContinuous f ↔ ∀ (i : ι), UniformContinuous f

Tactic:
by

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

Goal state before:
pp: α : Type ua
s : Set α
inst✝ : UniformSpace α
⊢ map (Prod.map Subtype.val Subtype.val) (𝓤 ↑s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔ UniformContinuous (s.domRestrict f)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ (x : α), (f x, F n x) ∈ sβ i

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x ↦ f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (𝓝 a) (𝓝 (f a))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιX : Type u_6
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
pX : ιX → Prop
sX : ιX → Set X
hl : l.HasBasis pX sX
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformly F f l ↔ ∀ (i : ιβ), pβ i → ∃ j, pX j ∧ ∀ ⦃x : X⦄, x ∈ sX j → ∀ (a : α), (f a, F x a) ∈ sβ i

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : f.TotallyBounded
s : Set α
hs : s ∈ f
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ U.preimage t ∈ f

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuousOn f s
⊢ ContinuousOn f s

Tactic:
by

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
⊢ comap (fun p ↦ (MulOpposite.op p.1, MulOpposite.op p.2)) (𝓤 αᵐᵒᵖ) = 𝓤 α

Tactic:
by

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 β
⊢ instTopologicalSpaceProd = instUniformSpaceProd.toTopologicalSpace

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
⊢ UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (𝓟 s)

Tactic:
by

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✝² : (𝓤 α).IsCountablyGenerated
inst✝¹ : UniformSpace β
inst✝ : (𝓤 β).IsCountablyGenerated
⊢ (𝓤 (α × β)).IsCountablyGenerated

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
hF : UniformCauchySeqOn F p s
⊢ UniformCauchySeqOnFilter F p (𝓟 s)

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
by

Goal state after:
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)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (x, y) ≤ 𝓤 α

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
p : ι → Prop
U : ι → SetRel α α
H : (𝓤 α).HasBasis p U
f : Filter α
x✝³ x✝² : Set (α × α)
x✝¹ : x✝³ ⊆ x✝²
h : ∃ t, t.Finite ∧ SetRel.preimage x✝³ t ∈ f
x✝ : Set α
ht : x✝.Finite ∧ SetRel.preimage x✝³ x✝ ∈ f
⊢ SetRel.preimage x✝³ x✝ ⊆ SetRel.preimage x✝² x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
x y : α
⊢ Inseparable x y ↔ ClusterPt (x, y) (𝓤 α)

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
h : ∀ V ∈ 𝓤 α, SetRel.IsSymm V → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y V
V : SetRel α α
x✝ : V ∈ 𝓤 α ∧ V.IsSymm
left✝ : V ∈ 𝓤 α
right✝ : V.IsSymm
⊢ ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ id V}

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ ∀ (x y : α), (∀ r ∈ 𝓤 α, (x, y) ∈ r) → x = y

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ Pairwise fun x y ↦ ∃ r ∈ 𝓤 α, (x, y) ∉ r

Tactic:
by

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

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

Tactic:
by

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

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ (𝓤 α).ker = diagonal α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : UniformSpace α
inst✝ : T0Space α
x y : α
h : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SetRel.IsSymm V → (x, y) ∈ V
⊢ ∀ {i : SetRel α α}, i ∈ 𝓤 α ∧ i.IsSymm → (x, y) ∈ id i

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
⊢ Inseparable a b ↔ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
⊢ TotallyBounded {x | ClusterPt x f}

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
h : TotallyBounded s
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] s)

Tactic:
by

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 : TendstoUniformlyOnFilter F f p p'
⊢ UniformCauchySeqOnFilter F p p'

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : SetRel β β
f : α → α → β
hf : UniformContinuous fun p ↦ f p.1 p.2
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
this : x = y
⊢ x ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
t₁ : UniformSpace α
t₂ : UniformSpace β
u : SetRel α α
v : SetRel β β
hu : u ∈ 𝓤 α
hv : v ∈ 𝓤 β
⊢ entourageProd u v ∈ 𝓤 (α × β)

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
x : α × β
⊢ ball x (entourageProd u v) = ball x.1 u ×ˢ ball x.2 v

Tactic:
by

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 : ι × ι) in p ×ˢ p, (fun x ↦ True) x

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
x : α
hx : ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty
y : α
hy : y ∈ ball x V₁
hy' : y ∈ s
V : Set (α × α)
V_in : V ∈ 𝓤 α
a✝ : SetRel.IsSymm V
z : α
hz : z ∈ ball x (V₁ ∩ V)
hz' : z ∈ s
⊢ z = y

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
s : Set α
t : Set β
⊢ (entourageProd u v).image (s ×ˢ t) = u.image s ×ˢ v.image t

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
f : ι → Filter α
⊢ (⨆ i, f i).TotallyBounded ↔ ∀ (i : ι), (f i).TotallyBounded

Tactic:
by

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

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
⊢ IsClosed[inst✝¹.toTopologicalSpace] s

Tactic:
by

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 : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y ↦ (f x, f y) ∉ V₀
⊢ (range f).Pairwise fun x y ↦ (x, y) ∉ V₀

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set ((α × β) × α × β)
h : s ∈ 𝓤 (α × β)
⊢ ∃ u ∈ 𝓤 α, ∃ v ∈ 𝓤 β, entourageProd u v ⊆ s

Tactic:
by

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 α
⊢ (⨆ i ∈ I, f i).TotallyBounded ↔ ∀ i ∈ I, (f i).TotallyBounded

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ Filter.comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
S : Set (Filter α)
hS : S.Finite
⊢ (sSup S).TotallyBounded ↔ ∀ f ∈ S, f.TotallyBounded

Tactic:
by

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ UniformContinuous fun a ↦ (f₁ a, f₂ a)

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
⊢ TotallyBounded (⋃ i, s i) ↔ ∀ (i : ι), TotallyBounded (s i)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : t ∈ map (Prod.map mk mk) (𝓤 α)
⊢ t ∈ (map (Prod.map mk mk) (𝓤 α)).lift' fun s ↦ SetRel.comp s s

Tactic:
by

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 γ
⊢ Sort ?u.30

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
⊢ Filter.comap mk (𝓝 (mk x)) = Filter.comap mk (Filter.comap (Prod.mk (mk x)) (map (Prod.map mk mk) (𝓤 α)))

Tactic:
by

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

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
⊢ TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : SeparationQuotient α × SeparationQuotient β → γ
⊢ UniformContinuous f ↔ UniformContinuous fun p ↦ f (mk p.1, mk p.2)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
h : UniformContinuous f
a : α
⊢ lift' f (mk a) = f a

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
S : Set (Set α)
hS : S.Finite
⊢ TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

Tactic:
by

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
ua1 ua2 : UniformSpace α
ub1 ub2 : UniformSpace β
uc1 : UniformSpace γ
h : UniformContinuous fun p ↦ f p.1 p.2
⊢ UniformContinuous fun p ↦ f p.1 p.2

Tactic:
by

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
⊢ ⊥.TotallyBounded

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
⊢ UniformContinuous (lift' f)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ lift' (mk ∘ f) (mk a) = mk (f a)

Tactic:
lift'_mk (uniformContinuous_mk.comp h)

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ (mk ∘ f) a = mk (f a)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s t : Set α
⊢ TotallyBounded (s ∪ t) ↔ TotallyBounded s ∧ TotallyBounded t

Tactic:
by

Goal state after: