awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
f : α → X
a : α
⊢ Tendsto f (pure a) (𝓝 (f a))

Tactic:
(tendsto_pure_pure f a).mono_right (pure_le_nhds _)

Premises used: pure_le_nhds, Filter.tendsto_pure_pure, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
inst_1 : PartialOrder α
inst_2 : OrderTop α
f : α → X
⊢ Tendsto f atTop (𝓝 (f ⊤))

Tactic:
(tendsto_atTop_pure f).mono_right (pure_le_nhds _)

Premises used: pure_le_nhds, Filter.tendsto_atTop_pure, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
α : Type u_1
x : X
s t : Set X
⊢ (𝓝 x).NeBot

Tactic:
neBot_of_le (pure_le_nhds x)

Premises used: pure_le_nhds, Filter.neBot_of_le
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
l : Filter α
f : α → X
h : ∀ᶠ (x' : α) in l, f x' = x
⊢ Tendsto f l (𝓝 x)

Tactic:
tendsto_const_nhds.congr' (.symm h)

Premises used: tendsto_const_nhds, Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
l : Filter α
f : α → X
hf : f =ᶠ[l] fun (x_1 : α) ↦ x
⊢ Tendsto f l (𝓝 x)

Tactic:
tendsto_nhds_of_eventually_eq hf

Premises used: tendsto_nhds_of_eventually_eq
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ interior s ↔ Membership.mem (γ := Set X) {x : X | s ∈ 𝓝 x} x

Tactic:
simp only [mem_interior, mem_nhds_iff, mem_setOf_eq]

Premises used: mem_nhds_iff, Set.mem_setOf_eq, mem_interior
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ Eq.{u + 1} (α := Set X) {x : X | s ∈ 𝓝 x} {x : X | 𝓝 x ≤ 𝓟 s}

Tactic:
simp only [le_principal_iff]

Premises used: Filter.le_principal_iff
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ interior s ∈ 𝓝 x ↔ s ∈ 𝓝 x

Tactic:
⟨fun h => mem_of_superset h interior_subset, fun h =>
    IsOpen.mem_nhds isOpen_interior (mem_interior_iff_mem_nhds.2 h)⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, interior_subset, isOpen_interior, IsOpen.mem_nhds, Iff.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
⊢ Eq.{u + 1} (α := Set X) (interior {x : X | p x}) {x : X | ∀ᶠ (y : X) in 𝓝 x, p y}

Tactic:
interior_eq_nhds'

Premises used: Set.Mem, Filter.Eventually, setOf, interior_eq_nhds'
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
⊢ IsOpen[inst] {x : X | ∀ᶠ (y : X) in 𝓝 x, p y}

Tactic:
simp only [← interior_setOf_eq, isOpen_interior]

Premises used: isOpen_interior, interior_setOf_eq
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
simp_rw : s ⊆ {x : X | 𝓝 x ≤ 𝓟 s} ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
simp_rw₁ : (∀ x ∈ s, Membership.mem (γ := Set X) {x : X | 𝓝 x ≤ 𝓟 s} x) ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
⊢ s ⊆ interior s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s

Tactic:
simp_rw [interior_eq_nhds, subset_def, mem_setOf]

Premises used: Set.subset_def, Set.mem_setOf, interior_eq_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
a : ∀ (x : Set X), IsOpen[t] x ↔ IsOpen[t'] x
⊢ t = t'

Tactic:
ext
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x : Set X
a : (∀ x_1 ∈ x, 𝓝 x_1 ≤ 𝓟 x) ↔ ∀ x_1 ∈ x, 𝓝 x_1 ≤ 𝓟 x
⊢ IsOpen[t] x ↔ IsOpen[t'] x

Tactic:
simp_rw [@isOpen_iff_nhds _ _ _, H]

Premises used: isOpen_iff_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsOpen[inst] s ↔ ∀ x ∈ s, s ∈ 𝓝 x

Tactic:
isOpen_iff_nhds.trans <| forall_congr' fun _ => imp_congr_right fun _ => le_principal_iff

Premises used: imp_congr_right, Filter.le_principal_iff, forall_congr', Iff.trans, isOpen_iff_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsOpen[inst] s ↔ ∀ x ∈ s, ∀ᶠ (y : X) in 𝓝 x, y ∈ s

Tactic:
isOpen_iff_mem_nhds

Premises used: Set.Mem, Filter.Eventually, setOf, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ IsOpen[inst] {x} ↔ 𝓝 x = pure x

Tactic:
simp [← (pure_le_nhds _).ge_iff_eq', isOpen_iff_mem_nhds]

Premises used: pure_le_nhds, LE.le.ge_iff_eq', isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
rw : 𝓝 x ≤ pure x ∧ pure x ≤ 𝓝 x ↔ {x} ∈ 𝓝 x
⊢ IsOpen[inst] {x} ↔ 𝓝[≠] x = ⊥

Tactic:
rw [isOpen_singleton_iff_nhds_eq_pure, nhdsWithin, ← mem_iff_inf_principal_compl,
      le_antisymm_iff]

Premises used: nhdsWithin, le_antisymm_iff, isOpen_singleton_iff_nhds_eq_pure, Filter.mem_iff_inf_principal_compl
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ 𝓝 x ≤ pure x ∧ pure x ≤ 𝓝 x ↔ {x} ∈ 𝓝 x

Tactic:
simp [pure_le_nhds x]

Premises used: pure_le_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : x ∈ closure[inst] s ↔ ¬∀ᶠ (x : X) in 𝓝 x, x ∉ s
rw₁ : x ∈ closure[inst] s ↔ {x : X | x ∉ s} ∉ 𝓝 x
rw₂ : x ∈ closure[inst] s ↔ x ∉ interior {x : X | x ∉ s}
rw₃ : x ∈ (interior sᶜ)ᶜ ↔ x ∉ interior {x : X | x ∉ s}
rw₄ : x ∉ interior sᶜ ↔ x ∉ interior {x : X | x ∉ s}
rw₅ rw₆ : x ∉ interior {x : X | x ∉ s} ↔ x ∉ interior {x : X | x ∉ s}
⊢ x ∈ closure[inst] s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s

Tactic:
rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
    closure_eq_compl_interior_compl, mem_compl_iff, compl_def]

Premises used: Set.compl_def, mem_interior_iff_mem_nhds, Filter.Eventually, Filter.Frequently, closure_eq_compl_interior_compl, Set.mem_compl_iff
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : closure[inst] s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
⊢ IsClosed[inst] s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
rw [← closure_subset_iff_isClosed]

Premises used: closure_subset_iff_isClosed
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure[inst] s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
forall_congr' fun x => ?_

Premises used: Set.Subset, forall_congr'
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
refine : ∀ (x : X), x ∈ closure[inst] s → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
⊢ closure[inst] s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
refine forall_congr' fun x => ?_

Premises used: forall_congr'
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : X
rw rw₁ : (∃ᶠ (x : X) in 𝓝 x, x ∈ s) → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
⊢ x ∈ closure[inst] s → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
rw [mem_closure_iff_frequently]

Premises used: mem_closure_iff_frequently
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw :
  (∀ ⦃s_1 : Set X⦄, s_1 ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ 𝓟 s → (s_1 ∩ s').Nonempty) ↔
    ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty
⊢ (𝓝[s] x).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Tactic:
rw [nhdsWithin, inf_neBot_iff]

Premises used: nhdsWithin, Filter.inf_neBot_iff
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ (∀ ⦃s_1 : Set X⦄, s_1 ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ 𝓟 s → (s_1 ∩ s').Nonempty) ↔
    ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Tactic:
forall₂_congr fun U _ ↦
    ⟨fun h ↦ h (mem_principal_self _), fun h u hsu ↦ h.mono <| inter_subset_inter_right _ hsu⟩

Premises used: Set.inter_subset_inter_right, Filter.mem_principal_self, Set.Nonempty.mono, forall₂_congr, Iff.intro
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ (∀ ⦃s_1 : Set X⦄, s_1 ∈ 𝓝 x → ∀ ⦃s' : Set X⦄, s' ∈ 𝓟 s → (s_1 ∩ s').Nonempty) ↔
    ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Tactic:
exact forall₂_congr fun U _ ↦
    ⟨fun h ↦ h (mem_principal_self _), fun h u hsu ↦ h.mono <| inter_subset_inter_right _ hsu⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s t : Set X
h : s ⊆ t
⊢ 𝓝[s] x ≤ 𝓝[t] x

Tactic:
inf_le_inf_left _ (principal_mono.mpr h)

Premises used: Iff.mpr, Filter.principal_mono, Set.Mem, inf_le_inf_left
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] s
⊢ interior (s ∪ t) ⊆ s ∪ interior t

Tactic:
fun a ⟨u, ⟨⟨hu₁, hu₂⟩, ha⟩⟩ =>
  (Classical.em (a ∈ s)).imp_right fun h =>
    mem_interior.mpr
      ⟨u ∩ sᶜ, fun _x hx => (hu₂ hx.1).resolve_left hx.2, IsOpen.inter hu₁ IsClosed.isOpen_compl,
        ⟨ha, h⟩⟩

Premises used: Iff.mpr, IsClosed.isOpen_compl, Compl.compl, Membership.mem, Or.resolve_left, Set.Subset, Inter.inter, And.right, And.left, _private.0.IsClosed.interior_union_left.match_1, And.intro, interior, IsOpen.inter, Classical.em, Exists.intro, mem_interior, Union.union, Or.imp_right
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
⊢ interior (s ∪ t) ⊆ interior s ∪ t

Tactic:
simpa only [union_comm _ t] using h.interior_union_left

Premises used: Set.union_comm, IsClosed.interior_union_left
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : IsOpen[inst] s
⊢ (closure[inst] (s ∩ t))ᶜ ⊆ (s ∩ closure[inst] t)ᶜ

Tactic:
simpa only [← interior_compl, compl_inter] using IsClosed.interior_union_left h.isClosed_compl

Premises used: Set.compl_inter, IsOpen.isClosed_compl, interior_compl, IsClosed.interior_union_left
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : IsOpen[inst] t
⊢ closure[inst] s ∩ t ⊆ closure[inst] (s ∩ t)

Tactic:
simpa only [inter_comm t] using h.inter_closure

Premises used: IsOpen.inter_closure, Set.inter_comm
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : Dense s
ht : IsOpen[inst] t
rw : t = t ∩ univ
rw₁ rw₂ : t = t
⊢ t = t ∩ closure[inst] s

Tactic:
rw [hs.closure_eq, inter_univ]

Premises used: Set.inter_univ, Dense.closure_eq
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : Dense s
ht : Dense t
hso : IsOpen[inst] s
x : X
⊢ x ∈ closure[inst] (s ∩ closure[inst] t)

Tactic:
simp [hs.closure_eq, ht.closure_eq]

Premises used: Dense.closure_eq
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : Dense s
ht : Dense t
hto : IsOpen[inst] t
⊢ Dense (s ∩ t)

Tactic:
inter_comm t s ▸ ht.inter_of_isOpen_left hs hto

Premises used: Eq.rec, Dense.inter_of_isOpen_left, Set.inter_comm
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s t : Set X
hs : Dense s
ht : t ∈ 𝓝 x
⊢ (s ∩ t).Nonempty

Tactic:
let ⟨U, hsub, ho, hx⟩ := mem_nhds_iff.1 ht
  (hs.inter_open_nonempty U ho ⟨x, hx⟩).mono fun _y hy => ⟨hy.2, hsub hy.1⟩

Premises used: mem_nhds_iff, _private.0.mem_of_mem_nhds.match_1, Set.Nonempty.mono, Inter.inter, Dense.inter_open_nonempty, Set.Nonempty, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure[inst] s \ closure[inst] t = (closure[inst] t)ᶜ ∩ closure[inst] s

Tactic:
simp only [diff_eq, inter_comm]

Premises used: Set.diff_eq, Set.inter_comm
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure[inst] ((closure[inst] t)ᶜ ∩ s) = closure[inst] (s \ closure[inst] t)

Tactic:
simp only [diff_eq, inter_comm]

Premises used: Set.diff_eq, Set.inter_comm
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
h : ∃ᶠ (x : X) in 𝓝 x, x ∈ s
hs : IsClosed[inst] s
⊢ x ∈ s

Tactic:
hs.closure_subset h.mem_closure

Premises used: IsClosed.closure_subset, Filter.Frequently.mem_closure
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
s : Set X
f : α → X
b : Filter α
hs : IsClosed[inst] s
h : ∃ᶠ (x : α) in b, f x ∈ s
hf : Tendsto f b (𝓝 x)
⊢ x ∈ s

Tactic:
(hf.frequently <| show ∃ᶠ x in b, (fun y => y ∈ s) (f x) from h).mem_of_closed hs

Premises used: Filter.Tendsto.frequently, Filter.Frequently.mem_of_closed
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
s : Set X
f : α → X
b : Filter α
inst_1 : b.NeBot
hs : IsClosed[inst] s
hf : Tendsto f b (𝓝 x)
h : ∀ᶠ (x : α) in b, f x ∈ s
⊢ x ∈ s

Tactic:
hs.mem_of_frequently_of_tendsto h.frequently hf

Premises used: IsClosed.mem_of_frequently_of_tendsto, Filter.Eventually.frequently
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
s : Set X
f : α → X
b : Filter α
h : ∃ᶠ (x : α) in b, f x ∈ s
hf : Tendsto f b (𝓝 x)
⊢ x ∈ closure[inst] s

Tactic:
(hf.frequently h).mem_closure

Premises used: Filter.Tendsto.frequently, Filter.Frequently.mem_closure
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
s : Set X
f : α → X
b : Filter α
inst_1 : b.NeBot
hf : Tendsto f b (𝓝 x)
h : ∀ᶠ (x : α) in b, f x ∈ s
⊢ x ∈ closure[inst] s

Tactic:
mem_closure_of_frequently_of_tendsto h.frequently hf

Premises used: mem_closure_of_frequently_of_tendsto, Filter.Eventually.frequently
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
rw : l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)
⊢ Tendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Tendsto f l (𝓝 x)

Tactic:
rw [tendsto_iff_comap, tendsto_iff_comap]

Premises used: Filter.tendsto_iff_comap
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x_1 : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x_1
U : Set α
t : Set X
ht : t ∈ 𝓝 x_1
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
⊢ f x ∈ t

Tactic:
have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x_1 : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x_1
U : Set α
t : Set X
ht : t ∈ 𝓝 x_1
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
this : f x ∈ t
⊢ x ∈ U

Tactic:
htU this
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x_1 : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x_1
U : Set α
t : Set X
ht : t ∈ 𝓝 x_1
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
this : f x ∈ t
⊢ x ∈ U

Tactic:
exact htU this
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ 𝓟 sᶜ ≤ comap f (𝓝 x)

Tactic:
replace h : 𝓟 sᶜ ≤ comap f (𝓝 x) := by
    rintro U ⟨t, ht, htU⟩ x hx
    have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
    exact htU this
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)

Tactic:
⟨fun h' => ?_, le_trans inf_le_left⟩

Premises used: Iff.intro, inf_le_left, le_trans
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
refine : ∀ (h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)), l ≤ comap f (𝓝 x)
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)

Tactic:
refine ⟨fun h' => ?_, le_trans inf_le_left⟩
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
⊢ l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)

Tactic:
have := sup_le h' h
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)

Tactic:
rw [sup_inf_right, sup_principal, union_compl_self, principal_univ, inf_top_eq, sup_le_iff]
    at this

Premises used: Filter.sup_principal, inf_top_eq, Filter.principal_univ, sup_inf_right, Set.union_compl_self, sup_le_iff
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : l ≤ comap f (𝓝 x) ∧ 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
⊢ nhdsKer {x} = (𝓝 x).ker

Tactic:
simp [nhdsKer]

Premises used: nhdsKer
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
x y : X
rw : x ∈ (𝓝 y).ker ↔ x ⤳ y
rw₁ : Membership.mem (γ := Set X) {y_1 : X | y_1 ⤳ y} x ↔ x ⤳ y
rw₂ rw₃ : x ⤳ y ↔ x ⤳ y
⊢ Membership.mem (γ := Set X) (nhdsKer {y}) x ↔ x ⤳ y

Tactic:
rw [nhdsKer_singleton_eq_ker_nhds, ker_nhds_eq_specializes, mem_setOf]

Premises used: nhdsKer_singleton_eq_ker_nhds, ker_nhds_eq_specializes, Set.mem_setOf
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ nhdsKer s = ⋂₀ {t : Set X | IsOpen[inst] t ∧ s ⊆ t}

Tactic:
(hasBasis_nhdsSet _).ker.trans sInter_eq_biInter.symm

Premises used: hasBasis_nhdsSet, Set.sInter_eq_biInter, nhdsKer, Filter.HasBasis.ker, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ nhdsKer s ↔ ∀ (U : Set X), IsOpen[inst] U → s ⊆ U → x ∈ U

Tactic:
simp [nhdsKer_def]

Premises used: nhdsKer_def
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ s ⊆ nhdsKer t ↔ ∀ (U : Set X), IsOpen[inst] U → t ⊆ U → s ⊆ U

Tactic:
simp [nhdsKer_def]

Premises used: nhdsKer_def
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ s ⊆ nhdsKer s

Tactic:
subset_nhdsKer_iff.2 fun _ _ ↦ id

Premises used: Iff.mpr, subset_nhdsKer_iff, id
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsOpen[inst] t
rw : ⋂₀ {t : Set X | IsOpen[inst] t ∧ s ⊆ t} ⊆ t
⊢ nhdsKer s ⊆ t

Tactic:
rw [nhdsKer_def]

Premises used: nhdsKer_def
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsOpen[inst] t
⊢ ⋂₀ {t : Set X | IsOpen[inst] t ∧ s ⊆ t} ⊆ t

Tactic:
sInter_subset_of_mem ⟨h₂, h₁⟩

Premises used: Set.sInter_subset_of_mem, And.intro
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsOpen[inst] t
⊢ ⋂₀ {t : Set X | IsOpen[inst] t ∧ s ⊆ t} ⊆ t

Tactic:
exact sInter_subset_of_mem ⟨h₂, h₁⟩
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
h : IsOpen[inst] s
⊢ nhdsKer s = s

Tactic:
(nhdsKer_minimal Subset.rfl h).antisymm subset_nhdsKer

Premises used: subset_nhdsKer, Set.Subset.rfl, HasSubset.Subset.antisymm, nhdsKer_minimal
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
ht : IsOpen[inst] t
⊢ nhdsKer s ⊆ t ↔ s ⊆ t

Tactic:
⟨subset_nhdsKer.trans, fun h ↦ nhdsKer_minimal h ht⟩

Premises used: subset_nhdsKer, HasSubset.Subset.trans, Iff.intro, nhdsKer_minimal
-- Module: Mathlib.Topology.NhdsKer
Goal:
ι : Sort u_1
X : Type u_2
inst : TopologicalSpace X
s : ι → Set X
⊢ Eq.{u_2 + 1} (α := Set X) (nhdsKer (⋃ (i : ι), s i)) (⋃ (i : ι), nhdsKer (s i))

Tactic:
simp only [nhdsKer, nhdsSet_iUnion, ker_iSup]

Premises used: nhdsSet_iUnion, nhdsKer, Filter.ker_iSup
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
ι : Type u_3
s : Set ι
t : ι → Set X
⊢ Eq.{u_2 + 1} (α := Set X) (nhdsKer (⋃ i ∈ s, t i)) (⋃ i ∈ s, nhdsKer (t i))

Tactic:
simp only [nhdsKer_iUnion]

Premises used: nhdsKer_iUnion
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ nhdsKer (s ∪ t) = nhdsKer s ∪ nhdsKer t

Tactic:
simp only [nhdsKer, nhdsSet_union, ker_sup]

Premises used: nhdsSet_union, Filter.ker_sup, nhdsKer
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
S : Set (Set X)
⊢ nhdsKer (⋃₀ S) = ⋃ s ∈ S, nhdsKer s

Tactic:
simp only [sUnion_eq_biUnion, nhdsKer_iUnion]

Premises used: Set.sUnion_eq_biUnion, nhdsKer_iUnion
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ nhdsKer s ↔ Membership.mem (γ := Set X) (nhdsKer (⋃ y ∈ s, {y})) x

Tactic:
simp
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
x : X
⊢ Membership.mem (γ := Set X) (nhdsKer (⋃ y ∈ s, {y})) x ↔ ∃ y ∈ s, x ⤳ y

Tactic:
simp only [nhdsKer_iUnion, mem_nhdsKer_singleton, mem_iUnion₂, exists_prop]

Premises used: exists_prop, Set.mem_iUnion₂, mem_nhdsKer_singleton, nhdsKer_iUnion
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ Monotone.{u_2, u_2} (α := Set X) nhdsKer

Tactic:
fun _s _t h ↦ ker_mono <| nhdsSet_mono h

Premises used: nhdsSet_mono, Monotone, Filter.ker_mono, nhdsKer
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : s ⊆ t
⊢ nhdsKer s ⊆ nhdsKer t

Tactic:
nhdsKer_mono h

Premises used: nhdsKer_mono
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ nhdsKer s ⊆ nhdsKer t ↔ 𝓝ˢ s ≤ 𝓝ˢ t

Tactic:
simp +contextual only [subset_nhdsKer_iff, (hasBasis_nhdsSet _).ge_iff,
    and_imp, IsOpen.mem_nhdsSet, IsOpen.nhdsKer_subset]

Premises used: subset_nhdsKer_iff, IsOpen.nhdsKer_subset, and_imp, hasBasis_nhdsSet, Filter.HasBasis.ge_iff, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ nhdsKer s = nhdsKer t ↔ 𝓝ˢ s = 𝓝ˢ t

Tactic:
simp [le_antisymm_iff]

Premises used: le_antisymm_iff
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
x y : X
⊢ x ⤳ y ↔ Subset (α := Set X) (nhdsKer {x}) (nhdsKer {y})

Tactic:
simp [Specializes]

Premises used: Specializes
-- Module: Mathlib.Topology.NhdsKer
Goal:
ι : Sort u_1
X : Type u_2
inst : TopologicalSpace X
s : ι → Set X
⊢ Subset.{u_2} (α := Set X) (nhdsKer (⋂ (i : ι), s i)) (⋂ (i : ι), nhdsKer (s i))

Tactic:
nhdsKer_mono.map_iInf_le

Premises used: Set.iInter, Monotone.map_iInf_le, nhdsKer_mono
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ nhdsKer (s ∩ t) ⊆ nhdsKer s ∩ nhdsKer t

Tactic:
nhdsKer_mono.map_inf_le _ _

Premises used: Monotone.map_inf_le, nhdsKer_mono
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set (Set X)
⊢ nhdsKer (⋂₀ s) ⊆ ⋂ x ∈ s, nhdsKer x

Tactic:
nhdsKer_mono.map_sInf_le

Premises used: Set.iInter, Monotone.map_sInf_le, nhdsKer_mono, Set.sInter
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ Eq.{u_2 + 1} (α := Set X) (nhdsKer ∅) ∅

Tactic:
isOpen_empty.nhdsKer_eq

Premises used: IsOpen.nhdsKer_eq, isOpen_empty
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ Eq.{u_2 + 1} (α := Set X) (nhdsKer univ) univ

Tactic:
isOpen_univ.nhdsKer_eq

Premises used: isOpen_univ, IsOpen.nhdsKer_eq
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ Eq.{u_2 + 1} (α := Set X) (nhdsKer ∅) ∅

Tactic:
nhdsKer_empty

Premises used: nhdsKer_empty
-- Module: Mathlib.Topology.NhdsKer
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ Eq.{u_2 + 1} (α := Set X) (nhdsKer ∅) ∅

Tactic:
exact nhdsKer_empty

Premises used: nhdsKer_empty