awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
z : α
s : Set α
⊢ z ∈ closure[inst] (s \ {z}) ↔ ∃ᶠ (x : α) in 𝓝[≠] z, x ∈ s

Tactic:
simp [mem_closure_iff_frequently, frequently_nhdsWithin_iff]

Premises used: mem_closure_iff_frequently, frequently_nhdsWithin_iff
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
⟨fun h => ?_, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩

Premises used: Iff.mpr, eventually_nhds_nhdsWithin, Filter.Eventually.filter_mono, Iff.intro, inf_le_left
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
p : α → Prop
refine : ∀ (h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x), ∀ᶠ (x : α) in 𝓝[s] a, p x
⊢ (∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
refine ⟨fun h => ?_, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x
simp : ∀ (h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x), ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
simp only [eventually_nhdsWithin_iff] at h ⊢

Premises used: eventually_nhdsWithin_iff
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x
⊢ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x

Tactic:
h.mono fun x hx hxs => (hx hxs).self_of_nhds hxs

Premises used: Filter.Eventually.self_of_nhds, Filter.Eventually.mono
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x
⊢ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x

Tactic:
exact h.mono fun x hx hxs => (hx hxs).self_of_nhds hxs

Premises used: Filter.Eventually.self_of_nhds, Filter.Eventually.mono
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
⊢ (∀ᶠ (x' : α) in 𝓝[s] x, t ∈ 𝓝[s] x') ↔ t ∈ 𝓝[s] x

Tactic:
eventually_eventually_nhdsWithin

Premises used: Set.Mem, Filter.Eventually, setOf, eventually_eventually_nhdsWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a = ⨅ (t : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {t : Set α | a ∈ t ∧ IsOpen[inst] t} t), 𝓟 (t ∩ s)

Tactic:
((nhds_basis_opens a).inf_principal s).eq_biInf

Premises used: Set.Mem, nhdsWithin, setOf, Filter.HasBasis.eq_biInf, Filter.HasBasis.inf_principal, nhds_basis_opens
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝 a ⊓ 𝓟 univ = 𝓝 a
rw₁ : 𝓝 a ⊓ ⊤ = 𝓝 a
rw₂ rw₃ : 𝓝 a = 𝓝 a
⊢ 𝓝[univ] a = 𝓝 a

Tactic:
rw [nhdsWithin, principal_univ, inf_top_eq]

Premises used: nhdsWithin, inf_top_eq, Filter.principal_univ
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_5
p : ι → Prop
s : ι → Set α
a : α
h : (𝓝 a).HasBasis p s
t : Set α
⊢ (𝓝[t] a).HasBasis p fun (i : ι) ↦ s i ∩ t

Tactic:
h.inf_principal t

Premises used: nhdsWithin, Filter.HasBasis.inf_principal
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
t : Set α
⊢ (𝓝[t] a).HasBasis (fun (u : Set α) ↦ a ∈ u ∧ IsOpen[inst] u) fun (u : Set α) ↦ u ∩ t

Tactic:
nhdsWithin_hasBasis (nhds_basis_opens a) t

Premises used: nhdsWithin_hasBasis, nhds_basis_opens
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set α
a : α
s : Set α
⊢ t ∈ 𝓝[s] a ↔ ∃ (u : Set α), IsOpen[inst] u ∧ a ∈ u ∧ u ∩ s ⊆ t

Tactic:
simpa only [and_assoc, and_left_comm] using (nhdsWithin_basis_open a s).mem_iff

Premises used: nhdsWithin_basis_open, Filter.HasBasis.mem_iff, and_left_comm, and_assoc
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set α
a : α
s : Set α
⊢ t ∈ 𝓝[s] a ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t

Tactic:
(nhdsWithin_hasBasis (𝓝 a).basis_sets s).mem_iff

Premises used: Filter.HasBasis.mem_iff, nhds, Filter.basis_sets, nhdsWithin_hasBasis
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s : Set α
hs : s ∈ 𝓝 x
t : Set α
⊢ s \ t ∈ 𝓝[tᶜ] x

Tactic:
diff_mem_inf_principal_compl hs t

Premises used: Set.Mem, Filter.diff_mem_inf_principal_compl
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
rw : s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ
⊢ s \ t' ∈ 𝓝[t \ t'] x

Tactic:
rw [nhdsWithin, diff_eq, diff_eq, ← inf_principal, ← inf_assoc]

Premises used: Filter.inf_principal, nhdsWithin, Set.diff_eq, inf_assoc
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ

Tactic:
inter_mem_inf hs (mem_principal_self _)

Premises used: Filter.mem_principal_self, Filter.inter_mem_inf, Set.Mem
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ

Tactic:
exact inter_mem_inf hs (mem_principal_self _)

Premises used: Filter.mem_principal_self, Filter.inter_mem_inf
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
rcases : ∀ (w : Set α) (Hw : w ∈ 𝓝 a) (hw : w ∩ s ⊆ t), t ∈ 𝓝 a
⊢ t ∈ 𝓝 a

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩

Premises used: Iff.mp, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
w : Set α
Hw : w ∈ 𝓝 a
hw : w ∩ s ⊆ t
⊢ t ∈ 𝓝 a

Tactic:
(𝓝 a).sets_of_superset ((𝓝 a).inter_sets Hw h1) hw

Premises used: nhds, Filter.inter_sets, Filter.sets_of_superset
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
w : Set α
Hw : w ∈ 𝓝 a
hw : w ∩ s ⊆ t
⊢ t ∈ 𝓝 a

Tactic:
exact (𝓝 a).sets_of_superset ((𝓝 a).inter_sets Hw h1) hw

Premises used: nhds, Filter.inter_sets, Filter.sets_of_superset
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
x : α
⊢ t ∈ 𝓝[s] x ↔ ∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t

Tactic:
eventually_inf_principal

Premises used: Filter.eventually_inf_principal, Set.Mem, Filter.Eventually, setOf
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
x : α
simp_rw : (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ s =ᶠ[𝓝 x] s ∩ t
simp_rw₁ : (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ ∀ᶠ (x : α) in 𝓝 x, x ∈ s ↔ x ∈ s ∩ t
simp_rw₂ : (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ ∀ᶠ (x : α) in 𝓝 x, x ∈ s ↔ x ∈ s ∧ x ∈ t
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t

Tactic:
simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]

Premises used: Set.mem_inter_iff, iff_self_and, Filter.eventuallyEq_set, mem_nhdsWithin_iff_eventually
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
x : α
⊢ s ∩ t =ᶠ[𝓝 x] s ∩ t ∩ t

Tactic:
simp [inter_assoc]

Premises used: Set.inter_assoc
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
x : α
⊢ s ∩ t =ᶠ[𝓝 x] s ∩ t ∩ s

Tactic:
simp [inter_comm s t, inter_assoc]

Premises used: Set.inter_comm, Set.inter_assoc
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
x : α
⊢ 𝓝[s] x = 𝓝[t] x ↔ s =ᶠ[𝓝 x] t

Tactic:
set_eventuallyEq_iff_inf_principal.symm

Premises used: nhdsWithin, Filter.set_eventuallyEq_iff_inf_principal, Iff.symm
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
x : α
⊢ 𝓝[s] x ≤ 𝓝[t] x ↔ t ∈ 𝓝[s] x

Tactic:
set_eventuallyLE_iff_inf_principal_le.symm.trans set_eventuallyLE_iff_mem_inf_principal

Premises used: Set.Mem, Filter.set_eventuallyLE_iff_inf_principal_le, Filter.set_eventuallyLE_iff_mem_inf_principal, Iff.trans, Iff.symm
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
hs : s ∈ 𝓝 (X a)
⊢ a ∈ t

Tactic:
h
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
hs : s ∈ 𝓝 (X a)
lift : ∀ (a : { x : α // x ∈ t }) (hs : s ∈ 𝓝 (X (↑a : α))), X ⁻¹' s ∈ 𝓝[t] (↑a : α)
⊢ X ⁻¹' s ∈ 𝓝[t] a

Tactic:
lift a to t using h
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : { x : α // x ∈ t }
hs : s ∈ 𝓝 (X (↑a : α))
⊢ (fun (x : (↑t : Type u_1)) ↦ X (↑x : α)) ⁻¹' s ∈ 𝓝 a

Tactic:
replace hs : (fun x : t => X x) ⁻¹' s ∈ 𝓝 a := preimage_nhds_coinduced hs
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : { x : α // x ∈ t }
hs : (fun (x : (↑t : Type u_1)) ↦ X (↑x : α)) ⁻¹' s ∈ 𝓝 a
rwa : X ⁻¹' s ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (𝓝 a)
rwa₁ rwa₂ rwa₃ rwa₄ : Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' X ⁻¹' s ∈ 𝓝 a
⊢ X ⁻¹' s ∈ 𝓝[t] (↑a : α)

Tactic:
rwa [← map_nhds_subtype_val, mem_map]

Premises used: Filter.mem_map, map_nhds_subtype_val
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
a : α
h : s ∈ 𝓝 a
⊢ s ∈ 𝓝[t] a

Tactic:
mem_inf_of_left h

Premises used: Set.Mem, Filter.mem_inf_of_left
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ s ∈ 𝓝[s] a

Tactic:
mem_inf_of_right (mem_principal_self s)

Premises used: Filter.mem_principal_self, Set.Mem, Filter.mem_inf_of_right
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ ∀ᶠ (x : α) in 𝓝[s] a, x ∈ s

Tactic:
self_mem_nhdsWithin

Premises used: Set.Mem, Filter.Eventually, setOf, self_mem_nhdsWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
a : α
h : t ∈ 𝓝 a
⊢ s ∩ t ∈ 𝓝[s] a

Tactic:
inter_mem self_mem_nhdsWithin (mem_inf_of_left h)

Premises used: Filter.inter_mem, Filter.mem_inf_of_left, self_mem_nhdsWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
ha : a ∈ s
⊢ pure a ≤ 𝓝[s] a

Tactic:
le_inf (pure_le_nhds a) (le_principal_iff.2 ha)

Premises used: Iff.mpr, Filter.le_principal_iff, Set.Mem, pure_le_nhds, le_inf
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
ha : a ∈ s
ht : t ∈ 𝓝[s] a
⊢ a ∈ t

Tactic:
pure_le_nhdsWithin ha ht

Premises used: Set.Mem, setOf, pure_le_nhdsWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
p : α → Prop
s : Set α
x : α
h : ∀ᶠ (y : α) in 𝓝[s] x, p y
hx : x ∈ s
⊢ p x

Tactic:
mem_of_mem_nhdsWithin hx h

Premises used: Set.Mem, mem_of_mem_nhdsWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
l : Filter β
s : Set α
a : α
ha : a ∈ s
⊢ Tendsto (fun (x : β) ↦ a) l (𝓝[s] a)

Tactic:
tendsto_const_pure.mono_right <| pure_le_nhdsWithin ha

Premises used: pure_le_nhdsWithin, Filter.Tendsto.mono_right, Filter.tendsto_const_pure
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ 𝓝[s] a = 𝓝[s ∩ t] a

Tactic:
le_antisymm (le_inf inf_le_left (le_principal_iff.mpr (inter_mem self_mem_nhdsWithin h)))
    (inf_le_inf_left _ (principal_mono.mpr Set.inter_subset_left))

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.principal_mono, Filter.inter_mem, inf_le_inf_left, Set.inter_subset_left, le_inf, le_antisymm, self_mem_nhdsWithin, inf_le_left
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝 a
⊢ 𝓝[s] a = 𝓝[s ∩ t] a

Tactic:
nhdsWithin_restrict'' s <| mem_inf_of_left h

Premises used: nhdsWithin_restrict'', Filter.mem_inf_of_left
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h₀ : a ∈ t
h₁ : IsOpen[inst] t
⊢ 𝓝[s] a = 𝓝[s ∩ t] a

Tactic:
nhdsWithin_restrict' s (IsOpen.mem_nhds h₁ h₀)

Premises used: nhdsWithin_restrict', IsOpen.mem_nhds
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a

Tactic:
nhdsWithin_le_iff.mpr h

Premises used: Iff.mpr, nhdsWithin_le_iff
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
rw : 𝓝[s] a ≤ 𝓝[univ] a
⊢ 𝓝[s] a ≤ 𝓝 a

Tactic:
rw [← nhdsWithin_univ]

Premises used: nhdsWithin_univ
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
h : univ ∈ 𝓝[s] a
⊢ 𝓝[s] a ≤ 𝓝[univ] a

Tactic:
apply nhdsWithin_le_of_mem

Premises used: nhdsWithin_le_of_mem
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ univ ∈ 𝓝[s] a

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ univ ∈ 𝓝[s] a

Tactic:
exact univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
rw : 𝓝[t ∩ s] a = 𝓝[u] a
rw₁ : 𝓝[t ∩ s] a = 𝓝[u ∩ s] a
rw₂ rw₃ : 𝓝[u ∩ s] a = 𝓝[u ∩ s] a
⊢ 𝓝[t] a = 𝓝[u] a

Tactic:
rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]

Premises used: nhdsWithin_restrict'
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen[inst] s
h₂ : t ∩ s = u ∩ s
rw : 𝓝[t ∩ s] a = 𝓝[u] a
rw₁ : 𝓝[t ∩ s] a = 𝓝[u ∩ s] a
rw₂ rw₃ : 𝓝[u ∩ s] a = 𝓝[u ∩ s] a
⊢ 𝓝[t] a = 𝓝[u] a

Tactic:
rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]

Premises used: nhdsWithin_restrict
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a = 𝓝 a ↔ s ∈ 𝓝 a

Tactic:
inf_eq_left.trans le_principal_iff

Premises used: Filter.le_principal_iff, nhdsWithin, inf_eq_left, Iff.trans
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
h : IsOpen[inst] s
ha : a ∈ s
⊢ 𝓝[s] a = 𝓝 a

Tactic:
nhdsWithin_eq_nhds.2 <| h.mem_nhds ha

Premises used: Iff.mpr, nhdsWithin_eq_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen[inst] t
hs : s ∈ 𝓝 (X a)
rw : X ⁻¹' s ∈ 𝓝[t] a
⊢ X ⁻¹' s ∈ 𝓝 a

Tactic:
rw [← ht.nhdsWithin_eq h]

Premises used: IsOpen.nhdsWithin_eq
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen[inst] t
hs : s ∈ 𝓝 (X a)
⊢ X ⁻¹' s ∈ 𝓝[t] a

Tactic:
preimage_nhdsWithin_coinduced' h hs

Premises used: preimage_nhdsWithin_coinduced'
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen[inst] t
hs : s ∈ 𝓝 (X a)
⊢ X ⁻¹' s ∈ 𝓝[t] a

Tactic:
exact preimage_nhdsWithin_coinduced' h hs

Premises used: preimage_nhdsWithin_coinduced'
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝 a ⊓ 𝓟 ∅ = ⊥
rw₁ : 𝓝 a ⊓ ⊥ = ⊥
rw₂ rw₃ : Eq.{u_1 + 1} (α := Filter α) ⊥ ⊥
⊢ 𝓝[∅] a = ⊥

Tactic:
rw [nhdsWithin, principal_empty, inf_bot_eq]

Premises used: nhdsWithin, Filter.principal_empty, inf_bot_eq
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
rw : 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ (𝓟 s ⊔ 𝓟 t)
rw₁ rw₂ : 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 (s ∪ t)
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t

Tactic:
rw [← inf_sup_left, sup_principal]

Premises used: Filter.sup_principal, inf_sup_left
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
b : α
I₁ I₂ : Set α
hI : univ = I₁ ∪ I₂
rw : 𝓝[univ] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
rw₁ : 𝓝[I₁ ∪ I₂] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
rw₂ rw₃ : 𝓝[I₁] b ⊔ 𝓝[I₂] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
⊢ 𝓝 b = 𝓝[I₁] b ⊔ 𝓝[I₂] b

Tactic:
rw [← nhdsWithin_univ b, hI, nhdsWithin_union]

Premises used: nhdsWithin_univ, nhdsWithin_union
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a b c d : Set α
x : α
h : a ∈ 𝓝[b] x
h' : c ∈ 𝓝[d] x
⊢ a ∩ c ∈ 𝓝[b ∩ d] x

Tactic:
inter_mem (nhdsWithin_mono _ inter_subset_left h) (nhdsWithin_mono _ inter_subset_right h')

Premises used: Filter.inter_mem, Set.inter_subset_left, nhdsWithin_mono, Set.inter_subset_right
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
rw : L ∪ R ∈ 𝓝[I₁] b ⊔ 𝓝[I₂] b
⊢ L ∪ R ∈ 𝓝 b

Tactic:
rw [← nhdsWithin_univ b, h, nhdsWithin_union]

Premises used: nhdsWithin_univ, nhdsWithin_union
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ⊆ L ∪ R

Tactic:
simp
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ R ⊆ L ∪ R

Tactic:
simp
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ∪ R ∈ 𝓝[I₁] b ⊔ 𝓝[I₂] b

Tactic:
exact ⟨mem_of_superset hL (by simp), mem_of_superset hR (by simp)⟩
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
x : α
rw : 𝓝[Iio x ∪ Ioi x] x = 𝓝[<] x ⊔ 𝓝[>] x
rw₁ rw₂ : 𝓝[<] x ⊔ 𝓝[>] x = 𝓝[<] x ⊔ 𝓝[>] x
⊢ 𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x

Tactic:
rw [← Iio_union_Ioi, nhdsWithin_union]

Premises used: Set.Iio_union_Ioi, nhdsWithin_union
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
b : α
L : Set α
hL : L ∈ 𝓝[≤] b
R : Set α
hR : R ∈ 𝓝[≥] b
⊢ L ∩ Iic b ∪ R ∩ Ici b ∈ 𝓝 b

Tactic:
union_mem_nhds_of_mem_nhdsWithin Iic_union_Ici.symm
    (inter_mem hL self_mem_nhdsWithin) (inter_mem hR self_mem_nhdsWithin)

Premises used: Filter.inter_mem, union_mem_nhds_of_mem_nhdsWithin, Set.Iic_union_Ici, self_mem_nhdsWithin, Eq.symm
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_5
I : Set ι
s : ι → Set α
a : α
⊢ 𝓝[⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), s i] a =
    ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), 𝓝[s i] a

Tactic:
simp
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_5
I : Set ι
s : ι → Set α
a : α
a_1 : ι
s_1 : Set ι
h : a_1 ∉ s_1
hs : s_1.Finite
hT : 𝓝[⋃ i ∈ s_1, s i] a = ⨆ i ∈ s_1, 𝓝[s i] a
⊢ 𝓝[⋃ i ∈ insert a_1 s_1, s i] a = ⨆ i ∈ insert a_1 s_1, 𝓝[s i] a

Tactic:
simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]

Premises used: iSup_insert, Set.biUnion_insert, nhdsWithin_union
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_5
I : Set ι
hI : I.Finite
s : ι → Set α
a : α
empty :
  𝓝[⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), s i] a =
    ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), 𝓝[s i] a
insert :
  ∀ {a_1 : ι} {s_1 : Set ι},
    a_1 ∉ s_1 →
      s_1.Finite →
        ∀ (hT : 𝓝[⋃ i ∈ s_1, s i] a = ⨆ i ∈ s_1, 𝓝[s i] a),
          𝓝[⋃ i ∈ Insert.insert a_1 s_1, s i] a = ⨆ i ∈ Insert.insert a_1 s_1, 𝓝[s i] a
⊢ 𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a

Tactic:
induction I, hI using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hT => simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]

Premises used: iSup_insert, Set.biUnion_insert, Insert.insert, nhdsWithin_union
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Set α)
hS : S.Finite
a : α
rw : 𝓝[⋃ i ∈ S, i] a = ⨆ s ∈ S, 𝓝[s] a
rw₁ rw₂ : Eq.{u_1 + 1} (α := Filter α) (⨆ i ∈ S, 𝓝[i] a) (⨆ s ∈ S, 𝓝[s] a)
⊢ 𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a

Tactic:
rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]

Premises used: nhdsWithin_biUnion, Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_5
inst_1 : Finite ι
s : ι → Set α
a : α
rw : 𝓝[⋃₀ range s] a = ⨆ (i : ι), 𝓝[s i] a
rw₁ : Eq.{u_1 + 1} (α := Filter α) (⨆ s_1 ∈ range s, 𝓝[s_1] a) (⨆ (i : ι), 𝓝[s i] a)
rw₂ rw₃ : Eq.{u_1 + 1} (α := Filter α) (⨆ (i : ι), 𝓝[s i] a) (⨆ (i : ι), 𝓝[s i] a)
⊢ 𝓝[⋃ (i : ι), s i] a = ⨆ (i : ι), 𝓝[s i] a

Tactic:
rw [← sUnion_range, nhdsWithin_sUnion (finite_range s), iSup_range]

Premises used: Set.sUnion_range, nhdsWithin_sUnion, iSup_range, Set.finite_range
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
rw : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t)
rw₁ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t))
rw₂ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 (s ∩ t))
rw₃ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓝 a ⊓ 𝓟 (s ∩ t)
rw₄ rw₅ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 (s ∩ t)
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)

Tactic:
rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]

Premises used: Filter.inf_principal, inf_assoc, inf_idem, inf_left_comm
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
rw : 𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t
rw₁ rw₂ : 𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t) = 𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t)
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t

Tactic:
rw [← inf_principal, inf_assoc]

Premises used: Filter.inf_principal, inf_assoc
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
rw : 𝓝[t] a ≤ 𝓝[s] a
⊢ 𝓝[s ∩ t] a = 𝓝[t] a

Tactic:
rw [nhdsWithin_inter, inf_eq_right]

Premises used: nhdsWithin_inter, inf_eq_right
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a

Tactic:
nhdsWithin_le_of_mem h

Premises used: nhdsWithin_le_of_mem
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[t] a ≤ 𝓝[s] a

Tactic:
exact nhdsWithin_le_of_mem h

Premises used: nhdsWithin_le_of_mem
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
rw : 𝓝[t ∩ s] a = 𝓝[s] a
rw₁ rw₂ : 𝓝[s] a = 𝓝[s] a
⊢ 𝓝[s ∩ t] a = 𝓝[s] a

Tactic:
rw [inter_comm, nhdsWithin_inter_of_mem h]

Premises used: nhdsWithin_inter_of_mem, Set.inter_comm
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝 a ⊓ 𝓟 {a} = pure a
rw₁ : 𝓝 a ⊓ pure a = pure a
rw₂ rw₃ : Eq (α := Filter α) (pure a) (pure a)
⊢ 𝓝[{a}] a = pure a

Tactic:
rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]

Premises used: Iff.mpr, pure_le_nhds, nhdsWithin, Filter.principal_singleton, inf_eq_right
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
rw : 𝓝[{a} ∪ s] a = pure a ⊔ 𝓝[s] a
rw₁ : 𝓝[{a}] a ⊔ 𝓝[s] a = pure a ⊔ 𝓝[s] a
rw₂ rw₃ : pure a ⊔ 𝓝[s] a = pure a ⊔ 𝓝[s] a
⊢ 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a

Tactic:
rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]

Premises used: nhdsWithin_singleton, Set.singleton_union, nhdsWithin_union
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
⊢ t ∈ 𝓝[insert a s] a ↔ a ∈ t ∧ t ∈ 𝓝[s] a

Tactic:
simp
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ insert a t ∈ 𝓝[insert a s] a

Tactic:
simp [mem_of_superset h]

Premises used: Filter.mem_of_superset