awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ (nhdsKer s) = 𝓝ˢ s

Tactic:
le_antisymm ((hasBasis_nhdsSet _).ge_iff.2 ?_) (nhdsSet_mono subset_nhdsKer)

Premises used: Iff.mpr, subset_nhdsKer, nhdsSet_mono, hasBasis_nhdsSet, Filter.HasBasis.ge_iff, le_antisymm
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
refine : ∀ (i' : Set X), IsOpen[inst] i' ∧ s ⊆ i' → i' ∈ 𝓝ˢ (nhdsKer s)
⊢ 𝓝ˢ (nhdsKer s) = 𝓝ˢ s

Tactic:
refine le_antisymm ((hasBasis_nhdsSet _).ge_iff.2 ?_) (nhdsSet_mono subset_nhdsKer)

Premises used: Iff.mpr, subset_nhdsKer, nhdsSet_mono, hasBasis_nhdsSet, Filter.HasBasis.ge_iff, le_antisymm
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ ∀ (i' : Set X), IsOpen[inst] i' ∧ s ⊆ i' → i' ∈ 𝓝ˢ (nhdsKer s)

Tactic:
fun U ⟨hUo, hsU⟩ ↦ hUo.mem_nhdsSet.2 <| hUo.nhdsKer_subset.2 hsU

Premises used: Iff.mpr, IsOpen.nhdsKer_subset, Membership.mem, _private.0.nhdsSet_nhdsKer.match_1, nhdsKer, nhdsSet, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ ∀ (i' : Set X), IsOpen[inst] i' ∧ s ⊆ i' → i' ∈ 𝓝ˢ (nhdsKer s)

Tactic:
exact fun U ⟨hUo, hsU⟩ ↦ hUo.mem_nhdsSet.2 <| hUo.nhdsKer_subset.2 hsU
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ nhdsKer (nhdsKer s) = nhdsKer s

Tactic:
simp only [nhdsKer_eq_nhdsKer_iff_nhdsSet, nhdsSet_nhdsKer]

Premises used: nhdsKer_eq_nhdsKer_iff_nhdsSet, nhdsSet_nhdsKer
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
simp_rw : (𝓝 (x, y)).ker = (𝓝 x).ker ×ˢ (𝓝 y).ker
simp_rw₁ : (𝓝 x ×ˢ 𝓝 y).ker = (𝓝 x).ker ×ˢ (𝓝 y).ker
⊢ nhdsKer {(x, y)} = SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {x}) (nhdsKer {y})

Tactic:
simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_prod_eq, ker_prod]

Premises used: nhdsKer_singleton_eq_ker_nhds, Filter.ker_prod, nhds_prod_eq
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
rw : ⋃ i ∈ s ×ˢ t, nhdsKer {i}
| nhdsKer (s ×ˢ t)

Tactic:
rw [← biUnion_of_singleton (s ×ˢ t), nhdsKer_biUnion]

Premises used: SProd.sprod, Set.biUnion_of_singleton, nhdsKer_biUnion
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
conv_lhs : nhdsKer (s ×ˢ t) = ⋃ p ∈ s ×ˢ t, nhdsKer {p}
conv_lhs₁ : Eq (α := Set (X × Y)) (⋃ i ∈ s ×ˢ t, nhdsKer {i}) (⋃ p ∈ s ×ˢ t, nhdsKer {p})
⊢ nhdsKer (s ×ˢ t) = ⋃ p ∈ s ×ˢ t, nhdsKer {p}

Tactic:
conv_lhs => rw [← biUnion_of_singleton (s ×ˢ t), nhdsKer_biUnion]

Premises used: SProd.sprod, Set.biUnion_of_singleton, nhdsKer_biUnion
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
h :
  ∀ (x : X) (y : Y),
    (x, y) ∈ s ×ˢ t → nhdsKer {(x, y)} = SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {(x, y).1}) (nhdsKer {(x, y).2})
⊢ Eq (α := Set (X × Y)) (⋃ p ∈ s ×ˢ t, nhdsKer {p})
    (⋃ p ∈ s ×ˢ t, SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {p.1}) (nhdsKer {p.2}))

Tactic:
congr! with ⟨x, y⟩ _
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
x : X
y : Y
h_1 : (x, y) ∈ s ×ˢ t
h h₁ :
  SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {x}) (nhdsKer {y}) =
    SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {(x, y).1}) (nhdsKer {(x, y).2})
⊢ nhdsKer {(x, y)} = SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {(x, y).1}) (nhdsKer {(x, y).2})

Tactic:
rw [nhdsKer_pair]

Premises used: nhdsKer_pair
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
simp_rw :
  SProd.sprod (α := Set X) (β := Set Y) (nhdsKer (⋃ i ∈ s, {i})) (nhdsKer (⋃ i ∈ t, {i})) = nhdsKer s ×ˢ nhdsKer t
⊢ SProd.sprod (α := Set X) (β := Set Y) (⋃ x ∈ s, nhdsKer {x}) (⋃ y ∈ t, nhdsKer {y}) = nhdsKer s ×ˢ nhdsKer t

Tactic:
simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]

Premises used: Set.biUnion_of_singleton, nhdsKer_biUnion
-- Module: Mathlib.Topology.NhdsKer
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
p : (i : ι) → X i
simp_rw : (𝓝 p).ker = Set.pi (α := X) univ fun (i : ι) ↦ (𝓝 (p i)).ker
simp_rw₁ :
  Eq (α := Set ((i : ι) → X i)) (ker (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (p i)))
    (Set.pi (α := X) univ fun (i : ι) ↦ (𝓝 (p i)).ker)
⊢ Eq (α := Set ((i : ι) → X i)) (nhdsKer {p}) (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})

Tactic:
simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_pi, ker_pi]

Premises used: nhdsKer_singleton_eq_ker_nhds, nhds_pi, Filter.ker_pi
-- Module: Mathlib.Topology.NhdsKer
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
rw : ⋃ i ∈ Set.pi (α := X) univ s, nhdsKer {i}
| nhdsKer (Set.pi (α := X) univ s)

Tactic:
rw [← biUnion_of_singleton (univ.pi s), nhdsKer_biUnion]

Premises used: Set.univ, Set.biUnion_of_singleton, nhdsKer_biUnion, Set.pi
-- Module: Mathlib.Topology.NhdsKer
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
conv_lhs : nhdsKer (Set.pi (α := X) univ s) = ⋃ p ∈ Set.pi (α := X) univ s, nhdsKer {p}
conv_lhs₁ :
  Eq (α := Set ((i : ι) → X i)) (⋃ i ∈ Set.pi (α := X) univ s, nhdsKer {i}) (⋃ p ∈ Set.pi (α := X) univ s, nhdsKer {p})
⊢ nhdsKer (Set.pi (α := X) univ s) = ⋃ p ∈ Set.pi (α := X) univ s, nhdsKer {p}

Tactic:
conv_lhs => rw [← biUnion_of_singleton (univ.pi s), nhdsKer_biUnion]

Premises used: Set.univ, Set.biUnion_of_singleton, nhdsKer_biUnion, Set.pi
-- Module: Mathlib.Topology.NhdsKer
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h :
  ∀ p ∈ Set.pi (α := X) univ s,
    Eq (α := Set ((i : ι) → X i)) (nhdsKer {p}) (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})
⊢ Eq (α := Set ((i : ι) → X i)) (⋃ p ∈ Set.pi (α := X) univ s, nhdsKer {p})
    (⋃ p ∈ Set.pi (α := X) univ s, Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})

Tactic:
congr! with p _
-- Module: Mathlib.Topology.NhdsKer
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
p : (i : ι) → X i
h_1 : p ∈ Set.pi (α := X) univ s
h h₁ :
  Eq (α := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})
    (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})
⊢ Eq (α := Set ((i : ι) → X i)) (nhdsKer {p}) (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})

Tactic:
rw [nhdsKer_singleton_pi]

Premises used: nhdsKer_singleton_pi
-- Module: Mathlib.Topology.NhdsKer
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
simp_rw :
  Eq (α := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer (⋃ i_1 ∈ s i, {i_1}))
    (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer (s i))
⊢ Eq (α := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ ⋃ x ∈ s i, nhdsKer {x})
    (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer (s i))

Tactic:
simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]

Premises used: Set.biUnion_of_singleton, nhdsKer_biUnion
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_4
inst : TopologicalSpace (X × X)
rw : Eq.{u_4 + 1} (α := Filter (X × X)) (sSup (range (ι := X) (𝓝 ∘ fun (x : X) ↦ (x, x)))) (⨆ (x : X), 𝓝 (x, x))
⊢ 𝓝ˢ (diagonal X) = ⨆ (x : X), 𝓝 (x, x)

Tactic:
rw [nhdsSet, ← range_diag, ← range_comp]

Premises used: Set.range_comp, Set.range_diag, nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_4
inst : TopologicalSpace (X × X)
⊢ Eq.{u_4 + 1} (α := Filter (X × X)) (sSup (range (ι := X) (𝓝 ∘ fun (x : X) ↦ (x, x)))) (⨆ (x : X), 𝓝 (x, x))

Tactic:
rfl
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
simp_rw : s ∈ sSup (𝓝 '' t) ↔ ∀ x ∈ t, s ∈ 𝓝 x
simp_rw₁ : (∀ f ∈ 𝓝 '' t, s ∈ f) ↔ ∀ x ∈ t, s ∈ 𝓝 x
⊢ s ∈ 𝓝ˢ t ↔ ∀ x ∈ t, s ∈ 𝓝 x

Tactic:
simp_rw [nhdsSet, Filter.mem_sSup, forall_mem_image]

Premises used: nhdsSet, Set.forall_mem_image, Filter.mem_sSup
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
f : Filter X
s : Set X
⊢ 𝓝ˢ s ≤ f ↔ ∀ x ∈ s, 𝓝 x ≤ f

Tactic:
simp [nhdsSet]

Premises used: nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
t : X → Set X
h : ∀ x ∈ s, t x ∈ 𝓝 x
⊢ ⋃ x ∈ s, t x ∈ 𝓝ˢ s

Tactic:
mem_nhdsSet_iff_forall.2 fun x hx => mem_of_superset (h x hx) <|
    subset_iUnion₂ (s := fun x _ => t x) x hx

Premises used: Iff.mpr, Set.subset_iUnion₂, mem_nhdsSet_iff_forall, Filter.mem_of_superset
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
simp_rw : s ⊆ interior t ↔ ∀ x ∈ s, t ∈ 𝓝 x
⊢ s ⊆ interior t ↔ t ∈ 𝓝ˢ s

Tactic:
simp_rw [mem_nhdsSet_iff_forall, subset_interior_iff_nhds]

Premises used: subset_interior_iff_nhds, mem_nhdsSet_iff_forall
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
rw : sᶜ ∈ 𝓝ˢ t ↔ Disjoint (closure[inst] s) t
rw₁ : t ⊆ interior sᶜ ↔ Disjoint (closure[inst] s) t
rw₂ : t ⊆ (closure[inst] s)ᶜ ↔ Disjoint (closure[inst] s) t
rw₃ rw₄ : Disjoint (closure[inst] s) t ↔ Disjoint (closure[inst] s) t
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure[inst] s) t

Tactic:
rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
    subset_compl_iff_disjoint_left]

Premises used: Filter.disjoint_principal_left, Set.subset_compl_iff_disjoint_left, subset_interior_iff_mem_nhdsSet, interior_compl
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
rw : Disjoint (𝓟 t) (𝓝ˢ s) ↔ Disjoint s (closure[inst] t)
rw₁ : Disjoint (closure[inst] t) s ↔ Disjoint s (closure[inst] t)
rw₂ rw₃ : Disjoint s (closure[inst] t) ↔ Disjoint s (closure[inst] t)
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure[inst] t)

Tactic:
rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]

Premises used: disjoint_comm, disjoint_principal_nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
rw : t ⊆ interior s ↔ ∃ (U : Set X), IsOpen[inst] U ∧ t ⊆ U ∧ U ⊆ s
rw₁ rw₂ : (∃ (U : Set X), IsOpen[inst] U ∧ t ⊆ U ∧ U ⊆ s) ↔ ∃ (U : Set X), IsOpen[inst] U ∧ t ⊆ U ∧ U ⊆ s
⊢ s ∈ 𝓝ˢ t ↔ ∃ (U : Set X), IsOpen[inst] U ∧ t ⊆ U ∧ U ⊆ s

Tactic:
rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]

Premises used: subset_interior_iff_mem_nhdsSet, subset_interior_iff
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
p : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ↔ ∃ (t : Set X), IsOpen[inst] t ∧ s ⊆ t ∧ ∀ x ∈ t, p x

Tactic:
mem_nhdsSet_iff_exists

Premises used: Set.Mem, Filter.Eventually, setOf, mem_nhdsSet_iff_exists, Set.Subset
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
p : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ↔ ∀ x ∈ s, ∀ᶠ (y : X) in 𝓝 x, p y

Tactic:
mem_nhdsSet_iff_forall

Premises used: Filter.Eventually, mem_nhdsSet_iff_forall
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ t ∈ 𝓝ˢ s ↔ ∃ (i : Set X), (IsOpen[inst] i ∧ s ⊆ i) ∧ i ⊆ t

Tactic:
simp [mem_nhdsSet_iff_exists, and_assoc]

Premises used: mem_nhdsSet_iff_exists, and_assoc
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ (𝓝ˢ s).lift' interior = 𝓝ˢ s

Tactic:
(hasBasis_nhdsSet s).lift'_interior_eq_self fun _ ↦ And.left

Premises used: hasBasis_nhdsSet, Filter.HasBasis.lift'_interior_eq_self, And.left
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Sort u_4
p : ι → Prop
s : ι → Set X
t : Set X
h : (𝓝ˢ t).HasBasis p s
⊢ (𝓝ˢ t).HasBasis p fun (x : ι) ↦ interior (s x)

Tactic:
lift'_nhdsSet_interior t ▸ h.lift'_interior

Premises used: lift'_nhdsSet_interior, Eq.rec, Filter.HasBasis.lift'_interior
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hU : IsOpen[inst] s
rw : t ⊆ interior s ↔ t ⊆ s
rw₁ rw₂ : t ⊆ s ↔ t ⊆ s
⊢ s ∈ 𝓝ˢ t ↔ t ⊆ s

Tactic:
rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]

Premises used: subset_interior_iff_mem_nhdsSet, IsOpen.interior_eq
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ho : IsOpen[inst] s
⊢ s ∈ 𝓝ˢ s

Tactic:
ho.mem_nhdsSet.mpr Subset.rfl

Premises used: Iff.mpr, Set.Subset.rfl, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ 𝓟 s ≤ 𝓝ˢ s

Tactic:
fun _s hs =>
  (subset_interior_iff_mem_nhdsSet.mpr hs).trans interior_subset

Premises used: Iff.mpr, interior_subset, Set.Mem, setOf, HasSubset.Subset.trans, Set.Subset, subset_interior_iff_mem_nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : t ∈ 𝓝ˢ s
⊢ s ⊆ t

Tactic:
principal_le_nhdsSet h

Premises used: Set.Mem, setOf, Set.Subset, principal_le_nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
p : X → Prop
h : ∀ᶠ (x : X) in 𝓝ˢ s, p x
⊢ ∀ x ∈ s, p x

Tactic:
principal_le_nhdsSet h

Premises used: Set.Mem, setOf, Set.Subset, principal_le_nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
Y : Type u_4
f g : X → Y
h : f =ᶠ[𝓝ˢ s] g
⊢ EqOn f g s

Tactic:
h.self_of_nhdsSet

Premises used: Set.EqOn, Filter.Eventually.self_of_nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
rw : 𝓝ˢ s ≤ 𝓟 s ↔ IsOpen[inst] s
rw₁ : s ∈ 𝓝ˢ s ↔ IsOpen[inst] s
rw₂ : (∀ x ∈ s, s ∈ 𝓝 x) ↔ IsOpen[inst] s
rw₃ rw₄ : (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ x ∈ s, s ∈ 𝓝 x
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen[inst] s

Tactic:
rw [← principal_le_nhdsSet.ge_iff_eq', le_principal_iff, mem_nhdsSet_iff_forall,
    isOpen_iff_mem_nhds]

Premises used: Filter.le_principal_iff, mem_nhdsSet_iff_forall, LE.le.ge_iff_eq', isOpen_iff_mem_nhds, principal_le_nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ (interior s) = 𝓟 (interior s)

Tactic:
isOpen_interior.nhdsSet_eq

Premises used: isOpen_interior, IsOpen.nhdsSet_eq
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
⊢ 𝓝ˢ {x} = 𝓝 x

Tactic:
simp [nhdsSet]

Premises used: nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ s ∈ 𝓝ˢ (interior s)

Tactic:
subset_interior_iff_mem_nhdsSet.mp Subset.rfl

Premises used: Set.Subset.rfl, subset_interior_iff_mem_nhdsSet, Iff.mp
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
rw : Eq.{u_2 + 1} (α := Filter X) (𝓟 ∅) ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := Filter X) ⊥ ⊥
⊢ Eq.{u_2 + 1} (α := Filter X) (𝓝ˢ ∅) ⊥

Tactic:
rw [isOpen_empty.nhdsSet_eq, principal_empty]

Premises used: Filter.principal_empty, IsOpen.nhdsSet_eq, isOpen_empty
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ Membership.mem (γ := Filter X) (𝓝ˢ ∅) s

Tactic:
simp
-- Module: Mathlib.Topology.NhdsSet
Goal:
α : Type u_4
inst : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ s = ⊥ → s = ∅

Tactic:
simp [← empty_mem_iff_bot, mem_nhdsSet_iff_forall, eq_empty_iff_forall_notMem]

Premises used: mem_nhdsSet_iff_forall, Set.eq_empty_iff_forall_notMem, Filter.empty_mem_iff_bot
-- Module: Mathlib.Topology.NhdsSet
Goal:
α : Type u_4
inst : TopologicalSpace α
s : Set α
⊢ s = ∅ → 𝓝ˢ s = ⊥

Tactic:
simp +contextual
-- Module: Mathlib.Topology.NhdsSet
Goal:
α : Type u_4
inst : TopologicalSpace α
s : Set α
⊢ ¬(𝓝ˢ s).NeBot ↔ ¬s.Nonempty

Tactic:
simp [not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
rw : Eq.{u_2 + 1} (α := Filter X) (𝓟 univ) ⊤
rw₁ rw₂ : Eq.{u_2 + 1} (α := Filter X) ⊤ ⊤
⊢ Eq.{u_2 + 1} (α := Filter X) (𝓝ˢ univ) ⊤

Tactic:
rw [isOpen_univ.nhdsSet_eq, principal_univ]

Premises used: Filter.principal_univ, isOpen_univ, IsOpen.nhdsSet_eq
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : s ⊆ t
⊢ 𝓝ˢ s ≤ 𝓝ˢ t

Tactic:
sSup_le_sSup <| image_mono h

Premises used: Set.Mem, Set.image_mono, sSup_le_sSup
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ Monotone.{u_2, u_2} (α := Set X) 𝓝ˢ

Tactic:
fun _ _ => nhdsSet_mono

Premises used: nhdsSet_mono, Monotone
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
x : X
h : x ∈ s
⊢ 𝓝 x ≤ 𝓝ˢ s

Tactic:
le_sSup <| mem_image_of_mem _ h

Premises used: Set.Mem, Set.mem_image_of_mem, le_sSup
-- Module: Mathlib.Topology.NhdsSet
Goal:
α : Type u_1
X : Type u_2
inst : TopologicalSpace X
s : Set X
f : α → X
l : Filter α
x : X
hx : x ∈ s
hf : Tendsto f l (𝓝 x)
⊢ Tendsto f l (𝓝ˢ s)

Tactic:
hf.trans (nhds_le_nhdsSet hx)

Premises used: nhds_le_nhdsSet, Filter.Tendsto, LE.le.trans
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t

Tactic:
simp only [nhdsSet, image_union, sSup_union]

Premises used: sSup_union, nhdsSet, Set.image_union
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
rw : s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)

Tactic:
rw [nhdsSet_union]

Premises used: nhdsSet_union
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂

Tactic:
union_mem_sup h₁ h₂

Premises used: Filter.union_mem_sup
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂

Tactic:
exact union_mem_sup h₁ h₂

Premises used: Filter.union_mem_sup
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
s : Set X
rw : 𝓝ˢ ({x} ∪ s) = 𝓝 x ⊔ 𝓝ˢ s
rw₁ : 𝓝ˢ {x} ⊔ 𝓝ˢ s = 𝓝 x ⊔ 𝓝ˢ s
rw₂ rw₃ : 𝓝 x ⊔ 𝓝ˢ s = 𝓝 x ⊔ 𝓝ˢ s
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s

Tactic:
rw [insert_eq, nhdsSet_union, nhdsSet_singleton]

Premises used: nhdsSet_union, Set.insert_eq, nhdsSet_singleton
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ 𝓝ˢ (s ∩ t) ≤ 𝓝ˢ s ⊓ 𝓝ˢ t

Tactic:
(monotone_nhdsSet (X := X)).map_inf_le s t

Premises used: Set.Mem, setOf, Monotone.map_inf_le, monotone_nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Sort u_4
s : ι → Set X
⊢ LE.le.{u_2} (α := Filter X) (𝓝ˢ (⋂ (i : ι), s i)) (⨅ (i : ι), 𝓝ˢ (s i))

Tactic:
(monotone_nhdsSet (X := X)).map_iInf_le

Premises used: Set.Mem, Set.iInter, setOf, Monotone.map_iInf_le, monotone_nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set (Set X)
⊢ 𝓝ˢ (⋂₀ s) ≤ ⨅ x ∈ s, 𝓝ˢ x

Tactic:
(monotone_nhdsSet (X := X)).map_sInf_le

Premises used: Set.Mem, setOf, Monotone.map_sInf_le, monotone_nhdsSet, Set.sInter
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
rw rw₁ : 𝓝ˢ s = 𝓝ˢ s
⊢ 𝓝ˢ s = 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ)

Tactic:
rw [Set.inter_union_compl s t]

Premises used: Set.inter_union_compl
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
rw rw₁ : 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)
⊢ 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)

Tactic:
rw [nhdsSet_union]

Premises used: nhdsSet_union
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
nth_grw nth_grw₁ : 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ) ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ

Tactic:
nth_grw 2 [inter_subset_right]

Premises used: Set.inter_subset_right
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
rw rw₁ : 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ = 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ = 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ

Tactic:
rw [h.isOpen_compl.nhdsSet_eq]

Premises used: IsClosed.isOpen_compl, IsOpen.nhdsSet_eq
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
rw : 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
⊢ 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 tᶜ

Tactic:
rw [Set.inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ

Tactic:
h.nhdsSet_le_sup s

Premises used: IsClosed.nhdsSet_le_sup
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ

Tactic:
exact h.nhdsSet_le_sup s

Premises used: IsClosed.nhdsSet_le_sup
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
p : X → Prop
h : ∀ᶠ (y : X) in 𝓝ˢ s, p y
⊢ ∀ᶠ (y : X) in 𝓝ˢ s, ∀ᶠ (x : X) in 𝓝 y, p x

Tactic:
eventually_nhdsSet_iff_forall.mpr fun x x_in ↦
    (eventually_nhdsSet_iff_forall.mp h x x_in).eventually_nhds

Premises used: Iff.mpr, Filter.Eventually.eventually_nhds, Iff.mp, eventually_nhdsSet_iff_forall
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
p : X → Prop
rw : (∀ᶠ (x : X) in 𝓝ˢ s ⊔ 𝓝ˢ t, p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x
rw₁ rw₂ : ((∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x
⊢ (∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x

Tactic:
rw [nhdsSet_union, eventually_sup]

Premises used: nhdsSet_union, Filter.eventually_sup
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
p : X → Prop
hs : ∀ᶠ (x : X) in 𝓝ˢ s, p x
ht : ∀ᶠ (x : X) in 𝓝ˢ t, p x
⊢ ∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x

Tactic:
Filter.Eventually.union_nhdsSet.mpr ⟨hs, ht⟩

Premises used: Iff.mpr, Filter.Eventually.union_nhdsSet, And.intro
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Sort u_4
s : ι → Set X
⊢ Eq.{u_2 + 1} (α := Filter X) (𝓝ˢ (⋃ (i : ι), s i)) (⨆ (i : ι), 𝓝ˢ (s i))

Tactic:
simp only [nhdsSet, image_iUnion, sSup_iUnion (β := Filter X)]

Premises used: Set.image_iUnion, sSup_iUnion, nhdsSet
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Sort u_4
p : ι → Prop
s : ι → Set X
P : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (⋃ (i : ι), ⋃ (_ : p i), s i), P x) ↔ ∀ (i : ι), p i → ∀ᶠ (x : X) in 𝓝ˢ (s i), P x

Tactic:
simp only [nhdsSet_iUnion, eventually_iSup]

Premises used: nhdsSet_iUnion, Filter.eventually_iSup
-- Module: Mathlib.Topology.NhdsSet
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Sort u_4
s : ι → Set X
P : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (⋃ (i : ι), s i), P x) ↔ ∀ (i : ι), ∀ᶠ (x : X) in 𝓝ˢ (s i), P x

Tactic:
simp only [nhdsSet_iUnion, eventually_iSup]

Premises used: nhdsSet_iUnion, Filter.eventually_iSup
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ ((𝓝 a).bind fun (x : α) ↦ 𝓝[s] x) = 𝓝[s] a

Tactic:
bind_inf_principal.trans <| congr_arg₂ _ nhds_bind_nhds rfl

Premises used: nhdsWithin, nhds_bind_nhds, Filter.bind_inf_principal, rfl, Eq.trans, congr_arg₂
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝 a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x

Tactic:
Filter.ext_iff.1 nhds_bind_nhdsWithin { x | p x }

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.ext_iff, Set.preimage, Iff.mp, nhds_bind_nhdsWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
p : α → Prop
⊢ (∀ᶠ (x : α) in 𝓝[s] a, p x) ↔ ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x

Tactic:
eventually_inf_principal

Premises used: Filter.eventually_inf_principal, nhdsWithin
-- Module: Mathlib.Topology.NhdsWithin
Goal:
α : Type u_1
inst : TopologicalSpace α
z : α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in 𝓝 z, x ∈ s ∧ p x) ↔ ∃ᶠ (x : α) in 𝓝 z, p x ∧ x ∈ s

Tactic:
simp only [and_comm]

Premises used: and_comm