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

Goal state before:
pp: case inr.succ.succ.cons.refine_4
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
i : Fin (n + 1)
U : Fin n → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
h₃ : Pairwise (Disjoint on (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons (a ∪ b) U))
h₁ : ∀ (i_1 : Fin (n + 1)), IsClopen (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1))
h₂ : ∀ (i_1 : Fin (n + 1)), (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1)).Nonempty
h₄ : ⋃ i_1, Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1) = univ
hi : ¬IsConnected (a ∪ b)
⊢ ⋃ i, Fin.cons a (Fin.cons b U) i = univ

Tactic:
simpa using

Goal state after:
case inr.succ.succ.cons.refine_4
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
i : Fin (n + 1)
U : Fin n → Set α
a b : Set α
ha : IsClopen a
hb : IsClopen b
ha' : a.Nonempty
hb' : b.Nonempty
hab : Disjoint a b
h₃ : Pairwise (Disjoint on (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons (a ∪ b) U))
h₁ : ∀ (i_1 : Fin (n + 1)), IsClopen (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1))
h₂ : ∀ (i_1 : Fin (n + 1)), (Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1)).Nonempty
h₄ : ⋃ i_1, Fin.cons (a ∪ b) U ((Equiv.swap 0 i) i_1) = univ
hi : ¬IsConnected (a ∪ b)
⊢ a ∪ b ∪ ⋃ i, U i = univ
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
this : ContinuousOn u.boolIndicator s
⊢ False

Tactic:
simpa using

Goal state after:
α : 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
this : ContinuousOn u.boolIndicator s
⊢ False
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this✝ : f.NeBot
this : g.NeBot
⊢ Cauchy (f ×ˢ g)

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
g : Filter β
hf : Cauchy f
hg : Cauchy g
this✝ : f.NeBot
this : g.NeBot
⊢ Cauchy f ∧ Cauchy g
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
s : Set α
hm : UniformContinuousOn m s
hfs : f ≤ 𝓟 s
this : Cauchy (Filter.comap Subtype.val f)
⊢ Cauchy (map m f)

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : UniformSpace β
f : Filter α
m : α → β
hf : Cauchy f
s : Set α
hm : UniformContinuousOn m s
hfs : f ≤ 𝓟 s
this : Cauchy (Filter.comap Subtype.val f)
⊢ Cauchy (map m f)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
u : β → α
h : CauchySeq u
⊢ Tendsto (Prod.map u u) atTop (𝓤 α)

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝ : Preorder β
u : β → α
h : CauchySeq u
⊢ map (Prod.map u u) atTop ≤ 𝓤 α
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
simpa using

Goal state after:
α : Type u
uniformSpace : UniformSpace α
β : Type u_1
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
V : SetRel α α
hV : V ∈ 𝓤 α
this✝ : Nonempty β
this : Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
f : ℕ ≃ ℕ
H : CauchySeq (u ∘ ⇑f)
⊢ CauchySeq u

Tactic:
simpa using

Goal state after:
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
f : ℕ ≃ ℕ
H : CauchySeq (u ∘ ⇑f)
⊢ CauchySeq u
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Type u_1
δ : Type u_2
inst✝² : UniformSpace β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
u : γ → α
v : δ → β
hu : CauchySeq u
hv : CauchySeq v
⊢ CauchySeq (Prod.map u v)

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Type u_1
δ : Type u_2
inst✝² : UniformSpace β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
u : γ → α
v : δ → β
hu : CauchySeq u
hv : CauchySeq v
⊢ Cauchy (map (Prod.map u v) atTop)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h✝ : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
i : ι
h : ∀ᶠ (y : α) in p', (f y, F i y) ∈ u
⊢ i ∈ (fun x_1 ↦ (f x, F x_1 x)) ⁻¹' u

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h✝ : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
i : ι
h : ∀ᶠ (y : α) in p', (f y, F i y) ∈ u
⊢ (f x, F i x) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOnFilter F f p (𝓟 s)
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n ↦ F n ∘ g) (f ∘ g) p (𝓟 (g ⁻¹' s))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOnFilter F f p (𝓟 s)
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n ↦ F n ∘ g) (f ∘ g) p (𝓟 (g ⁻¹' s))
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformlyOnFilter F f p ⊤
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n ↦ F n ∘ g) (f ∘ g) p ⊤

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformlyOnFilter F f p ⊤
g : γ → α
⊢ TendstoUniformlyOnFilter (fun n ↦ F n ∘ g) (f ∘ g) p ⊤
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 ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOnFilter F f p (𝓟 s)
h' : TendstoUniformlyOnFilter F' f' p' (𝓟 s')
⊢ TendstoUniformlyOnFilter (fun i ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (𝓟 (s ×ˢ s'))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
s' : Set α'
h : TendstoUniformlyOnFilter F f p (𝓟 s)
h' : TendstoUniformlyOnFilter F' f' p' (𝓟 s')
⊢ TendstoUniformlyOnFilter (fun i ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (𝓟 (s ×ˢ s'))
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 ∈ 𝓤 α
⊢ ⋃ i, ball (xs i) U = univ

Tactic:
rw [← biUnion_range (f := xs) (g := fun x ↦ UniformSpace.ball x U)]

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.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace (α × β)
h : Nonempty β
f✝ : Filter α
hf : Cauchy f✝
y : β
a : α
b : β
hab : f✝ ×ˢ pure y ≤ 𝓝 (a, b)
⊢ f✝ ≤ 𝓝 a

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace (α × β)
h : Nonempty β
f✝ : Filter α
hf : Cauchy f✝
y : β
a : α
b : β
hab : f✝ ×ˢ pure y ≤ 𝓝 (a, b)
⊢ f✝ ≤ 𝓝 a
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace (α × β)
h : Nonempty α
f✝ : Filter β
hf : Cauchy f✝
x a : α
b : β
hab : pure x ×ˢ f✝ ≤ 𝓝 (a, b)
⊢ f✝ ≤ 𝓝 b

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace (α × β)
h : Nonempty α
f✝ : Filter β
hf : Cauchy f✝
x a : α
b : β
hab : pure x ×ˢ f✝ ≤ 𝓝 (a, b)
⊢ f✝ ≤ 𝓝 b
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 α
hU : U ∈ 𝓝 x
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ univ)
⊢ TendstoUniformly F (F x) (𝓝 x)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace β
x : α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
U : Set α
hU : U ∈ 𝓝 x
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ univ)
⊢ TendstoUniformly F (F x) (𝓝 x)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
hf : Cauchy f
⊢ ∃ x, f = pure x

Tactic:
by
  rcases hf with ⟨f_ne_bot, f_le⟩
  simp only [DiscreteUniformity.eq_principal_setRelId, le_principal_iff, mem_prod_iff] at f_le
  obtain ⟨S, hS, T, hT, H⟩ := f_le
  obtain ⟨x, rfl, _, _, _⟩ := SetRel.exists_eq_singleton_of_prod_subset_id
    (f_ne_bot.nonempty_of_mem hS) (f_ne_bot.nonempty_of_mem hT) H
  exact ⟨x, f_ne_bot.le_pure_iff.mp <| le_pure_iff.mpr hS⟩

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

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

Tactic:
by
  ext : 2
  rw [uniformity_comap, Prod.map_id, comap_id]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = 𝓤 α

Tactic:
rw [← hf.1, ← hg.1, comap_comap]

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x ↦ ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = comap ((fun x ↦ (g x.1, g x.2)) ∘ fun x ↦ (f x.1, f x.2)) (𝓤 γ)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
hs : s ∈ 𝓤 α
x : α × α
h : x ∈ Prod.map Sum.inl Sum.inl ⁻¹' (Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr))
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
hs : s ∈ 𝓤 α
x : α × α
h : x ∈ Prod.map Sum.inl Sum.inl ⁻¹' (Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr))
⊢ x ∈ s
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
hs : s ∈ 𝓤 β
x : β × β
h : x ∈ Prod.map Sum.inr Sum.inr ⁻¹' (range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s)
⊢ x ∈ s

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
hs : s ∈ 𝓤 β
x : β × β
h : x ∈ Prod.map Sum.inr Sum.inr ⁻¹' (range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s)
⊢ x ∈ s
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
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
⊢ {x | (x, y) ∈ d}ᶜ ∈ c

Tactic:
simpa using

Goal state after:
α : 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
this : f ≤ g
c : Filter α
hcf : c ≤ f
hc : Cauchy c
m : Set α
hm : m ∈ c
hmd : m ×ˢ m ⊆ d
y : α
hym : y ∈ m
⊢ {x | (x, y) ∈ d}ᶜ ∈ c
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 ι
γ : Type u_5
hf : UniformCauchySeqOnFilter F p (𝓟 s)
g : γ → α
⊢ UniformCauchySeqOnFilter (fun n ↦ F n ∘ g) p (𝓟 (g ⁻¹' s))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
γ : Type u_5
hf : UniformCauchySeqOnFilter F p (𝓟 s)
g : γ → α
⊢ UniformCauchySeqOnFilter (fun n ↦ F n ∘ g) p (𝓟 (g ⁻¹' s))
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
x y : α
⊢ (x, y) ∈ Prod.map f f ⁻¹' s → (x, y) ∈ SetRel.id

Tactic:
simpa using

Goal state after:
β : Type v
inst✝ : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y ↦ (f x, f y) ∉ s
x y : α
⊢ (f x, f y) ∈ s → x = y
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
p : α → Prop
e : α → β
ue : IsUniformEmbedding e
de : IsDenseEmbedding e
⊢ comap (fun x ↦ (IsDenseEmbedding.subtypeEmb p e x.1, IsDenseEmbedding.subtypeEmb p e x.2))
      (𝓤 { x // x ∈ closure[inst✝.toTopologicalSpace] (e '' {x | p x}) }) =
    𝓤 { x // p x }

Tactic:
simp [comap_comap, Function.comp_def, IsDenseEmbedding.subtypeEmb, uniformity_subtype,
        ue.comap_uniformity.symm]

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

Goal state before:
pp: α✝ : Type u
β : Type v
uniformSpace : UniformSpace α✝
α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
f✝ : Filter α
hf : Cauchy f✝
⊢ ∃ x, f✝ ≤ 𝓝 x

Tactic:
simpa using

Goal state after:
α✝ : Type u
β : Type v
uniformSpace : UniformSpace α✝
α : Type u
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
f✝ : Filter α
hf : Cauchy f✝
⊢ ∃ x, f✝ ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
completeSpace_iff_isComplete_range hf,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
⊢ IsComplete (range f) ↔ CompleteSpace β
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen[inst✝.toTopologicalSpace] s
hcover : K ⊆ ⋃ i, ↑i
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s

Tactic:
simpa using

Goal state after:
α : Type ua
inst✝ : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen[inst✝.toTopologicalSpace] s
hcover : K ⊆ ⋃ i, ↑i
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
a : α
ha : Tendsto (seq hf U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → seq hf U_mem b ∈ {y | (a, y) ∈ U m}
⊢ (a, seq hf U_mem (max m n)) ∈ s

Tactic:
· exact hm (hn _ <| le_max_right m n)

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

Goal state before:
pp: α : 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
⊢ K ⊆ ⋃ x, interior U

Tactic:
simpa using

Goal state after:
α : 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
⊢ U ∈ 𝓝ˢ K
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : IsUniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
a : α
⊢ Tendsto f (comap e (𝓝 a)) (𝓝 (⋯.extend f a))

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : IsUniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
a : α
⊢ Tendsto f (comap e (𝓝 a)) (𝓝 ((comap e (𝓝 a)).limUnder f))
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : 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) ⊆ interior U

Tactic:
simpa using

Goal state after:
α : 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 ∧ ∀ i_1 ∈ K, ball i_1 (V i) ⊆ interior U
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_9
β : Type u_10
inst✝¹ : TopologicalSpace α
inst✝ : DivisionMonoid β
f : α → β
hf : HasCompactMulSupport f
⊢ HasCompactMulSupport f⁻¹

Tactic:
simpa using

Goal state after:
α : Type u_9
β : Type u_10
inst✝¹ : TopologicalSpace α
inst✝ : DivisionMonoid β
f : α → β
hf : HasCompactMulSupport f
⊢ IsCompact (closure[inst✝¹] (mulSupport f))
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
a✝ : α
⊢ (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) (i a✝) = SeparationQuotient.mk (i a✝)

Tactic:
simpa using

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
a✝ : α
⊢ Inseparable (hg.extend i (ff a✝)) (i a✝)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
x : α
⊢ ((SeparationQuotient.mk ∘ ⋯.extend f) ∘ i) x = (SeparationQuotient.mk ∘ f) x

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
x : α
⊢ Inseparable (⋯.extend f (i x)) (f x)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
⊢ ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ univ ⊆ ⋃ x ∈ t, ball x U

Tactic:
simpa using

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
hs : ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
⊢ ∀ U ∈ 𝓤 α, ∃ t, t.Countable ∧ ⋃ x ∈ t, ball x U = univ
Module: Mathlib.Topology.UniformSpace.Pi

Goal state before:
pp: ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
this : IsUniformInducing (const ι)
⊢ CompleteSpace X

Tactic:
simp_rw [@completeSpace_iff_isComplete_range _ _ (_) (_) _ this, range_const_eq_diagonal,
    ofPred_forall]

Goal state after:
ι : Type u_4
X : Type u_5
u : ι → UniformSpace X
hu : ∀ (i : ι), CompleteSpace X
a✝ : Nontrivial X
t : TopologicalSpace X
ht : T2Space X
hut : ∀ (i : ι), (u i).toTopologicalSpace ≤ t
this : IsUniformInducing (const ι)
⊢ IsComplete (⋂ i, ⋂ i_1, {x | x i = x i_1})
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOn F f p s
u : Set (β × β)
hu : u ∈ 𝓤 β
x✝¹ : α
x✝ : x✝¹ ∈ s
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h : TendstoUniformlyOn F f p s
u : Set (β × β)
hu : u ∈ 𝓤 β
x✝¹ : α
x✝ : x✝¹ ∈ s
⊢ ∀ᶠ (n : ι) in p, ∀ y ∈ s, (f y, F n y) ∈ u