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

Goal state before:
pp: α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i j : ι
x : ↑(U i)
y : ↑(U j)
hxy : connectedComponent ↑x = connectedComponent ↑y
⊢ ∃ x ∈ U i, x ∈ U j

Tactic:
]

Goal state after:
α : Type u
β : Type v
ι✝ : Type u_1
X : ι✝ → Type u_2
inst✝ : TopologicalSpace α
s t u v : Set α
ι : Type u_3
U : ι → Set α
hclopen : ∀ (i : ι), IsClopen (U i)
hdisj : Pairwise (Disjoint on U)
hunion : ⋃ i, U i = univ
hconn : ∀ (i : ι), IsPreconnected (U i)
heq : ∀ {x : α} {i : ι} (hx : x ∈ U i), Subtype.val '' connectedComponent ⟨x, hx⟩ = connectedComponent x
x✝¹ x✝ : (i : ι) × ConnectedComponents ↑(U i)
i j : ι
x : ↑(U i)
y : ↑(U j)
hxy : connectedComponent ↑x = connectedComponent ↑y
⊢ ∃ x ∈ U i, x ∈ U j
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hs : IsOpen[inst✝¹] s
hne : s.Nonempty
h✝ : IsMeagre s
h : sᶜ ∈ residual X
⊢ ?m.17 ∈ residual X

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hs : IsOpen[inst✝¹] s
hne : s.Nonempty
h✝ : IsMeagre s
h : sᶜ ∈ residual X
⊢ ?m.17 ∈ residual X
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ x, f ↑x ⋯)

Tactic:
]

Goal state after:
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : (x : α) → x ∈ S → Set X
ho : ∀ (s : α) (H : s ∈ S), IsGδ (f s H)
hS : S.Countable
hd : ∀ (s : α) (H : s ∈ S), Dense (f s H)
⊢ Dense (⋂ x, f ↑x ⋯)
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (⋂ b, bif b then s else t)

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
hsc : Dense s
htc : Dense t
⊢ Dense (⋂ b, bif b then s else t)
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
i : ι
x : X
⊢ x ∈ ∅ᶜ

Tactic:
]

Goal state after:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
i : ι
x : X
⊢ x ∈ ∅ᶜ
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
⊢ x ∈ ⋃ i, interior (f i)

Tactic:
]

Goal state after:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
hgd : Dense (⋂ i, g i)
x : X
hxs : x ∈ s
hxg : ∀ (i : ι), x ∈ g i
⊢ x ∈ ⋃ i, interior (f i)
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
T : Set (Set X)
s : Set X
hs : IsGδ s
hd : Dense s
hc : T.Countable
hc' : ∀ t ∈ T, IsClosed[inst✝¹] t
hU : s ⊆ ⋃₀ T
⊢ s ⊆ ⋃₀ T

Tactic:
]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
T : Set (Set X)
s : Set X
hs : IsGδ s
hd : Dense s
hc : T.Countable
hc' : ∀ t ∈ T, IsClosed[inst✝¹] t
hU : s ⊆ ⋃₀ T
⊢ s ⊆ ⋃₀ T
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h.symm '' s) ↔ IsCompact s

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsCompact (⇑h.symm '' s) ↔ IsCompact s
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact (⇑h.symm '' s) ↔ IsSigmaCompact s

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsSigmaCompact (⇑h.symm '' s) ↔ IsSigmaCompact s
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsPreconnected s ↔ IsPreconnected s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsConnected s ↔ IsConnected s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this : connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
h : X ≃ₜ Y
x : X
hx : x ∈ s
this : connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
⊢ connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ cocompact Y = cocompact Y

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x : X
⊢ {h x}ᶜ = {h x}ᶜ

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ coclosedCompact Y = coclosedCompact Y

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
x : X
⊢ (map (⇑h.symm) (𝓝 (h x))).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ h x ∈ s ∧ IsConnected s) fun x ↦ ⇑h.symm '' x

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : LocallyConnectedSpace Y
h : X ≃ₜ Y
x : X
⊢ (map (⇑h.symm) (𝓝 (h x))).HasBasis (fun s ↦ IsOpen[inst✝] s ∧ h x ∈ s ∧ IsConnected s) fun x ↦ ⇑h.symm '' x
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ⇑(sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace]
    ⇑(sumArrowHomeomorphProdArrow.symm.trans (piCongrLeft finSumFinEquiv)).toEquiv
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ ∀ (x : Mˣ), ContinuousAt (fun u ↦ ↑u⁻¹) x

Tactic:
]

Goal state after:
M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ ∀ (x : Mˣ), ContinuousAt (fun u ↦ ↑u⁻¹) x
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
⊢ ∀ (s : Set X), IsClosed[inst✝³] s → IsClosed[inst✝²] (⇑f.symm ⁻¹' s)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
⊢ ∀ (s : Set X), IsClosed[inst✝³] s → IsClosed[inst✝²] (⇑f.symm ⁻¹' s)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
C : Set X
hC : IsClosed[inst✝³] C
hC' : IsClosed[inst✝²] (⇑f.symm ⁻¹' C)
⊢ IsClosed[inst✝²] (⇑f.symm ⁻¹' C)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous[inst✝³, inst✝²] ⇑f
C : Set X
hC : IsClosed[inst✝³] C
hC' : IsClosed[inst✝²] (⇑f.symm ⁻¹' C)
⊢ IsClosed[inst✝²] (⇑f.symm ⁻¹' C)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph ⇑e ↔ Continuous[inst✝¹, inst✝] ⇑e ∧ IsOpenMap ⇑e

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph ⇑e ↔ Continuous[inst✝¹, inst✝] ⇑e ∧ IsOpenMap ⇑e
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝¹] s

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsQuotientMap f ∧ Injective f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝¹] s
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
⊢ Continuous[inst✝³, inst✝²] f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous[inst✝³, inst✝²] f ∧ Bijective f

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
⊢ Continuous[inst✝³, inst✝²] f ∧ IsClosedMap f ∧ Bijective f ↔ Continuous[inst✝³, inst✝²] f ∧ Bijective f
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
hf : Continuous[inst✝³, inst✝²] f
⊢ Bijective f ↔ Bijective f

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.Constructions

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf : IsEmbedding ⇑f
⊢ IsEmbedding (⇑(embedProduct N) ∘ ⇑(map f))

Tactic:
exact hf.prodMap (opHomeomorph.isEmbedding.comp <| hf.comp opHomeomorph.symm.isEmbedding)
    |>.comp isEmbedding_embedProduct

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x y : α
⊢ y ∈ connectedComponent x ↔ y ∈ connectedComponent x

Tactic:
]

Goal state after:
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
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' v)ᶜ

Tactic:
]

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
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' v)ᶜ
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
⊢ f ⁻¹' {false} = f ⁻¹' {false}

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ (univ.Nonempty ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ) ↔
    univ.Nonempty ∧ ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ

Tactic:
]

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

Goal state before:
pp: X : Type u_2
inst✝ : UniformSpace X
⊢ (∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ 𝓟 SetRel.id) ↔ ∀ (s : Set (X × X)), s ∈ uniformity X ↔ s ∈ 𝓟 SetRel.id

Tactic:
]

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

Goal state before:
pp: X : Type u_1
u : UniformSpace X
inst✝ : DiscreteUniformity X
⊢ ⊥ = ⊥

Tactic:
]

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

Goal state before:
pp: X : Type u_2
inst✝ : UniformSpace X
⊢ inst✝ = ⊥ ↔ inst✝ = ⊥

Tactic:
]

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

Goal state before:
pp: α : Type ua
R : SetRel α α
f g : Filter α
inst✝ : R.IsSymm
⊢ R ∈ g ×ˢ f ↔ R ∈ g ×ˢ f

Tactic:
]

Goal state after:
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 : α
⊢ comap (Prod.mk x) u.uniformity = comap (Prod.mk x) u.uniformity

Tactic:
]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : U ∈ UniformSpace.uniformity
x : α
⊢ Prod.mk x ⁻¹' U ∈ comap (Prod.mk x) UniformSpace.uniformity

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
u : UniformSpace α
U : Set (α × α)
hU : U ∈ UniformSpace.uniformity
x : α
⊢ Prod.mk x ⁻¹' U ∈ comap (Prod.mk x) UniformSpace.uniformity
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
u : UniformSpace α
a : α
⊢ comap (Prod.mk a) u.toCore.uniformity = comap (Prod.mk a) UniformSpace.uniformity

Tactic:
]

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

Goal state before:
pp: α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity

Tactic:
]

Goal state after:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.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 : α
⊢ comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity

Tactic:
]

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

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
l : Filter β
f : β → α
⊢ l.NeBot ∧ map (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α ↔ l.NeBot ∧ map (fun p ↦ (f p.1, f p.2)) (l ×ˢ l) ≤ 𝓤 α

Tactic:
]

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

Goal state before:
pp: β : Type v
u v : UniformSpace β
F : Filter β
⊢ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β ↔ (F.NeBot ∧ F ×ˢ F ≤ 𝓤 β) ∧ F.NeBot ∧ F ×ˢ F ≤ 𝓤 β

Tactic:
]

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

Goal state before:
pp: β : Type v
ι : Sort u_1
inst✝ : Nonempty ι
u : ι → UniformSpace β
l : Filter β
⊢ (l.NeBot ∧ ∀ (i : ι), l ×ˢ l ≤ 𝓤 β) ↔ l.NeBot ∧ ∀ (x : ι), l ×ˢ l ≤ 𝓤 β

Tactic:
]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)

Tactic:
]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (comap Prod.swap (𝓤 α)).sets

Tactic:
]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (comap Prod.swap (𝓤 α)).sets
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f

Tactic:
]

Goal state after:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun s ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ ((𝓤 α).lift fun s ↦ f (s ○ s)) = (𝓤 α).lift fun s ↦ f (s ○ s)

pp: case hg
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone fun s ↦ s ○ s

pp: case hh
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone f

Tactic:
]

Goal state after:
case hg
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone fun s ↦ s ○ s

case hh
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ Monotone 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 ×ˢ atTop) (𝓤 α)
⊢ ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Tactic:
]

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 α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : Tendsto (Prod.map u u) atTop (𝓤 α)
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n

Tactic:
]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : Tendsto (Prod.map u u) atTop (𝓤 α)
f g : ℕ → ℕ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
V : SetRel β β
inst✝ : V.IsSymm
x y : β
⊢ x ∈ ball y V ↔ y ∈ {y | (y, x) ∈ V}

Tactic:
]

Goal state after:
β : Type ub
V : SetRel β β
inst✝ : V.IsSymm
x y : β
⊢ x ∈ ball y V ↔ y ∈ {y | (y, x) ∈ V}
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformlyOnFilter F f p ⊤ ↔ TendstoUniformlyOnFilter F f p ⊤

Tactic:
]

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
n : ℕ
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n

Tactic:
]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
V : ℕ → SetRel α α
hV : ∀ (n : ℕ), V n ∈ 𝓤 α
u : ℕ → α
hu : ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
n : ℕ
⊢ ∃ N, ∀ k ≥ N, ∀ l ≥ k, (u l, u k) ∈ V n
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
V W : SetRel β β
x y z : β
inst✝ : V.IsSymm
hx : z ∈ ball x V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W

Tactic:
]

Goal state after:
β : Type ub
V W : SetRel β β
x y z : β
inst✝ : V.IsSymm
hx : z ∈ ball x V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
⊢ TendstoUniformly F f p

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
⊢ TendstoUniformly F f p
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y z : β
hzy : (z, y) ∈ W
w : β
hpw : (x, w) ∈ V
hwz : (w, z) ∈ M
⊢ (x, y).2 ∈ ball (w, z).2 W

Tactic:
]

Goal state after:
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y z : β
hzy : (z, y) ∈ W
w : β
hpw : (x, w) ∈ V
hwz : (w, z) ∈ M
⊢ (x, y).2 ∈ ball (w, z).2 W
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : SetRel α α}, s ∈ 𝓤 α → ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun x ↦ U ○ x)^[n✝] U ⊆ t
⊢ U ⊆ s ∧ U ○ (fun x ↦ U ○ x)^[n✝] U ⊆ s

Tactic:
]

Goal state after:
case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : SetRel α α}, s ∈ 𝓤 α → ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun x ↦ U ○ x)^[n✝] U ⊆ t
⊢ U ⊆ s ∧ U ○ (fun x ↦ U ○ x)^[n✝] U ⊆ s
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V

Tactic:
]

Goal state after:
case mp
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∀ V ∈ 𝓤 α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: case mpr
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (x, y).2 ∈ ball (w, z).2 W
⊢ (x, y) ∈ V ○ M ○ W

Tactic:
]

Goal state after:
case mpr
β : Type ub
V W M : SetRel β β
inst✝ : W.IsSymm
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (x, y).2 ∈ ball (w, z).2 W
⊢ (x, y) ∈ V ○ M ○ W
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:
]

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