awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V W : Set (β × β)
h : V ⊆ W
x : β
⊢ ball x V ⊆ ball x W

Tactic:
preimage_mono h

Premises used: UniformSpace.ball, Set.preimage_mono
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
x : β
V W : Set (β × β)
⊢ ball x (V ∩ W) = ball x V ∩ ball x W

Tactic:
preimage_inter

Premises used: Set.preimage_inter, UniformSpace.ball
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
x : β
V W : Set (β × β)
⊢ ball x (V ∩ W) ⊆ ball x V

Tactic:
ball_mono inter_subset_left x

Premises used: UniformSpace.ball_mono, Set.inter_subset_left
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
x : β
V W : Set (β × β)
⊢ ball x (V ∩ W) ⊆ ball x W

Tactic:
ball_mono inter_subset_right x

Premises used: UniformSpace.ball_mono, Set.inter_subset_right
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
ι : Sort u_1
x : β
V : ι → Set (β × β)
⊢ ball x (⋂ (i : ι), V i) = ⋂ (i : ι), ball x (V i)

Tactic:
preimage_iInter

Premises used: UniformSpace.ball, Set.preimage_iInter
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V : SetRel β β
inst : V.IsSymm
x y : β
⊢ x ∈ ball y V ↔ y ∈ ball x V

Tactic:
V.comm

Premises used: Set.Mem, setOf, UniformSpace.ball, Set.preimage, SetRel.comm
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V : SetRel β β
inst : V.IsSymm
x : β
h : ∀ (y : β), y ∈ ball x V ↔ Membership.mem (γ := Set β) {y : β | (y, x) ∈ V} y
⊢ ball x V = {y : β | (y, x) ∈ V}

Tactic:
ext y
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V : SetRel β β
inst : V.IsSymm
x y : β
h : x ∈ ball y V ↔ Membership.mem (γ := Set β) {y : β | (y, x) ∈ V} y
⊢ y ∈ ball x V ↔ Membership.mem (γ := Set β) {y : β | (y, x) ∈ V} y

Tactic:
rw [mem_ball_symmetry]

Premises used: UniformSpace.mem_ball_symmetry
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V : SetRel β β
inst : V.IsSymm
x y : β
⊢ x ∈ ball y V ↔ Membership.mem (γ := Set β) {y : β | (y, x) ∈ V} y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, UniformSpace.ball, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V : SetRel β β
inst : V.IsSymm
x y : β
⊢ x ∈ ball y V ↔ Membership.mem (γ := Set β) {y : β | (y, x) ∈ V} y

Tactic:
exact Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V W : SetRel β β
x y z : β
inst : V.IsSymm
hx : x ∈ ball z V
hy : y ∈ ball z W
⊢ z ∈ ball x V

Tactic:
rw [mem_ball_symmetry] at hx

Premises used: UniformSpace.mem_ball_symmetry
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V W : SetRel β β
x y z : β
inst : V.IsSymm
hx : x ∈ ball z V
hy : y ∈ ball z W
hx₁ : z ∈ ball x V
⊢ y ∈ ball z W

Tactic:
rw [mem_ball_symmetry] at hx

Premises used: UniformSpace.mem_ball_symmetry
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : 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:
⟨z, hx, hy⟩

Premises used: Set.Mem, setOf, SetRel.comp, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : 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:
exact ⟨z, hx, hy⟩
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V W M : SetRel β β
inst : W.IsSymm
p : β × β
obtain : ∀ (x y : β), (x, y) ∈ V ○ M ○ W ↔ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty
⊢ p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty

Tactic:
obtain ⟨x, y⟩ := p
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
V W M : SetRel β β
inst : W.IsSymm
x y : β
mp : (x, y) ∈ V ○ M ○ W → (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty
mpr : (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty → (x, y) ∈ V ○ M ○ W
⊢ (x, y) ∈ V ○ M ○ W ↔ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : 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
rwa rwa₁ rwa₂ rwa₃ : (x, y).2 ∈ ball (w, z).2 W
⊢ (w, z).2 ∈ ball (x, y).2 W

Tactic:
rwa [mem_ball_symmetry]

Premises used: UniformSpace.mem_ball_symmetry
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : 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
⊢ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty

Tactic:
exact ⟨(w, z), ⟨hpw, by rwa [mem_ball_symmetry]⟩, hwz⟩
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : 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 : (w, z).2 ∈ ball (x, y).2 W
⊢ (x, y).2 ∈ ball (w, z).2 W

Tactic:
rw [mem_ball_symmetry] at z_in

Premises used: UniformSpace.mem_ball_symmetry
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : 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:
⟨z, ⟨w, w_in, hwz⟩, z_in⟩

Premises used: Set.Mem, setOf, SetRel.comp, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : 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:
exact ⟨z, ⟨w, w_in, hwz⟩, z_in⟩
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
β : Type ub
U : SetRel β β
inst : U.IsSymm
s N : Set β
⊢ U.IsCover s N ↔ s ⊆ ⋃ y ∈ N, ball y U

Tactic:
simp [SetRel.IsCover, subset_def, ball, U.comm]

Premises used: Set.subset_def, UniformSpace.ball, SetRel.IsCover, SetRel.comm
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α

Tactic:
simp only [nhds_eq_comap_uniformity, mem_comap_prodMk]

Premises used: Filter.mem_comap_prodMk, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
rw : {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ map Prod.swap (𝓤 α)
⊢ s ∈ 𝓝 x ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ 𝓤 α

Tactic:
rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right]

Premises used: mem_nhds_uniformity_iff_right, uniformity_eq_symm
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
⊢ {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ map Prod.swap (𝓤 α)

Tactic:
simp only [mem_map, preimage_setOf_eq, Prod.snd_swap, Prod.fst_swap]

Premises used: Prod.fst_swap, Set.preimage_setOf_eq, Prod.snd_swap, Filter.mem_map
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
T : Set α
hx : x ∈ T
S : Set α
⊢ 𝓝[S] x = comap (Prod.mk x) (𝓤 α ⊓ 𝓟 (T ×ˢ S))

Tactic:
simp [nhdsWithin, nhds_eq_comap_uniformity, hx]

Premises used: nhdsWithin, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
S : Set α
⊢ 𝓝[S] x = comap (Prod.mk x) (𝓤 α ⊓ 𝓟 (SProd.sprod (α := Set α) univ S))

Tactic:
nhdsWithin_eq_comap_uniformity_of_mem (mem_univ _) S

Premises used: nhdsWithin_eq_comap_uniformity_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
simp_rw : (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
simp_rw₁ : (∀ x ∈ s, s ∈ comap (Prod.mk x) (𝓤 α)) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
simp_rw₂ : (∀ x ∈ s, ∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
⊢ IsOpen[inst.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap, ball]

Premises used: Filter.mem_comap, UniformSpace.ball, nhds_eq_comap_uniformity, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
rw : (comap (Prod.mk x) (𝓤 α)).HasBasis p fun (i : ι) ↦ ball x (s i)
⊢ (𝓝 x).HasBasis p fun (i : ι) ↦ ball x (s i)

Tactic:
rw [nhds_eq_comap_uniformity]

Premises used: nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
⊢ (comap (Prod.mk x) (𝓤 α)).HasBasis p fun (i : ι) ↦ ball x (s i)

Tactic:
h.comap (Prod.mk x)

Premises used: Prod.mk, UniformSpace.ball, Filter.HasBasis.comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
⊢ (comap (Prod.mk x) (𝓤 α)).HasBasis p fun (i : ι) ↦ ball x (s i)

Tactic:
exact h.comap (Prod.mk x)

Premises used: Prod.mk, Filter.HasBasis.comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
⊢ (comap Prod.swap (𝓤 α)).HasBasis p fun (i : ι) ↦ Prod.swap ⁻¹' s i

Tactic:
replace h := h.comap Prod.swap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
x : α
h : (comap Prod.swap (𝓤 α)).HasBasis p fun (i : ι) ↦ Prod.swap ⁻¹' s i
⊢ (𝓤 α).HasBasis p fun (i : ι) ↦ Prod.swap ⁻¹' s i

Tactic:
rw [comap_swap_uniformity] at h

Premises used: comap_swap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
x : α
h : (𝓤 α).HasBasis p fun (i : ι) ↦ Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun (i : ι) ↦ {y : α | (y, x) ∈ s i}

Tactic:
nhds_basis_uniformity' h

Premises used: Set.Mem, nhds_basis_uniformity', setOf, UniformSpace.ball, Set.preimage, Prod.swap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
x : α
h : (𝓤 α).HasBasis p fun (i : ι) ↦ Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun (i : ι) ↦ {y : α | (y, x) ∈ s i}

Tactic:
exact nhds_basis_uniformity' h

Premises used: nhds_basis_uniformity'
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
⊢ 𝓝 x = comap (fun (y : α) ↦ (y, x)) (𝓤 α)

Tactic:
(nhds_basis_uniformity (𝓤 α).basis_sets).eq_of_same_basis <| (𝓤 α).basis_sets.comap _

Premises used: uniformity, Filter.HasBasis.comap, Filter.basis_sets, nhds_basis_uniformity, Filter.HasBasis.eq_of_same_basis
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
rw : (∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
rw [nhds_eq_comap_uniformity, mem_comap]

Premises used: Filter.mem_comap, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
⊢ (∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
simp_rw [ball]

Premises used: UniformSpace.ball
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : SetRel α α
V_in : V ∈ 𝓤 α
rw : ∃ V_1 ∈ 𝓤 α, ball x V_1 ⊆ ball x V
⊢ ball x V ∈ 𝓝 x

Tactic:
rw [UniformSpace.mem_nhds_iff]

Premises used: UniformSpace.mem_nhds_iff
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : SetRel α α
V_in : V ∈ 𝓤 α
⊢ ∃ V_1 ∈ 𝓤 α, ball x V_1 ⊆ ball x V

Tactic:
⟨V, V_in, Subset.rfl⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : SetRel α α
V_in : V ∈ 𝓤 α
⊢ ∃ V_1 ∈ 𝓤 α, ball x V_1 ⊆ ball x V

Tactic:
exact ⟨V, V_in, Subset.rfl⟩
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
S : Set α
V : SetRel α α
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
rw : ∃ t ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S), Prod.mk x ⁻¹' t ⊆ ball x V
⊢ ball x V ∈ 𝓝[S] x

Tactic:
rw [nhdsWithin_eq_comap_uniformity_of_mem x_in, mem_comap]

Premises used: nhdsWithin_eq_comap_uniformity_of_mem, Filter.mem_comap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
S : Set α
V : SetRel α α
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
⊢ ∃ t ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S), Prod.mk x ⁻¹' t ⊆ ball x V

Tactic:
⟨V, V_in, Subset.rfl⟩

Premises used: Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
S : Set α
V : SetRel α α
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
⊢ ∃ t ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S), Prod.mk x ⁻¹' t ⊆ ball x V

Tactic:
exact ⟨V, V_in, Subset.rfl⟩
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
rw : (∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

Tactic:
rw [UniformSpace.mem_nhds_iff]

Premises used: UniformSpace.mem_nhds_iff
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
mp : (∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
mpr : (∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 α, ball x V ⊆ s
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
right : ball x (SetRel.symmetrize V) ⊆ s
⊢ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s

Tactic:
use SetRel.symmetrize V, symmetrize_mem_uniformity V_in, inferInstance

Premises used: SetRel.symmetrize, symmetrize_mem_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ball x (SetRel.symmetrize V) ⊆ s

Tactic:
Subset.trans (ball_mono SetRel.symmetrize_subset_self x) V_sub

Premises used: Set.Subset.trans, UniformSpace.ball_mono, SetRel.symmetrize_subset_self
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ball x (SetRel.symmetrize V) ⊆ s

Tactic:
exact Subset.trans (ball_mono SetRel.symmetrize_subset_self x) V_sub

Premises used: Set.Subset.trans, UniformSpace.ball_mono, SetRel.symmetrize_subset_self
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
left : SetRel.IsSymm V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
⟨V, V_in, V_sub⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
left : SetRel.IsSymm V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
exact ⟨V, V_in, V_sub⟩
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
t : Set α
⊢ t ∈ 𝓝 x ↔ ∃ (i : SetRel α α), (i ∈ 𝓤 α ∧ i.IsSymm) ∧ ball x i ⊆ t

Tactic:
simp [UniformSpace.mem_nhds_iff_symm, and_assoc]

Premises used: UniformSpace.mem_nhds_iff_symm, and_assoc
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure[inst.toTopologicalSpace] s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → SetRel.IsSymm V → (s ∩ ball x V).Nonempty

Tactic:
simp [mem_closure_iff_nhds_basis (hasBasis_nhds x), Set.Nonempty]

Premises used: UniformSpace.hasBasis_nhds, Set.Nonempty, mem_closure_iff_nhds_basis
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
x : α
⊢ x ∈ closure[inst.toTopologicalSpace] s ↔ ∀ {V : Set (α × α)}, V ∈ 𝓤 α → (ball x V ∩ s).Nonempty

Tactic:
simp [mem_closure_iff_nhds_basis' (nhds_basis_uniformity' (𝓤 α).basis_sets)]

Premises used: nhds_basis_uniformity', uniformity, mem_closure_iff_nhds_basis', Filter.basis_sets
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α
s : Set α
x : α
hx : x ∈ closure[inst.toTopologicalSpace] s
obtain : ∀ (y : α) (hxy : y ∈ ball x U) (hy : y ∈ s), x ∈ U.preimage s
⊢ x ∈ U.preimage s

Tactic:
obtain ⟨y, hxy, hy⟩ := mem_closure_iff_ball.mp hx hU

Premises used: UniformSpace.mem_closure_iff_ball, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α
s : Set α
x : α
hx : x ∈ closure[inst.toTopologicalSpace] s
y : α
hxy : y ∈ ball x U
hy : y ∈ s
⊢ x ∈ U.preimage s

Tactic:
⟨y, hy, hxy⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, SetRel.preimage
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α
s : Set α
x : α
hx : x ∈ closure[inst.toTopologicalSpace] s
y : α
hxy : y ∈ ball x U
hy : y ∈ s
⊢ x ∈ U.preimage s

Tactic:
exact ⟨y, hy, hxy⟩
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α
s : Set α
⊢ closure[inst.toTopologicalSpace] s ⊆ U.image s

Tactic:
closure_subset_preimage (symm_le_uniformity hU) s

Premises used: Set.Mem, setOf, symm_le_uniformity, Set.preimage, SetRel.image, Prod.swap, UniformSpace.closure_subset_preimage
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
⊢ 𝓝 x = (𝓤 α).lift' (ball x)

Tactic:
(nhds_basis_uniformity' (𝓤 α).basis_sets).eq_biInf

Premises used: nhds_basis_uniformity', uniformity, setOf, Filter.HasBasis.eq_biInf, Filter.basis_sets, Filter.lift', Filter.lift, Filter.principal
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
⊢ 𝓝 x = (𝓤 α).lift' fun (s : Set (α × α)) ↦ {y : α | (y, x) ∈ s}

Tactic:
(nhds_basis_uniformity (𝓤 α).basis_sets).eq_biInf

Premises used: Set.Mem, uniformity, setOf, Filter.HasBasis.eq_biInf, Filter.basis_sets, Filter.lift', Filter.lift, Filter.principal, nhds_basis_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : SetRel α α
h : s ∈ 𝓤 α
⊢ {y : α | (x, y) ∈ s} ∈ 𝓝 x

Tactic:
ball_mem_nhds x h

Premises used: UniformSpace.ball_mem_nhds, Set.Mem, setOf, UniformSpace.ball, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
y : α
s : SetRel α α
h : s ∈ 𝓤 α
⊢ {x : α | (x, y) ∈ s} ∈ 𝓝 y

Tactic:
mem_nhds_left _ (symm_le_uniformity h)

Premises used: Set.Mem, mem_nhds_left, setOf, symm_le_uniformity, Set.preimage, Prod.swap
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
a : α
U : Set α
h : U ∈ 𝓝 a
⊢ ∃ V ∈ 𝓝 a, ∃ t ∈ 𝓤 α, ∀ a' ∈ V, ball a' t ⊆ U

Tactic:
let ⟨t, ht, htU⟩ := comp_mem_uniformity_sets (mem_nhds_uniformity_iff_right.1 h)
  ⟨_, mem_nhds_left a ht, t, ht, fun a₁ h₁ a₂ h₂ => @htU (a, a₂) ⟨a₁, h₁, h₂⟩ rfl⟩

Premises used: mem_nhds_uniformity_iff_right, mem_nhds_left, uniformity, setOf, Membership.mem, Exists, nhds, Prod.mk, comp_mem_uniformity_sets, And, And.intro, Exists.intro, Iff.mp, _private.0.exists_mem_nhds_ball_subset_of_mem_nhds.match_1, rfl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
a : α
⊢ Tendsto (fun (a' : α) ↦ (a', a)) (𝓝 a) (𝓤 α)

Tactic:
fun _ =>
  mem_nhds_right a

Premises used: Set.Mem, setOf, Set.preimage, Filter.Tendsto, mem_nhds_right
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
a : α
⊢ Tendsto (fun (a' : α) ↦ (a, a')) (𝓝 a) (𝓤 α)

Tactic:
fun _ =>
  mem_nhds_left a

Premises used: Set.Mem, mem_nhds_left, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
rw : (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g (ball x s)
⊢ (𝓝 x).lift g = (𝓤 α).lift fun (s : SetRel α α) ↦ g (ball x s)

Tactic:
rw [nhds_eq_comap_uniformity, comap_lift_eq2 hg]

Premises used: Filter.comap_lift_eq2, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
simp_rw : (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g (Prod.mk x ⁻¹' s)
⊢ (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g (ball x s)

Tactic:
simp_rw [ball, Function.comp_def]

Premises used: UniformSpace.ball, Function.comp_def
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
rw : (𝓤 α).lift (g ∘ preimage fun (y : α) ↦ (y, x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g {y : α | (y, x) ∈ s}
⊢ (𝓝 x).lift g = (𝓤 α).lift fun (s : SetRel α α) ↦ g {y : α | (y, x) ∈ s}

Tactic:
rw [nhds_eq_comap_uniformity', comap_lift_eq2 hg]

Premises used: Filter.comap_lift_eq2, nhds_eq_comap_uniformity'
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
simp_rw :
  Eq.{ub + 1} (α := Filter β) ((𝓤 α).lift fun (x_1 : Set (α × α)) ↦ g ((fun (y : α) ↦ (y, x)) ⁻¹' x_1))
    ((𝓤 α).lift fun (s : SetRel α α) ↦ g {y : α | (y, x) ∈ s})
⊢ (𝓤 α).lift (g ∘ preimage fun (y : α) ↦ (y, x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g {y : α | (y, x) ∈ s}

Tactic:
simp_rw [Function.comp_def, preimage]

Premises used: Function.comp_def, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
a b : α
rw :
  Eq (α := Filter (α × α))
    ((𝓤 α).lift fun (s : Set (α × α)) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦ SProd.sprod (α := Set α) {y : α | (y, a) ∈ s} (ball b t))
    ((𝓤 α).lift fun (s : SetRel α α) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦
        SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t})
hg₁ : Monotone (β := Set α) fun (s : Set (α × α)) ↦ {y : α | (y, a) ∈ s}
hg₂ : Monotone (ball b)
⊢ 𝓝 a ×ˢ 𝓝 b =
    (𝓤 α).lift fun (s : SetRel α α) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦
        SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}

Tactic:
rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']

Premises used: Filter.prod_lift'_lift', nhds_eq_uniformity, nhds_eq_uniformity'
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ Eq (α := Filter (α × α))
    ((𝓤 α).lift fun (s : Set (α × α)) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦ SProd.sprod (α := Set α) {y : α | (y, a) ∈ s} (ball b t))
    ((𝓤 α).lift fun (s : SetRel α α) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦
        SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t})

Tactic:
rfl

Premises used: setOf, UniformSpace.ball, Set.preimage, rfl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ Monotone (β := Set α) fun (s : Set (α × α)) ↦ {y : α | (y, a) ∈ s}

Tactic:
monotone_preimage

Premises used: Set.Mem, setOf, Set.preimage, Set.monotone_preimage
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ Monotone (ball b)

Tactic:
monotone_preimage

Premises used: UniformSpace.ball, Set.monotone_preimage
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ Eq (α := Filter (α × α))
    ((𝓤 α).lift fun (s : Set (α × α)) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦ SProd.sprod (α := Set α) {y : α | (y, a) ∈ s} (ball b t))
    ((𝓤 α).lift fun (s : SetRel α α) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦
        SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t})

Tactic:
exacts [rfl, monotone_preimage, monotone_preimage]

Premises used: Set.monotone_preimage, rfl
-- Module: Mathlib.Topology.UniformSpace.Defs
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
U : ι → SetRel α α
h : (𝓤 α).HasBasis p U
s : Set α
h₁ :
  ∀ (x : α),
    Membership.mem (γ := Set α) (⋂ (i : ι), ⋂ (_ : p i), ⋃ x ∈ s, ball x (U i)) x ↔
      x ∈ closure[inst.toTopologicalSpace] s
⊢ ⋂ (i : ι), ⋂ (_ : p i), ⋃ x ∈ s, ball x (U i) = closure[inst.toTopologicalSpace] s

Tactic:
ext x