awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[≠] a

Tactic:
simp only [nhdsWithin, mem_inf_principal, mem_compl_iff, mem_singleton_iff, or_iff_not_imp_left,
    insert_def]

Premises used: Set.insert_def, nhdsWithin, Set.mem_singleton_iff, Classical.or_iff_not_imp_left, Filter.mem_inf_principal, Set.mem_compl_iff
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝[≠] a ⊔ 𝓝[{a}] a = 𝓝 a
rw₁ : 𝓝[{a}ᶜ ∪ {a}] a = 𝓝 a
rw₂ : 𝓝[univ] a = 𝓝 a
rw₃ rw₄ : 𝓝 a = 𝓝 a
⊢ 𝓝[≠] a ⊔ pure a = 𝓝 a

Tactic:
rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]

Premises used: nhdsWithin_singleton, nhdsWithin_univ, nhdsWithin_union, Set.compl_union_self
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝[≠] a ⊔ pure a = 𝓝 a
rw₁ rw₂ : 𝓝 a = 𝓝 a
⊢ pure a ⊔ 𝓝[≠] a = 𝓝 a

Tactic:
rw [← sup_comm, nhdsNE_sup_pure]

Premises used: sup_comm, nhdsNE_sup_pure
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ Tendsto f (𝓝[≠] a) (𝓝 (f a))

Tactic:
simp [ContinuousAt, -pure_sup_nhdsNE, ← pure_sup_nhdsNE a, tendsto_pure_nhds]

Premises used: ContinuousAt, tendsto_pure_nhds, pure_sup_nhdsNE
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
rw : u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)

Tactic:
rw [nhdsWithin_prod_eq]

Premises used: nhdsWithin_prod_eq
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b

Tactic:
prod_mem_prod hu hv

Premises used: Filter.prod_mem_prod
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b

Tactic:
exact prod_mem_prod hu hv

Premises used: Filter.prod_mem_prod
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
hst : s =ᶠ[𝓝 x] t
h : x ∈ interior s
⊢ 𝓝[s] x = 𝓝[t] x

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq] at hst

Premises used: nhdsWithin_eq_iff_eventuallyEq
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
hst : s =ᶠ[𝓝 x] t
h : x ∈ interior s
hst₁ : 𝓝[s] x = 𝓝[t] x
⊢ x ∈ interior s

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq] at hst

Premises used: nhdsWithin_eq_iff_eventuallyEq
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
hst : 𝓝[s] x = 𝓝[t] x
h : x ∈ interior s
⊢ x ∈ interior t

Tactic:
simpa [mem_interior_iff_mem_nhds, ← nhdsWithin_eq_nhds, hst] using h

Premises used: mem_interior_iff_mem_nhds, nhdsWithin_eq_nhds
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
hst : s =ᶠ[𝓝 x] t
⊢ x ∈ interior s ↔ x ∈ interior t

Tactic:
⟨fun h ↦ hst.mem_interior h, fun h ↦ hst.symm.mem_interior h⟩

Premises used: Filter.EventuallyEq.mem_interior, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[I.pi (α := X) s] x = ⨅ (i : ι), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))

Tactic:
simp only [nhdsWithin, nhds_pi, Filter.pi, comap_inf, comap_iInf, pi_def, comap_principal, ←
    iInf_principal_finite hI, ← iInf_inf_eq]

Premises used: nhdsWithin, nhds_pi, Filter.comap_iInf, Filter.comap_inf, Filter.iInf_principal_finite, Filter.pi, Filter.comap_principal, Set.pi_def, iInf_inf_eq
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
simp :
  Eq (α := Filter ((i : ι) → X i))
    ((⨅ (i : ι), comap (eval (β := X) i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval (β := X) i ⁻¹' s i))
    ((⨅ i ∈ I, comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun (x : (i : ι) → X i) ↦ x i) ⁻¹' s i)) ⊓
      ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)))
⊢ 𝓝[I.pi (α := X) s] x =
    (⨅ i ∈ I, comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝[s i] x i)) ⊓
      ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i))

Tactic:
simp only [nhdsWithin, nhds_pi, Filter.pi, pi_def, ← iInf_principal_finite hI, comap_inf,
    comap_principal]

Premises used: nhdsWithin, nhds_pi, Filter.comap_inf, Filter.iInf_principal_finite, Filter.pi, Filter.comap_principal, Set.pi_def
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
rw :
  Eq (α := Filter ((i : ι) → X i))
    (((⨅ i ∈ I, comap (eval (β := X) i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval (β := X) i ⁻¹' s i)) ⊓
      ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (eval (β := X) i) (𝓝 (x i)))
    ((⨅ i ∈ I, comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun (x : (i : ι) → X i) ↦ x i) ⁻¹' s i)) ⊓
      ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)))
⊢ Eq (α := Filter ((i : ι) → X i))
    ((⨅ (i : ι), comap (eval (β := X) i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval (β := X) i ⁻¹' s i))
    ((⨅ i ∈ I, comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun (x : (i : ι) → X i) ↦ x i) ⁻¹' s i)) ⊓
      ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)))

Tactic:
rw [iInf_split _ fun i => i ∈ I, inf_right_comm]

Premises used: Membership.mem, iInf_split, inf_right_comm
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ Eq (α := Filter ((i : ι) → X i))
    (((⨅ i ∈ I, comap (eval (β := X) i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval (β := X) i ⁻¹' s i)) ⊓
      ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (eval (β := X) i) (𝓝 (x i)))
    ((⨅ i ∈ I, comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun (x : (i : ι) → X i) ↦ x i) ⁻¹' s i)) ⊓
      ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)))

Tactic:
simp only [iInf_inf_eq]

Premises used: iInf_inf_eq
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : Finite ι
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[Set.pi (α := X) univ s] x = ⨅ (i : ι), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝[s i] x i)

Tactic:
simpa [nhdsWithin] using nhdsWithin_pi_eq finite_univ s x

Premises used: nhdsWithin, Set.finite_univ, nhdsWithin_pi_eq
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
I : Set ι
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[I.pi (α := X) s] x = ⊥ ↔ ∃ i ∈ I, 𝓝[s i] x i = ⊥

Tactic:
simp only [nhdsWithin, nhds_pi, pi_inf_principal_pi_eq_bot]

Premises used: nhdsWithin, nhds_pi, Filter.pi_inf_principal_pi_eq_bot
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
I : Set ι
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ (𝓝[I.pi (α := X) s] x).NeBot ↔ ∀ i ∈ I, (𝓝[s i] x i).NeBot

Tactic:
simp [neBot_iff, nhdsWithin_pi_eq_bot]

Premises used: Filter.neBot_iff, nhdsWithin_pi_eq_bot
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
ι : Type u_5
X : ι → Type u_6
inst_1 : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
x : (i : ι) → X i
inst_2 : ∀ (i : ι), (𝓝[s i] x i).NeBot
⊢ (𝓝[Set.pi (α := X) univ s] x).NeBot

Tactic:
simpa [nhdsWithin_pi_neBot]

Premises used: nhdsWithin_pi_neBot
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
ι : Type u_5
X : ι → Type u_6
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : Nonempty ι
inst_3 : (i : ι) → Preorder (X i)
x : (i : ι) → X i
inst_4 : ∀ (i : ι), (𝓝[<] x i).NeBot
⊢ (𝓝[<] x).NeBot

Tactic:
have : (𝓝[pi univ fun i ↦ Iio (x i)] x).NeBot := inferInstance
  this.mono <| nhdsWithin_mono _ fun _y hy ↦ lt_of_strongLT fun i ↦ hy i trivial

Premises used: trivial, Filter.NeBot.mono, lt_of_strongLT, inferInstance, nhdsWithin_mono
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
ι : Type u_5
X : ι → Type u_6
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : Nonempty ι
inst_3 : (i : ι) → Preorder (X i)
x : (i : ι) → X i
inst_4 : ∀ (i : ι), (𝓝[>] x i).NeBot
⊢ (𝓝[>] x).NeBot

Tactic:
Pi.instNeBotNhdsWithinIio (X := fun i ↦ (X i)ᵒᵈ) (x := fun i ↦ OrderDual.toDual (x i))

Premises used: Set.Ioi, setOf, Pi.instNeBotNhdsWithinIio, OrderDual
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
t : Set α
inst_1 : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
h₂ : Tendsto f (𝓝[s] a ⊓ 𝓟 t) l
h₃ : Tendsto g (𝓝[s] a ⊓ 𝓟 tᶜ) l
⊢ Tendsto (t.piecewise (β := fun (a : α) ↦ β) f g) (𝓝[s] a) l

Tactic:
apply Tendsto.piecewise

Premises used: Filter.Tendsto.piecewise
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
t : Set α
inst_1 : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
h₂ h₃ h₄ h₅ : Tendsto f (𝓝[s ∩ t] a) l
⊢ Tendsto f (𝓝[s] a ⊓ 𝓟 t) l

Tactic:
rwa [← nhdsWithin_inter']

Premises used: nhdsWithin_inter'
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
t : Set α
inst_1 : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ h₂ h₃ h₄ h₅ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto g (𝓝[s] a ⊓ 𝓟 tᶜ) l

Tactic:
rwa [← nhdsWithin_inter']

Premises used: nhdsWithin_inter'
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
p : α → Prop
inst_1 : DecidablePred p
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ {x : α | p x}] a) l
h₁ : Tendsto g (𝓝[s ∩ {x : α | ¬p x}] a) l
⊢ Tendsto (fun (x : α) ↦ if p x then f x else g x) (𝓝[s] a) l

Tactic:
h₀.piecewise_nhdsWithin h₁

Premises used: Set.Mem, setOf, Filter.Tendsto.piecewise_nhdsWithin, Set.piecewise
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
a : α
s : Set α
⊢ map f (𝓝[s] a) =
    ⨅ (t : Set α), ⨅ (_ : Membership.mem (γ := Set (Set α)) {t : Set α | a ∈ t ∧ IsOpen[inst] t} t), 𝓟 (f '' (t ∩ s))

Tactic:
((nhdsWithin_basis_open a s).map f).eq_biInf

Premises used: nhdsWithin_basis_open, Set.Mem, setOf, Filter.HasBasis.eq_biInf, Filter.HasBasis.map
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
a : α
s t : Set α
l : Filter β
hst : s ⊆ t
h : Tendsto f (𝓝[t] a) l
⊢ Tendsto f (𝓝[s] a) l

Tactic:
h.mono_left <| nhdsWithin_mono a hst

Premises used: Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : β → α
l : Filter β
a : α
s t : Set α
hst : s ⊆ t
h : Tendsto f l (𝓝[s] a)
⊢ Tendsto f l (𝓝[t] a)

Tactic:
h.mono_right (nhdsWithin_mono a hst)

Premises used: Filter.Tendsto.mono_right, nhdsWithin_mono
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
a : α
s : Set α
l : Filter β
h : Tendsto f (𝓝 a) l
⊢ Tendsto f (𝓝[s] a) l

Tactic:
h.mono_left inf_le_left

Premises used: Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ (i : Set α) (i_1 : a ∈ i ∧ IsOpen[inst] i), (∀ᶠ (x : β) in l, f x ∈ i) ∧ ∀ᶠ (x : β) in l, f x ∈ s

Tactic:
simp_rw [nhdsWithin_eq, tendsto_iInf, mem_setOf_eq, tendsto_principal, mem_inter_iff,
    eventually_and] at h

Premises used: Filter.eventually_and, Set.mem_inter_iff, Filter.tendsto_principal, Set.mem_setOf_eq, nhdsWithin_eq, Filter.tendsto_iInf
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α) (i_1 : a ∈ i ∧ IsOpen[inst] i), (∀ᶠ (x : β) in l, f x ∈ i) ∧ ∀ᶠ (x : β) in l, f x ∈ s
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
(h univ ⟨mem_univ a, isOpen_univ⟩).2

Premises used: Set.univ, isOpen_univ, And.right, And.intro, Set.mem_univ
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α) (i_1 : a ∈ i ∧ IsOpen[inst] i), (∀ᶠ (x : β) in l, f x ∈ i) ∧ ∀ᶠ (x : β) in l, f x ∈ s
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
exact (h univ ⟨mem_univ a, isOpen_univ⟩).2

Premises used: Set.univ, isOpen_univ, And.right, And.intro, Set.mem_univ
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ Tendsto f l (𝓝 a)

Tactic:
h.mono_right nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
x : α
hx : x ∈ s
⊢ (𝓝[s] x).NeBot

Tactic:
mem_closure_iff_nhdsWithin_neBot.1 <| subset_closure hx

Premises used: subset_closure, mem_closure_iff_nhdsWithin_neBot, Iff.mp
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsClosed[inst] s
x : α
hx : (𝓝[s] x).NeBot
⊢ x ∈ s

Tactic:
hs.closure_eq ▸ mem_closure_iff_nhdsWithin_neBot.2 hx

Premises used: Iff.mpr, IsClosed.closure_eq, Eq.rec, mem_closure_iff_nhdsWithin_neBot
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_5
f : ι → α
h : DenseRange f
x : α
⊢ (𝓝[range f] x).NeBot

Tactic:
mem_closure_iff_clusterPt.1 (h x)

Premises used: nhdsWithin, mem_closure_iff_clusterPt, ClusterPt, Iff.mp
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → TopologicalSpace (α i)
I : Set ι
s : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ x ∈ closure[Pi.topologicalSpace] (I.pi (α := α) s) ↔ ∀ i ∈ I, x i ∈ closure[inst i] (s i)

Tactic:
simp only [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_pi_neBot]

Premises used: mem_closure_iff_nhdsWithin_neBot, nhdsWithin_pi_neBot
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → TopologicalSpace (α i)
I : Set ι
s : (i : ι) → Set (α i)
⊢ closure[Pi.topologicalSpace] (I.pi (α := α) s) = I.pi (α := α) fun (i : ι) ↦ closure[inst i] (s i)

Tactic:
Set.ext fun _ => mem_closure_pi

Premises used: Set.ext, mem_closure_pi
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
α : ι → Type u_6
inst : (i : ι) → TopologicalSpace (α i)
s : (i : ι) → Set (α i)
I : Set ι
hs : ∀ i ∈ I, Dense (s i)
⊢ Dense (I.pi (α := α) s)

Tactic:
simp only [dense_iff_closure_eq, closure_pi_set, pi_congr rfl fun i hi => (hs i hi).closure_eq,
    pi_univ]

Premises used: dense_iff_closure_eq, Dense.closure_eq, Set.pi_congr, closure_pi_set, Set.pi_univ, rfl
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
rw : Dense (X := (i : ι) → Y i) (Set.pi (α := Y) univ fun (i : ι) ↦ range (f i))
⊢ DenseRange (Pi.map (α := X) (β := Y) f)

Tactic:
rw [DenseRange, Set.range_piMap]

Premises used: Set.range_piMap, DenseRange
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ Dense (X := (i : ι) → Y i) (Set.pi (α := Y) univ fun (i : ι) ↦ range (f i))

Tactic:
dense_pi Set.univ (fun i _ => hf i)

Premises used: Set.univ, dense_pi
-- Module: Mathlib.Topology.NhdsWithin
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ Dense (X := (i : ι) → Y i) (Set.pi (α := Y) univ fun (i : ι) ↦ range (f i))

Tactic:
exact dense_pi Set.univ (fun i _ => hf i)

Premises used: Set.univ, dense_pi
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
s : Set α
a : α
⊢ f =ᶠ[𝓝[s] a] g ↔ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → f x = g x

Tactic:
mem_inf_principal

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, Filter.mem_inf_principal
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
a : α
h₁ : f =ᶠ[𝓝[≠] a] g
h₂ : f a = g a
h : ∀ (a_1 : α), (Membership.mem (γ := Set α) {a}ᶜ a_1 → f a_1 = g a_1) → f a_1 = g a_1
⊢ f =ᶠ[𝓝 a] g

Tactic:
filter_upwards [eventually_nhdsWithin_iff.1 h₁]

Premises used: eventually_nhdsWithin_iff, Iff.mp
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
a : α
h₁ : f =ᶠ[𝓝[≠] a] g
h₂ : f a = g a
⊢ ∀ (a_1 : α), (Membership.mem (γ := Set α) {a}ᶜ a_1 → f a_1 = g a_1) → f a_1 = g a_1

Tactic:
grind
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
s : Set α
a : α
h : EqOn f g s
⊢ f =ᶠ[𝓝[s] a] g

Tactic:
mem_inf_of_right h

Premises used: Set.Mem, Filter.Eventually, Filter.EventuallyEq, Filter.mem_inf_of_right
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
s : Set α
a : α
h : EqOn f g s
⊢ f =ᶠ[𝓝[s] a] g

Tactic:
eventuallyEq_nhdsWithin_of_eqOn h

Premises used: eventuallyEq_nhdsWithin_of_eqOn
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
s : Set α
a : α
l : Filter β
hfg : ∀ x ∈ s, f x = g x
hf : Tendsto f (𝓝[s] a) l
⊢ Tendsto g (𝓝[s] a) l

Tactic:
(tendsto_congr' <| eventuallyEq_nhdsWithin_of_eqOn hfg).1 hf

Premises used: Iff.mp, Filter.tendsto_congr', eventuallyEq_nhdsWithin_of_eqOn
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : α
p : α → Prop
h : ∀ x ∈ s, p x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
mem_inf_of_right h

Premises used: Set.Mem, Filter.Eventually, Filter.mem_inf_of_right
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
a : α
l : Filter β
s : Set α
f : β → α
h1 : Tendsto f l (𝓝 a)
h2 : ∀ᶠ (x : β) in l, f x ∈ s
⊢ Tendsto f l (𝓝[s] a)

Tactic:
tendsto_inf.2 ⟨h1, tendsto_principal.2 h2⟩

Premises used: Iff.mpr, Filter.tendsto_inf, nhdsWithin, Filter.tendsto_principal, And.intro
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
a : α
l : Filter β
s : Set α
f : β → α
⊢ Tendsto f l (𝓝[s] a) ↔ Tendsto f l (𝓝 a) ∧ ∀ᶠ (n : β) in l, f n ∈ s

Tactic:
⟨fun h => ⟨tendsto_nhds_of_tendsto_nhdsWithin h, eventually_mem_of_tendsto_nhdsWithin h⟩, fun h =>
    tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ h.1 h.2⟩

Premises used: eventually_mem_of_tendsto_nhdsWithin, And.right, And.left, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, And.intro, tendsto_nhds_of_tendsto_nhdsWithin, Iff.intro
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
a : α
l : Filter β
f : β → α
⊢ Tendsto f l (𝓝[range f] a) ↔ Tendsto f l (𝓝 a)

Tactic:
⟨fun h => h.mono_right inf_le_left, fun h =>
    tendsto_inf.2 ⟨h, tendsto_principal.2 <| Eventually.of_forall mem_range_self⟩⟩

Premises used: Set.mem_range_self, Iff.mpr, Filter.tendsto_inf, Filter.Eventually.of_forall, Filter.tendsto_principal, And.intro, Iff.intro, inf_le_left, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
f g : α → β
a : α
h : f =ᶠ[𝓝[s] a] g
hmem : a ∈ s
⊢ f a = g a

Tactic:
h.self_of_nhdsWithin hmem

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

Tactic:
mem_nhdsWithin_of_mem_nhds h

Premises used: Filter.Eventually, mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
s : Set α
t : Set β
x : α
hst : MapsTo f s t
⊢ f ⁻¹' t ∈ 𝓝[s] x

Tactic:
Filter.mem_of_superset self_mem_nhdsWithin hst

Premises used: self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : { x : α // x ∈ s }
t u : Set { x : α // x ∈ s }
rw :
  t ∈ 𝓝 a ⊓ 𝓟 u ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₁ :
  t ∈ comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α)) ⊓ 𝓟 u ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₂ :
  Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α)) ⊓
        comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u)))
      t ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₃ :
  Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α) ⊓ 𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u)))
      t ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₄ rw₅ :
  Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
⊢ t ∈ 𝓝[u] a ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t

Tactic:
rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]

Premises used: nhdsWithin, Filter.comap_inf, nhds_subtype, Filter.principal_subtype
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : { x : α // x ∈ s }
t : Set { x : α // x ∈ s }
⊢ 𝓝[t] a = comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t] (↑a : α))

Tactic:
Filter.ext fun _ => mem_nhdsWithin_subtype

Premises used: Filter.ext, mem_nhdsWithin_subtype
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
⊢ 𝓝[s] a = map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a h))

Tactic:
(map_nhds_subtype_val ⟨a, h⟩).symm

Premises used: Subtype.mk, Eq.symm, map_nhds_subtype_val
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : (↑s : Type u_1)
t : Set (↑s : Type u_1)
rw : t ∈ 𝓝 a ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)
rw₁ rw₂ : t ∈ 𝓝 a ↔ t ∈ 𝓝 a
⊢ t ∈ 𝓝 a ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t ∈ 𝓝[s] (↑a : α)

Tactic:
rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]

Premises used: Subtype.val_injective, Filter.image_mem_map_iff, map_nhds_subtype_val