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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
⊢ f ⁻¹' t ⊆ u ∪ v → Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
huv

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
⊢ Disjoint u v → f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a))
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)

Tactic:
← di.nhds_eq_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : IsDenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ 𝓝 a
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace γ
di : IsDenseInducing i
f : α → γ
a : α
hf : ContinuousAt f a
⊢ Tendsto f (𝓝 a) (𝓝 ((comap i (𝓝 (i a))).limUnder f))

Tactic:
← di.nhds_eq_comap

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
inst✝ : TopologicalSpace γ
di : IsDenseInducing i
f : α → γ
a : α
hf : ContinuousAt f a
⊢ Tendsto f (𝓝 a) (𝓝 ((𝓝 a).limUnder f))
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case neg
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
hy : ∃ x, ∃ (_ : x ∈ 𝓝 y), ∃ x_1, ∃ (_ : x_1 ∈ l), Disjoint x x_1
⊢ ∃ x ∈ insert y (range f), ClusterPt x l

Tactic:
rcases hy with ⟨s, hsy, t, htl, hd⟩

Goal state after:
case neg
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (coLindelof X) (𝓝 y)
hfc : Continuous[inst✝², inst✝¹] f
l : Filter Y
hne : l.NeBot
inst✝ : CountableInterFilter l
hle : l ≤ 𝓟 (insert y (range f))
s : Set Y
hsy : s ∈ 𝓝 y
t : Set Y
htl : t ∈ l
hd : Disjoint s t
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
⊢ ⋃ y ∈ T₁, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ u

Tactic:
refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
t' : β
ht' : t' ∈ T₁
⊢ f ⁻¹' {t'} ⊆ f ⁻¹' t
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
e : α → β
p : β → Prop
he : DenseRange e
hp : IsClosed[inst✝] {x | p x}
h : ∀ (a : α), p (e a)
⊢ ∀ (b : β), p b

Tactic:
by
  have : univ ⊆ { b | p b } :=
    calc
      univ = closure (range e) := he.closure_range.symm
      _ ⊆ closure { b | p b } := closure_mono <| range_subset_iff.mpr h
      _ = _ := hp.closure_eq
  simpa only [univ_subset_iff, eq_univ_iff_forall, mem_ofPred]

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
⊢ ⋃ y ∈ T₂, f ⁻¹' {y} ⊆ f ⁻¹' t ∩ v

Tactic:
refine iUnion₂_subset fun t' ht' => subset_inter ?_ ht'.2

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
t' : β
ht' : t' ∈ T₂
⊢ f ⁻¹' {t'} ⊆ f ⁻¹' t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v

Tactic:
have T_decomp : t ⊆ T₁ ∪ T₂ := fun t' ht' => by
    rw [mem_union t' T₁ T₂]
    rcases fiber_decomp t' ht' with htu | htv
    · left; exact ⟨ht', htu⟩
    · right; exact ⟨ht', htv⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht' : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
T_decomp : t ⊆ T₁ ∪ T₂
⊢ f ⁻¹' t ⊆ u ∨ f ⁻¹' t ⊆ v
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 Z
W : Type u_5
inst✝ : TopologicalSpace W
f✝ f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
⊢ IsHomeomorph ⋯.connectedComponentsMap

Tactic:
have hbij := hf.connectedComponentsMap_bijective hf'

Goal state after:
X : Type u_1
Y : Type u_2
W✝ : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
W : Type u_5
inst✝ : TopologicalSpace W
f✝ f : X → Y
hf : IsCoinducing f
hf' : ∀ (y : Y), IsConnected (f ⁻¹' {y})
hbij : Bijective ⋯.connectedComponentsMap
⊢ IsHomeomorph ⋯.connectedComponentsMap
Module: Mathlib.Topology.UniformSpace.DiscreteUniformity

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
h : SetRel.id = ⋂ y, {p | p.2 = y → p.1 ∈ {y}}
⊢ SetRel.id ∈ uniformity Y

Tactic:
h,

Goal state after:
X : Type u_1
u : UniformSpace X
inst✝³ : DiscreteUniformity X
Y : Type u_2
inst✝² : Finite Y
inst✝¹ : UniformSpace Y
inst✝ : DiscreteTopology Y
h : SetRel.id = ⋂ y, {p | p.2 = y → p.1 ∈ {y}}
⊢ ⋂ y, {p | p.2 = y → p.1 ∈ {y}} ∈ uniformity Y
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
u : Core α
t : TopologicalSpace α
h : t = u.toTopologicalSpace
x : α
⊢ 𝓝 x = comap (Prod.mk x) u.uniformity

Tactic:
h,

Goal state after:
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u
u : Core α
t : TopologicalSpace α
h : t = u.toTopologicalSpace
x : α
⊢ 𝓝 x = comap (Prod.mk x) u.uniformity
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
i : TopologicalSpace α
u : UniformSpace α
h : i = u.toTopologicalSpace
x : α
⊢ 𝓝 x = comap (Prod.mk x) UniformSpace.uniformity

Tactic:
h,

Goal state after:
α✝ : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
i : TopologicalSpace α
u : UniformSpace α
h : i = u.toTopologicalSpace
x : α
⊢ 𝓝 x = comap (Prod.mk x) UniformSpace.uniformity
Module: Mathlib.Topology.UniformSpace.Basic

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

Tactic:
by
  rw [nhds_prod_eq]
  apply (hasBasis_nhds x).prod_same_index (hasBasis_nhds y)
  rintro U V ⟨U_in, U_symm⟩ ⟨V_in, V_symm⟩
  exact ⟨U ∩ V, ⟨(𝓤 α).inter_sets U_in V_in, inferInstance⟩, ball_inter_left x U V,
    ball_inter_right y U V⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
V : SetRel α α
V_in : V ∈ 𝓤 α
⊢ ball x V ∈ 𝓝 x

Tactic:
rw [UniformSpace.mem_nhds_iff]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
V : SetRel α α
V_in : V ∈ 𝓤 α
⊢ ∃ V_1 ∈ 𝓤 α, ball x V_1 ⊆ ball x V
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

Tactic:
rw [UniformSpace.mem_nhds_iff]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
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 : l ≤ 𝓟 S
⊢ ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
rw [le_principal_iff] at hls

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
⊢ ∃ x ∈ S, l ≤ 𝓝 x
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:
change Tendsto (Prod.map ↿F ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)

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 (Prod.map ↿F ↿F ∘ φ) (𝓝[U] x ×ˢ 𝓟 V) (𝓤 γ)
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:
simp only [UniformCauchySeqOn, UniformCauchySeqOnFilter]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
⊢ (∀ u ∈ 𝓤 β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ 𝓟 s, (F m.1.1 m.2, F m.1.2 m.2) ∈ u
Module: Mathlib.Topology.UniformSpace.Separation

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

Tactic:
uniformity_hasBasis_closed.inseparable_iff_uniformity,

Goal state after:
α : Type u
inst✝ : UniformSpace α
x y : α
h : ClusterPt (x, y) (𝓤 α)
⊢ ∀ (i : SetRel α α), i ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] i → (x, y) ∈ id i
Module: Mathlib.Topology.UniformSpace.Separation

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

pp: case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift' f)

Tactic:
· rwa [lift', dif_pos hf, uniformContinuous_lift]

Goal state after:
case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift' f)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
a✝ : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ m, ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
⊢ ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}

Tactic:
refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
  exact h_subset hx

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 α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s

Tactic:
have p3 : ∀ᶠ i in p, ∀ᶠ x in p', (f x, F i x) ∈ t := (h1 t ht).curry

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
inst✝ : p.NeBot
L : ι → β
ℓ : β
h1 : TendstoUniformlyOnFilter F f p p'
h2 : ∀ᶠ (i : ι) in p, Tendsto (F i) p' (𝓝 (L i))
h3 : Tendsto L p (𝓝 ℓ)
s : Set (β × β)
hs : s ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
hts : SetRel.comp t (SetRel.comp t t) ⊆ s
p1 : ∀ᶠ (i : ι) in p, (L i, ℓ) ∈ t
p2 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (F i x, L i) ∈ t
p3 : ∀ᶠ (i : ι) in p, ∀ᶠ (x : α) in p', (f x, F i x) ∈ t
⊢ ∀ᶠ (x : α) in p', (f x, ℓ) ∈ s
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

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

Tactic:
Subtype.range_coe_subtype

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)
ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst✝².toTopologicalSpace] (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ {x | p x} ∈ comap e (𝓝 b)
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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this✝ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d

Tactic:
have : interior t ∈ 𝓝 (x₁, x₂) := isOpen_interior.mem_nhds hx_t

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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
⊢ 𝓤 γ = 𝓤 γ

Tactic:
have : @CompactSpace γ u.toTopologicalSpace := by rwa [h]

Goal state after:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ ⨆ x, 𝓝 (x, x) = ⨆ x, 𝓝 (x, x)

Tactic:
h,

Goal state after:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ ⨆ x, 𝓝 (x, x) = ⨆ x, 𝓝 (x, x)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : ι → X → R
h✝ : LocallyFinite fun i ↦ support (s i)
f : ι → X → M
i : ι
x : X
h : s i x = 0
⊢ s i x • f i x = 0

Tactic:
h,

Goal state after:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
s : ι → X → R
h✝ : LocallyFinite fun i ↦ support (s i)
f : ι → X → M
i : ι
x : X
h : s i x = 0
⊢ 0 • f i x = 0
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst✝² : TopologicalSpace X
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : ι → X → M
h✝ : LocallyFinite fun i ↦ support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
⊢ s i x • f i x = 0

Tactic:
h,

Goal state after:
X : Type u_1
M : Type u_7
R : Type u_8
ι : Type u_9
inst✝² : TopologicalSpace X
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : ι → X → M
h✝ : LocallyFinite fun i ↦ support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
⊢ s i x • 0 = 0
Module: Mathlib.Topology.UniformSpace.Equiv

Goal state before:
pp: α : Type u
β : Type u_1
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
e : α ≃ β
h₁ : UniformContinuous e.toFun
h₂ : UniformContinuous e.invFun
e' : α ≃ β
h₁' : UniformContinuous e'.toFun
h₂' : UniformContinuous e'.invFun
h :
  { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ }.toEquiv =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' }.toEquiv
⊢ { toEquiv := e, uniformContinuous_toFun := h₁, uniformContinuous_invFun := h₂ } =
    { toEquiv := e', uniformContinuous_toFun := h₁', uniformContinuous_invFun := h₂' }

Tactic:
by simpa only [mk.injEq]

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set X
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → X → α
x₀ : X
hX : (𝓝 x₀).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

Tactic:
rw [equicontinuousAt_iff_continuousAt, ContinuousAt,
    hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)]
  rfl

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : Tendsto F l (𝓝 f)
h₂ : EquicontinuousWithinAt F univ x₀
⊢ ContinuousWithinAt f univ x₀

Tactic:
tendsto_pi_nhds

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : ∀ (x : X), Tendsto (fun i ↦ F i x) l (𝓝 (f x))
h₂ : EquicontinuousWithinAt F univ x₀
⊢ ContinuousWithinAt f univ x₀
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : Tendsto F l (𝓝 f)
h₂ : UniformEquicontinuousOn F univ
⊢ UniformContinuousOn f univ

Tactic:
tendsto_pi_nhds

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
h₁ : ∀ (x : β), Tendsto (fun i ↦ F i x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F univ
⊢ UniformContinuousOn f univ