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

Goal state before:
pp: X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hf : ∀ (i : ι'), IsOpen[inst✝¹] (f i)
⊢ ∀ t ∈ range f, IsOpen[inst✝¹] t

Tactic:
by rwa [forall_mem_range]

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

Goal state before:
pp: case inr
α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
x : α
hx : x ∈ S
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
exact ⟨f x, hTm hx, fun x' hx' => hS.constant_of_mapsTo hT hc hTm hx' hx⟩

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

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

Tactic:
apply (equivOfIsClopen hclopen hdisj hunion).symm.injective

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
i : ι
x : α
hx : x ∈ U i
⊢ (equivOfIsClopen hclopen hdisj hunion).symm ((equivOfIsClopen hclopen hdisj hunion) (mk x)) =
    (equivOfIsClopen hclopen hdisj hunion).symm ⟨i, mk ⟨x, hx⟩⟩
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}}
⊢ ∀ (i : Y), {p | p.2 = i → p.1 ∈ {i}} ∈ uniformity Y

Tactic:
← mem_nhds_uniformity_iff_left,

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}}
⊢ ∀ (i : Y), {i} ∈ nhds i
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case hopen
α : Type u
u : Core α
x a : α
U : Set (α × α)
⊢ U ∈ u.uniformity → ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity

Tactic:
hU

Goal state after:
case hopen
α : Type u
u : Core α
x a : α
U : Set (α × α)
hU : U ∈ u.uniformity
⊢ ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id U ∈ comap (Prod.mk x) u.uniformity
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
⊢ f ≤ 𝓝 x

Tactic:
intro s hs

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
x : α
adhs : ∀ s ∈ 𝓤 α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t
s : Set α
hs : s ∈ 𝓝 x
⊢ s ∈ f
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 (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
← prod_atTop_atTop_eq

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.2 = x → p.1 ∈ s} ∈ 𝓤 α

Tactic:
rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α ↔ {p | p.2 = x → p.1 ∈ s} ∈ map Prod.swap (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ Tendsto (Prod.map u u) atTop (𝓤 α) ↔ ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
← prod_atTop_atTop_eq

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α) ↔
    ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
⊢ Tendsto (Prod.map f f) atTop (𝓤 α)

Tactic:
intro s hs

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ s ∈ map (Prod.map f f) atTop
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mp
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

pp: case mpr
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
· rintro ⟨V, V_in, V_sub⟩
    use SetRel.symmetrize V, symmetrize_mem_uniformity V_in, inferInstance
    exact Subset.trans (ball_mono SetRel.symmetrize_subset_self x) V_sub

Goal state after:
case mpr
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 α, ball x V ⊆ s
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
b : Bool
x : ↑(S b)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
i : ι
hi : B i ⊆ V
⊢ ∃ i, Disjoint (ball (↑x) ((B i).comp (B i).inv)) (S !b)

Tactic:
refine ⟨i, subset_compl_iff_disjoint_right.1 (subset_trans (ball_mono ?_ x.1) hU)⟩

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
b : Bool
x : ↑(S b)
hST : (S !b)ᶜ ∈ 𝓝ˢ (S b)
U : Set (α × α)
hUu : U ∈ 𝓤 α
hU : ball (↑x) U ⊆ (S !b)ᶜ
V : SetRel α α
hV : V ∈ 𝓤 α
hVs : V.IsSymm
hVU : V.comp V ⊆ U
i : ι
hi : B i ⊆ V
⊢ (B i).comp (B i).inv ⊆ U
Module: Mathlib.Topology.UniformSpace.Basic

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

Tactic:
@nhds_inf _ u₁.toTopologicalSpace _,

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u₁ u₂ : UniformSpace α
x✝ : α
⊢ 𝓝 x✝ ⊓ 𝓝 x✝ = comap (Prod.mk x✝) (𝓤 α ⊓ 𝓤 α)
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
⊢ IsUniformEmbedding f

Tactic:
let _ : UniformSpace α := ⊥; have := discreteTopology_bot α
  exact IsUniformInducing.isUniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
⊢ ∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}

Tactic:
obtain ⟨n, hn⟩ := cauchySeq_iff.1 hs a ha

Goal state after:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
⊢ ∃ t, t.Finite ∧ range s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ a}
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
⊢ TotallyBounded (range s)

Tactic:
by
  intro a ha
  obtain ⟨n, hn⟩ := cauchySeq_iff.1 hs a ha
  refine ⟨s '' { k | k ≤ n }, (finite_le_nat _).image _, ?_⟩
  rw [range_subset_iff, biUnion_image]
  intro m
  rw [mem_iUnion₂]
  rcases le_total m n with hm | hm
  exacts [⟨m, hm, refl_mem_uniformity ha⟩, ⟨n, le_refl n, hn m hm n le_rfl⟩]

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 (𝓝 ℓ)
⊢ Tendsto (fun x ↦ (f x, ℓ)) p' (𝓤 β)

Tactic:
intro s hs

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 ∈ 𝓤 β
⊢ s ∈ map (fun x ↦ (f x, ℓ)) p'
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : ∀ x ∈ sᶜ, ∀ᶠ (y : α × β) in nhds x, y ∈ sᶜ
t : Set β
ht : IsCompact t
⊢ ∀ x ∈ (s.preimage t)ᶜ, ∀ᶠ (y : α) in nhds x, y ∈ (s.preimage t)ᶜ

Tactic:
simp_rw [Set.mem_compl_iff, SetRel.mem_preimage, not_exists, not_and]

Goal state after:
α : Type ua
β : Type ub
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : SetRel α β
hs : ∀ x ∈ sᶜ, ∀ᶠ (y : α × β) in nhds x, y ∈ sᶜ
t : Set β
ht : IsCompact t
⊢ ∀ (x : α), (∀ x_1 ∈ t, (x, x_1) ∉ s) → ∀ᶠ (y : α) in nhds x, ∀ x ∈ t, (y, x) ∉ s
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
this : (mulSupport fun i ↦ f i z) ⊆ ↑hnf.toFinset
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
by
        refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
        specialize hz i ⟨z, ⟨hi, hzn⟩⟩
        contrapose hz
        simp [hz, subset_mulTSupport (f i) hi]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable ↑(t n)
o : (n : ℕ) → (x : ↑(t n)) → (ball (↑x) (B n) ∩ s).Nonempty → α
hox : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x) (B n)
hos : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
U : Set (α × α)
⊢ U ∈ 𝓤 α → (ball x U ∩ ⋃ n, ⋃ x, range (o n x)).Nonempty

Tactic:
hU

Goal state after:
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
s : Set α
B : ℕ → SetRel α α
hB : (𝓤 α).HasAntitoneBasis B
right✝ : ∀ (n : ℕ), (B n).IsSymm
t : ℕ → Set α
tC : ∀ (n : ℕ), (t n).Countable
ht : ∀ (n : ℕ), s ⊆ ⋃ x ∈ t n, ball x (B n)
this : ∀ (n : ℕ), Countable ↑(t n)
o : (n : ℕ) → (x : ↑(t n)) → (ball (↑x) (B n) ∩ s).Nonempty → α
hox : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ ball (↑x) (B n)
hos : ∀ (n : ℕ) (x : ↑(t n)) (hx : (ball (↑x) (B n) ∩ s).Nonempty), o n x hx ∈ s
x : α
hx : x ∈ s
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ (ball x U ∩ ⋃ n, ⋃ x, range (o n x)).Nonempty
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
g : ι → α
h : ContinuousWithinAt f univ x
hg : Tendsto g p (𝓝[univ] x)
hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ Tendsto (fun n ↦ F n (g n)) p (𝓝 (f x))

Tactic:
exact tendsto_comp_of_locally_uniform_limit_within h hg hunif

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

Goal state before:
pp: case mp
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
⊢ U ∈ 𝓤 α → ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
hU

Goal state after:
case mp
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : EquicontinuousWithinAt F S x₀
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: case mpr
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
⊢ U ∈ 𝓤 α → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

Tactic:
hU

Goal state after:
case mpr
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
hx₀ : x₀ ∈ S
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ IsUniformEmbedding ⇑(toFun {s | s.Finite})

Tactic:
refine ⟨⟨?_⟩, Function.injective_id⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ comap (fun x ↦ ((toFun {s | s.Finite}) x.1, (toFun {s | s.Finite}) x.2)) (𝓤 (α → β)) = 𝓤 (α →ᵤ[{s | s.Finite}] β)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

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

Tactic:
hU

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ ∀ i ∈ 𝔖,
    ∃ I,
      I.Finite ∧
        (∀ i ∈ I, i ∈ 𝔗) ∧
          ⋂ i ∈ I, UniformOnFun.gen 𝔗 i V ⊆
            {x | ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.2) ∈ UniformOnFun.gen 𝔖 i V}

Tactic:
intro s hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
s : Set α
hs : s ∈ 𝔖
⊢ ∃ I,
    I.Finite ∧
      (∀ i ∈ I, i ∈ 𝔗) ∧
        ⋂ i ∈ I, UniformOnFun.gen 𝔗 i V ⊆
          {x | ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.2) ∈ UniformOnFun.gen 𝔖 s V}
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
⊢ U ∈ 𝓤 α → ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U

Tactic:
hU

Goal state after:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
x₀ : X
hA : EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
hu₁ : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
hu₂ : Continuous[tY, uα.toTopologicalSpace] (eval x₀ ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x : X) in 𝓝[S] x₀, ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i x₀, (u ∘ Subtype.val) i x) ∈ U
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
⊢ U ∈ 𝓤 α →
    ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
      ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i xy.1, (u ∘ Subtype.val) i xy.2) ∈ U

Tactic:
hU

Goal state after:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
    ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i xy.1, (u ∘ Subtype.val) i xy.2) ∈ U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ uniformSpace α γ 𝔖 = ⨅ i, uniformSpace α γ 𝔖

Tactic:
by
  simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]
  rw [iInf_comm]
  exact iInf_congr fun s => iInf_comm

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 → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x ↦ F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
⊢ U ∈ 𝓝 (f x₀) → U ∈ map f (𝓝[S] x₀)

Tactic:
hU

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 → α
S : Set X
x₀ : X
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : Tendsto (fun x ↦ F x x₀) l (𝓝 (f x₀))
h₃ : EquicontinuousWithinAt F S x₀
U : Set α
hU : U ∈ 𝓝 (f x₀)
⊢ U ∈ map f (𝓝[S] 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 : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
U : Set (α × α)
⊢ U ∈ 𝓤 α → U ∈ map (fun x ↦ (f x.1, f x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S))

Tactic:
hU

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst✝ : l.NeBot
F : ι → β → α
f : β → α
S : Set β
h₁ : ∀ x ∈ S, Tendsto (fun x_1 ↦ F x_1 x) l (𝓝 (f x))
h₂ : UniformEquicontinuousOn F S
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ U ∈ map (fun x ↦ (f x.1, f x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S))
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 ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x ↦ F x y) l (𝓝 (f y))
hx : x ∈ closure[tX] s
U : Set (α × α)
⊢ U ∈ 𝓤 α → ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}

Tactic:
hU

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x ↦ F x y) l (𝓝 (f y))
hx : x ∈ closure[tX] s
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x_1 : ι) in l, F x_1 x ∈ {y | (y, z) ∈ id U}
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ⨅ i,
      UniformSpace.comap (Function.eval i ∘ fun f s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) f)))
        (UniformFun.uniformSpace (↑↑i) β) =
    uniformSpace α β 𝔖

Tactic:
iInf_subtype

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ⨅ i,
      ⨅ (x : i ∈ 𝔖),
        UniformSpace.comap (Function.eval ⟨i, ⋯⟩ ∘ fun f s ↦ UniformFun.ofFun ((↑s).domRestrict ((toFun 𝔖) f)))
          (UniformFun.uniformSpace (↑i) β) =
    uniformSpace α β 𝔖
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
U : Set (β × β)
⊢ U ∈ 𝓤 β →
    ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
      (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx ↦ (toFun 𝔖) fx.1 fx.2) a ∈ SetRel.comp U U

Tactic:
hU

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx ↦ (toFun 𝔖) fx.1 fx.2) a ∈ SetRel.comp U U
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
⊢ F ≤ 𝓝 ((ofFun 𝔖) g)

Tactic:
simp_rw [UniformOnFun.nhds_eq_of_basis _ _ uniformity_hasBasis_closed, le_iInf₂_iff,
      le_principal_iff]

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : CompleteSpace β
h✝ : Nonempty β
F : Filter (α →ᵤ[𝔖] β)
hF : Cauchy F
this : F.NeBot
g : α → β
hg : ∀ x ∈ ⋃₀ 𝔖, Tendsto (fun x_1 ↦ (toFun 𝔖) x_1 x) F (𝓝 (g x))
⊢ ∀ i ∈ 𝔖,
    ∀ (i_1 : SetRel β β),
      i_1 ∈ 𝓤 β ∧ IsClosed[instTopologicalSpaceProd] i_1 →
        {g_1 | ∀ x ∈ i, ((toFun 𝔖) ((ofFun 𝔖) g) x, (toFun 𝔖) g_1 x) ∈ id i_1} ∈ F
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : ∃ a b, t₁ = {a} ∧ t₂ = {b} ∧ a * b = 1
hfg : (f * g).NeBot
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
obtain ⟨a, b, rfl, rfl, h⟩ := h

Goal state after:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
hfg : (f * g).NeBot
a b : α
h₁ : {a} ∈ f
h : a * b = 1
h₂ : {b} ∈ g
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
⊢ (∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1) → f * g = 1

Tactic:
rintro ⟨a, b, rfl, rfl, h⟩
    rw [pure_mul_pure, h, pure_one]

Goal state after: