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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
j : ι
hj : y ∈ s j
⊢ y ∈ s j

Tactic:
]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
x : α
hx : x ∈ t
i : ι
hi : x ∈ s i
y : α
hy : y ∈ t
j : ι
hj : y ∈ s j
⊢ y ∈ s j
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
ι : Type u_2
xs : ι → α
xs_dense : DenseRange xs
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ range xs, ball x U = univ

Tactic:
]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
ι : Type u_2
xs : ι → α
xs_dense : DenseRange xs
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ range xs, ball x U = univ
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)
⊢ ∃ s_1 ∈ 𝓝ˢ s, ∃ t_1 ∈ 𝓝ˢ t, Disjoint s_1 t_1

Tactic:
]

Goal state after:
α : 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)
⊢ ∃ s_1 ∈ 𝓝ˢ s, ∃ t_1 ∈ 𝓝ˢ t, Disjoint s_1 t_1
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 γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q ↦ ((x, q.2), q)
⊢ Tendsto (fun q ↦ (F x q.2, F q.1 q.2)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace β
x : α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
U : Set α
V : Set β
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ V)
hU : x ∈ U
φ : α × β → (α × β) × α × β := fun q ↦ ((x, q.2), q)
⊢ Tendsto (fun q ↦ (F x q.2, F q.1 q.2)) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.fst f✝ (𝓝 x1) ∧ Tendsto Prod.snd f✝ (𝓝 x2)

Tactic:
]

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
f✝ : Filter (α × β)
hf : Cauchy f✝
x1 : α
hx1 : map (fun p ↦ p.1) f✝ ≤ 𝓝 x1
x2 : β
hx2 : map (fun p ↦ p.2) f✝ ≤ 𝓝 x2
⊢ Tendsto Prod.fst f✝ (𝓝 x1) ∧ Tendsto Prod.snd f✝ (𝓝 x2)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x✝ : α
⊢ comap (Prod.mk x✝) (𝓤 α) ⊓ comap (Prod.mk x✝) (𝓤 α) = comap (Prod.mk x✝) (𝓤 α) ⊓ comap (Prod.mk x✝) (𝓤 α)

Tactic:
]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : Subsingleton α
u : UniformSpace α
⊢ univ ∈ (fun u ↦ 𝓤 α) u

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : Subsingleton α
u : UniformSpace α
⊢ univ ∈ (fun u ↦ 𝓤 α) u
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ (𝓤 β).lift' ((fun s ↦ s ○ s) ∘ preimage fun p ↦ (f p.1, f p.2)) ≤
    UniformSpace.uniformity.lift' ((preimage fun p ↦ (f p.1, f p.2)) ∘ fun s ↦ s ○ s)

pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Monotone fun s ↦ s ○ s

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ (𝓤 β).lift' ((fun s ↦ s ○ s) ∘ preimage fun p ↦ (f p.1, f p.2)) ≤
    UniformSpace.uniformity.lift' ((preimage fun p ↦ (f p.1, f p.2)) ∘ fun s ↦ s ○ s)

α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
f : α → β
u : UniformSpace β
⊢ Monotone fun s ↦ s ○ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ ∀ (y : β), u y ∈ K

Tactic:
]

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
K : Set α
h₁ : IsComplete K
u : β → α
h₂ : ∀ (n : β), u n ∈ K
h₃ : CauchySeq u
⊢ ∀ (y : β), u y ∈ K
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
⊢ ball (↑x) (B (U b x)) ∩ ball (↑y) (B (U (!b) y)) ⊆ ∅

Tactic:
]

Goal state after:
α : 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
⊢ ball (↑x) (B (U b x)) ∩ ball (↑y) (B (U (!b) y)) ⊆ ∅
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type u_2
x✝ : UniformSpace α
⊢ 𝓤 α = 𝓤 α

Tactic:
]

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
⊢ UniformContinuous ↿f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace β
x : α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
f : α → β → γ
h : UniformContinuous₂ f
⊢ UniformContinuous ↿f
Module: Mathlib.Topology.UniformSpace.Basic

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

Tactic:
]

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

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : u₁ ≤ u₂
a : α
⊢ (𝓤 α).lift' (ball a) ≤ (𝓤 α).lift' (ball a)

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Type ua
s : Set (UniformSpace α)
⊢ (⨅ a ∈ s, a).toTopologicalSpace = ⨅ i ∈ s, i.toTopologicalSpace
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β
⊢ (∀ (i : ιβ), pβ i → ∀ᶠ (x : X × α) in l ×ˢ l', (f x.2, F x.1 x.2) ∈ sβ i) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X × α) in l ×ˢ l', (f n.2, F n.1 n.2) ∈ sβ i

Tactic:
]

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
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
f : α → β
u₁ : Set (UniformSpace α)
u₂ : UniformSpace β
u : UniformSpace α
h₁ : u ∈ u₁
hf : UniformContinuous f
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ (∀ (x : UniformSpace β) (h : x ∈ u₂), Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)) ↔
    ∀ u ∈ u₂, Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
]

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
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : ι → UniformSpace α
u₂ : UniformSpace β
i : ι
hf : UniformContinuous f
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (⨅ i, 𝓤 α) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
ι : Sort u_1
f : α → β
u₁ : UniformSpace α
u₂ : ι → UniformSpace β
⊢ (∀ (i : ι), Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)) ↔ ∀ (i : ι), Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
]

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

Goal state before:
pp: α : Type ua
s : Set α
inst✝ : UniformSpace α
⊢ 𝓤 α ⊓ 𝓟 (s ×ˢ s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s)

Tactic:
]

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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto ((fun x ↦ (f x.1, f x.2)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔
    Tendsto (fun x ↦ (s.domRestrict f x.1, s.domRestrict f x.2)) (𝓤 ↑s) (𝓤 β)

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
⊢ Tendsto ((fun x ↦ (f x.1, f x.2)) ∘ Prod.map Subtype.val Subtype.val) (𝓤 ↑s) (𝓤 β) ↔
    Tendsto (fun x ↦ (s.domRestrict f x.1, s.domRestrict f x.2)) (𝓤 ↑s) (𝓤 β)
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 (map Subtype.val (𝓝 ⟨a, ⋯⟩)) (𝓝 (f a))

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
a : α
hf : UniformContinuous fun x ↦ f ↑x
ha : s ∈ 𝓝 a
⊢ Tendsto f (map Subtype.val (𝓝 ⟨a, ⋯⟩)) (𝓝 (f a))
Module: Mathlib.Topology.UniformSpace.Basic

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

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.domRestrict f)
⊢ ContinuousOn f s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.domRestrict f)
⊢ Continuous[instTopologicalSpaceSubtype, inst✝.toTopologicalSpace] (s.domRestrict f)

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
h : UniformContinuous (s.domRestrict f)
⊢ Continuous[instTopologicalSpaceSubtype, inst✝.toTopologicalSpace] (s.domRestrict f)
Module: Mathlib.Topology.UniformSpace.Cauchy

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

Tactic:
]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : (𝓟 s).TotallyBounded
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
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 ι
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ᶠ (x : ι × ι) in p ×ˢ p, ∀ y ∈ s, (F (x, y).1.1 (x, y).2, F (x, y).1.2 (x, y).2) ∈ u

Tactic:
]

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
⊢ (Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β)).IsCountablyGenerated

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝³ : UniformSpace α
inst✝² : (𝓤 α).IsCountablyGenerated
inst✝¹ : UniformSpace β
inst✝ : (𝓤 β).IsCountablyGenerated
⊢ (Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β)).IsCountablyGenerated
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
⊢ UniformCauchySeqOn F p s

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
hF : UniformCauchySeqOn F p s
⊢ UniformCauchySeqOn F p s
Module: Mathlib.Topology.UniformSpace.Separation

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

Tactic:
]

Goal state after:
α : Type u
inst✝ : UniformSpace α
x y : α
h : Inseparable x y
⊢ 𝓝 (y, y) ≤ 𝓤 α
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:
simpa only [ball_eq_of_symmetry] using! h V ‹_› ‹_›

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)) (𝓤 α ×ˢ 𝓤 β) =
    Filter.comap (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
]

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)
h : Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)
⊢ ClusterPt (a, b) (𝓤 α)

Tactic:
]

Goal state after:
α : 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)
h : Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)
⊢ ClusterPt (a, b) (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : x ∈ {x | ClusterPt x f}
⊢ x ∈ closure[uniformSpace.toTopologicalSpace] (V.preimage t)

Tactic:
]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : x ∈ {x | ClusterPt x f}
⊢ x ∈ closure[uniformSpace.toTopologicalSpace] (V.preimage t)
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : SetRel β β
f : α → α → β
hf : Tendsto ((fun x ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : SetRel β β
f : α → α → β
hf : Tendsto ((fun x ↦ (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
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
⊢ x ∈ s

Tactic:
]

Goal state after:
α : 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
⊢ x ∈ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
h : TotallyBounded s
⊢ TotallyBounded {a | ClusterPt a (𝓟 s)}

Tactic:
]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : Set α
h : TotallyBounded s
⊢ TotallyBounded {a | ClusterPt a (𝓟 s)}
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
⊢ y ∈ s

Tactic:
]

Goal state after:
α : 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
⊢ y ∈ s
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 ∈ Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 β)

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
t₁ : UniformSpace α
t₂ : UniformSpace β
u : SetRel α α
v : SetRel β β
hu : u ∈ 𝓤 α
hv : v ∈ 𝓤 β
⊢ entourageProd u v ∈ Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓ Filter.comap (fun p ↦ (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
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : α) in p', pb y) ∧
          ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → Tendsto (fun n ↦ F n (x, y).2) p (𝓝 (f (x, y).2))

Tactic:
]

Goal state after:
α : 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
⊢ ∃ pa,
    (∀ᶠ (x : ι × ι) in p ×ˢ p, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : α) in p', pb y) ∧
          ∀ {x : ι × ι}, pa x → ∀ {y : α}, pb y → Tendsto (fun n ↦ F n (x, y).2) p (𝓝 (f (x, y).2))
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:
refine ⟨fun h i ↦ h.mono (le_iSup _ _), fun h U hU ↦ ?_⟩
  choose t htf ht using (h · U hU)
  refine ⟨⋃ i, t i, finite_iUnion htf, ?_⟩
  simp_rw [U.preimage_iUnion, ← le_principal_iff, ← iSup_principal] at ht ⊢
  gcongr; apply ht

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
⊢ (∀ (a : ι) (b : a ∈ I), (f ↑⟨a, b⟩).TotallyBounded) ↔ ∀ i ∈ I, (f i).TotallyBounded

Tactic:
]

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

Goal state before:
pp: case inr
α : 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
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u

Tactic:
]

Goal state after:
case inr
α : 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
hmc : ∀ᶠ (x : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', Tendsto (fun n ↦ F n x.2) p (𝓝 (f x.2))
⊢ ∀ᶠ (y : α × ι) in p' ×ˢ p, (f y.swap.2, F y.swap.1 y.swap.2) ∈ u
Module: Mathlib.Topology.UniformSpace.Cauchy

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

Tactic:
]

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₂
⊢ Tendsto (fun x ↦ ((f₁ x.1, f₂ x.1), f₁ x.2, f₂ x.2)) (𝓤 α)
    (Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 β) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 γ))

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f₁ : α → β
f₂ : α → γ
h₁ : UniformContinuous f₁
h₂ : UniformContinuous f₂
⊢ Tendsto (fun x ↦ ((f₁ x.1, f₂ x.1), f₁ x.2, f₂ x.2)) (𝓤 α)
    (Filter.comap (fun p ↦ (p.1.1, p.2.1)) (𝓤 β) ⊓ Filter.comap (fun p ↦ (p.1.2, p.2.2)) (𝓤 γ))
Module: Mathlib.Topology.UniformSpace.Cauchy

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

Tactic:
]

Goal state after: