awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
neg :
  ∀ (z : X) (hzW : z ∈ W),
    z ∈ V ∩ ⋂ U ∈ S, interior Uᶜ → ∀ (hzV : z ∈ V), Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) z → False
⊢ (V ∩ ⋂ U ∈ S, interior Uᶜ)ᶜ ∈ 𝓝 x

Tactic:
refine mem_of_superset (hWo.mem_nhds hxW) fun z hzW ⟨hzV, _⟩ ↦ ?_
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
z : X
hzW : z ∈ W
h : z ∈ V ∩ ⋂ U ∈ S, interior Uᶜ
hzV : z ∈ V
right : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) z
⊢ False

Tactic:
disjoint_left.1 hVW hzV hzW

Premises used: Set.disjoint_left, Iff.mp
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
z : X
hzW : z ∈ W
h : z ∈ V ∩ ⋂ U ∈ S, interior Uᶜ
hzV : z ∈ V
right : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) z
⊢ False

Tactic:
exact disjoint_left.1 hVW hzV hzW

Premises used: Set.disjoint_left, Iff.mp
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
U : Set X
hU : U ∈ S
⊢ Disjoint U (V ∩ ⋂ U ∈ S, interior Uᶜ)

Tactic:
disjoint_left.2 fun z hzU ⟨_, hzU'⟩ ↦ interior_subset (mem_iInter₂.1 hzU' U hU) hzU

Premises used: Iff.mpr, False, interior_subset, Set.disjoint_left, Set.mem_iInter₂, Iff.mp, _private.0.exists_seq_infinite_isOpen_pairwise_disjoint.match_5
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this_1 : Std.Symm.{u_1 + 1} (α := Set X) Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) x_1
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : Membership.mem (γ := Set X) (⋂ U ∈ S, interior Uᶜ) y
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst] V
hWo : IsOpen[inst] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
U : Set X
hU : U ∈ S
⊢ Disjoint U (V ∩ ⋂ U ∈ S, interior Uᶜ)

Tactic:
exact disjoint_left.2 fun z hzU ⟨_, hzU'⟩ ↦ interior_subset (mem_iInter₂.1 hzU' U hU) hzU
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
rcases :
  ∀ (U : ℕ → Set X) (hUi : ∀ (n : ℕ), (U n).Infinite) (hUo : ∀ (n : ℕ), IsOpen[inst] (U n))
    (hd : Pairwise (Disjoint on U)), ∃ (f : ℕ → X), IsEmbedding f
⊢ ∃ (f : ℕ → X), IsEmbedding f

Tactic:
rcases exists_seq_infinite_isOpen_pairwise_disjoint X with ⟨U, hUi, hUo, hd⟩

Premises used: exists_seq_infinite_isOpen_pairwise_disjoint
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
choose : ∀ (f : (n : ℕ) → X) (hf : ∀ (n : ℕ), f n ∈ U n), ∃ (f : ℕ → X), IsEmbedding f
⊢ ∃ (f : ℕ → X), IsEmbedding f

Tactic:
choose f hf using fun n ↦ (hUi n).nonempty

Premises used: Set.Infinite.nonempty
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
f : (n : ℕ) → X
hf : ∀ (n : ℕ), f n ∈ U n
⊢ ∃ (f : ℕ → X), IsEmbedding f

Tactic:
⟨f, IsInducing.isEmbedding ⟨Eq.symm (eq_bot_of_singletons_open fun n ↦ ⟨U n, hUo n, ?_⟩)⟩⟩

Premises used: Topology.IsInducing.isEmbedding, Topology.IsInducing.mk, And.intro, Exists.intro, eq_bot_of_singletons_open, Eq.symm
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
f : (n : ℕ) → X
hf : ∀ (n : ℕ), f n ∈ U n
refine : ∀ (n : ℕ), f ⁻¹' U n = {n}
⊢ ∃ (f : ℕ → X), IsEmbedding f

Tactic:
refine ⟨f, IsInducing.isEmbedding ⟨Eq.symm (eq_bot_of_singletons_open fun n ↦ ⟨U n, hUo n, ?_⟩)⟩⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
f : (n : ℕ) → X
hf : ∀ (n : ℕ), f n ∈ U n
n : ℕ
⊢ f ⁻¹' U n = {n}

Tactic:
eq_singleton_iff_unique_mem.2 ⟨hf _, fun m hm ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
f : (n : ℕ) → X
hf : ∀ (n : ℕ), f n ∈ U n
n : ℕ
refine : ∀ (m : ℕ) (hm : m ∈ f ⁻¹' U n), m = n
⊢ f ⁻¹' U n = {n}

Tactic:
refine eq_singleton_iff_unique_mem.2 ⟨hf _, fun m hm ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Set.eq_singleton_iff_unique_mem
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
f : (n : ℕ) → X
hf : ∀ (n : ℕ), f n ∈ U n
n m : ℕ
hm : m ∈ f ⁻¹' U n
⊢ m = n

Tactic:
hd.eq (not_disjoint_iff.2 ⟨f m, hf _, hm⟩)

Premises used: Iff.mpr, Pairwise.eq, Set.not_disjoint_iff, And.intro, Exists.intro
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
U : ℕ → Set X
hUi : ∀ (n : ℕ), (U n).Infinite
hUo : ∀ (n : ℕ), IsOpen[inst] (U n)
hd : Pairwise (Disjoint on U)
f : (n : ℕ) → X
hf : ∀ (n : ℕ), f n ∈ U n
n m : ℕ
hm : m ∈ f ⁻¹' U n
⊢ m = n

Tactic:
exact hd.eq (not_disjoint_iff.2 ⟨f m, hf _, hm⟩)

Premises used: Iff.mpr, Pairwise.eq, Set.not_disjoint_iff, And.intro, Exists.intro
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
rcases : ∀ (f : ℕ → X) (hf : IsEmbedding f), ∃ (s : Set X), s.Infinite ∧ DiscreteTopology.{u_1} (↑s : Type u_1)
⊢ ∃ (s : Set X), s.Infinite ∧ DiscreteTopology.{u_1} (↑s : Type u_1)

Tactic:
rcases exists_topology_isEmbedding_nat X with ⟨f, hf⟩

Premises used: exists_topology_isEmbedding_nat
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
f : ℕ → X
hf : IsEmbedding f
⊢ ∃ (s : Set X), s.Infinite ∧ DiscreteTopology.{u_1} (↑s : Type u_1)

Tactic:
⟨range f, infinite_range_of_injective hf.injective, ?_⟩

Premises used: Set.infinite_range_of_injective, And.intro, Topology.IsEmbedding.injective, Exists.intro, Set.range
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
f : ℕ → X
hf : IsEmbedding f
refine : DiscreteTopology.{u_1} (↑(range f) : Type u_1)
⊢ ∃ (s : Set X), s.Infinite ∧ DiscreteTopology.{u_1} (↑s : Type u_1)

Tactic:
refine ⟨range f, infinite_range_of_injective hf.injective, ?_⟩
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
f : ℕ → X
hf : IsEmbedding f
⊢ DiscreteTopology.{u_1} (↑(range f) : Type u_1)

Tactic:
hf.toHomeomorph.symm.isEmbedding.discreteTopology

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.discreteTopology, Homeomorph.symm, Topology.IsEmbedding.toHomeomorph
-- Module: Mathlib.Topology.NatEmbedding
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
f : ℕ → X
hf : IsEmbedding f
⊢ DiscreteTopology.{u_1} (↑(range f) : Type u_1)

Tactic:
exact hf.toHomeomorph.symm.isEmbedding.discreteTopology

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.discreteTopology, Homeomorph.symm, Topology.IsEmbedding.toHomeomorph
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ 𝓝 x = ⨅ (s : Set X), ⨅ (_ : IsOpen[inst] s), ⨅ (_ : x ∈ s), 𝓟 s

Tactic:
simp only [nhds_def, mem_setOf_eq, @and_comm (x ∈ _), iInf_and]

Premises used: Set.mem_setOf_eq, and_comm, nhds_def, iInf_and
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
rw :
  HasBasis (α := X)
    (⨅ (s : Set X), ⨅ (_ : Membership.mem (γ := Set (Set X)) {s : Set X | x ∈ s ∧ IsOpen[inst] s} s), 𝓟 s)
    (fun (s : Set X) ↦ x ∈ s ∧ IsOpen[inst] s) fun (s : Set X) ↦ s
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ x ∈ s ∧ IsOpen[inst] s) fun (s : Set X) ↦ s

Tactic:
rw [nhds_def]

Premises used: nhds_def
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ HasBasis (α := X)
    (⨅ (s : Set X), ⨅ (_ : Membership.mem (γ := Set (Set X)) {s : Set X | x ∈ s ∧ IsOpen[inst] s} s), 𝓟 s)
    (fun (s : Set X) ↦ x ∈ s ∧ IsOpen[inst] s) fun (s : Set X) ↦ s

Tactic:
hasBasis_biInf_principal
    (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ =>
      ⟨s ∩ t, ⟨⟨has, hat⟩, IsOpen.inter hs ht⟩, ⟨inter_subset_left, inter_subset_right⟩⟩)
    ⟨univ, ⟨mem_univ x, isOpen_univ⟩⟩

Premises used: Filter.hasBasis_biInf_principal, _private.0.nhds_basis_opens.match_1, Set.Mem, Set.univ, setOf, Membership.mem, Exists, GE.ge, Set.inter_subset_left, isOpen_univ, Inter.inter, And, And.intro, IsOpen.inter, Exists.intro, Set.mem_univ, IsOpen, Order.Preimage, Set.inter_subset_right
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ HasBasis (α := X)
    (⨅ (s : Set X), ⨅ (_ : Membership.mem (γ := Set (Set X)) {s : Set X | x ∈ s ∧ IsOpen[inst] s} s), 𝓟 s)
    (fun (s : Set X) ↦ x ∈ s ∧ IsOpen[inst] s) fun (s : Set X) ↦ s

Tactic:
exact hasBasis_biInf_principal
    (fun s ⟨has, hs⟩ t ⟨hat, ht⟩ =>
      ⟨s ∩ t, ⟨⟨has, hat⟩, IsOpen.inter hs ht⟩, ⟨inter_subset_left, inter_subset_right⟩⟩)
    ⟨univ, ⟨mem_univ x, isOpen_univ⟩⟩
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
t : Set X
⊢ (∃ (x_1 : Set X), (x ∈ x_1ᶜ ∧ IsOpen[inst] x_1ᶜ) ∧ x_1ᶜ ⊆ t) ↔ ∃ (i : Set X), (x ∉ i ∧ IsClosed[inst] i) ∧ iᶜ ⊆ t

Tactic:
simp only [isOpen_compl_iff, mem_compl_iff]

Premises used: isOpen_compl_iff, Set.mem_compl_iff
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ (𝓝 x).lift' interior = 𝓝 x

Tactic:
(nhds_basis_opens x).lift'_interior_eq_self fun _ ↦ And.right

Premises used: Filter.HasBasis.lift'_interior_eq_self, And.right, nhds_basis_opens
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
x : X
p : ι → Prop
s : ι → Set X
h : (𝓝 x).HasBasis p s
⊢ (𝓝 x).HasBasis p fun (x : ι) ↦ interior (s x)

Tactic:
lift'_nhds_interior x ▸ h.lift'_interior

Premises used: Eq.rec, Filter.HasBasis.lift'_interior, lift'_nhds_interior
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
f : Filter X
⊢ f ≤ 𝓝 x ↔ ∀ (s : Set X), x ∈ s → IsOpen[inst] s → s ∈ f

Tactic:
simp [nhds_def]

Premises used: nhds_def
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst] s
sf : 𝓟 s ≤ f
rw : ⨅ (s : Set X), ⨅ (_ : Membership.mem (γ := Set (Set X)) {s : Set X | x ∈ s ∧ IsOpen[inst] s} s), 𝓟 s ≤ f
⊢ 𝓝 x ≤ f

Tactic:
rw [nhds_def]

Premises used: nhds_def
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst] s
sf : 𝓟 s ≤ f
⊢ ⨅ (s : Set X), ⨅ (_ : Membership.mem (γ := Set (Set X)) {s : Set X | x ∈ s ∧ IsOpen[inst] s} s), 𝓟 s ≤ f

Tactic:
iInf₂_le_of_le s ⟨h, o⟩ sf

Premises used: Set.Mem, setOf, iInf₂_le_of_le, And.intro
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst] s
sf : 𝓟 s ≤ f
⊢ ⨅ (s : Set X), ⨅ (_ : Membership.mem (γ := Set (Set X)) {s : Set X | x ∈ s ∧ IsOpen[inst] s} s), 𝓟 s ≤ f

Tactic:
exact iInf₂_le_of_le s ⟨h, o⟩ sf

Premises used: iInf₂_le_of_le
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ s ∈ 𝓝 x ↔ ∃ t ⊆ s, IsOpen[inst] t ∧ x ∈ t

Tactic:
(nhds_basis_opens x).mem_iff.trans <| exists_congr fun _ =>
    ⟨fun h => ⟨h.2, h.1.2, h.1.1⟩, fun h => ⟨⟨h.2.2, h.2.1⟩, h.1⟩⟩

Premises used: Filter.HasBasis.mem_iff, exists_congr, And.right, And.left, And.intro, Iff.intro, Iff.trans, nhds_basis_opens
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
p : X → Prop
⊢ (∃ t ⊆ {x : X | (fun (y : X) ↦ p y) x}, IsOpen[inst] t ∧ x ∈ t) ↔
    ∃ (t : Set X), (∀ y ∈ t, p y) ∧ IsOpen[inst] t ∧ x ∈ t

Tactic:
simp only [subset_def, mem_setOf_eq]

Premises used: Set.subset_def, Set.mem_setOf_eq
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
p : X → Prop
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen[inst] i → ∃ x ∈ i, p x) ↔ ∀ (U : Set X), x ∈ U → IsOpen[inst] U → ∃ y ∈ U, p y

Tactic:
simp
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ s ∈ 𝓝 x

Tactic:
mem_interior.trans mem_nhds_iff.symm

Premises used: mem_nhds_iff, Iff.trans, mem_interior, Iff.symm
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : X → α
⊢ map f (𝓝 x) =
    ⨅ (s : Set X), ⨅ (_ : Membership.mem (γ := Set (Set X)) {s : Set X | x ∈ s ∧ IsOpen[inst] s} s), 𝓟 (f '' s)

Tactic:
((nhds_basis_opens x).map f).eq_biInf

Premises used: Set.Mem, setOf, Filter.HasBasis.eq_biInf, Filter.HasBasis.map, nhds_basis_opens
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ s ∈ 𝓝 x → x ∈ s

Tactic:
fun H =>
  let ⟨_t, ht, _, hs⟩ := mem_nhds_iff.1 H; ht hs

Premises used: mem_nhds_iff, Membership.mem, _private.0.mem_of_mem_nhds.match_1, Iff.mp
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
p : X → Prop
h : ∀ᶠ (y : X) in 𝓝 x, p y
⊢ p x

Tactic:
mem_of_mem_nhds h

Premises used: Set.Mem, mem_of_mem_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
hs : IsOpen[inst] s
hx : x ∈ s
⊢ s ∈ 𝓝 x

Tactic:
mem_nhds_iff.2 ⟨s, Subset.refl _, hs, hx⟩

Premises used: Iff.mpr, Set.Subset.refl, mem_nhds_iff, And.intro, Exists.intro
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
hs : IsOpen[inst] s
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
⟨mem_of_mem_nhds, fun hx => mem_nhds_iff.2 ⟨s, Subset.rfl, hs, hx⟩⟩

Premises used: Iff.mpr, mem_nhds_iff, mem_of_mem_nhds, Set.Subset.rfl, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
hs : IsClosed[inst] s
hx : x ∉ s
⊢ sᶜ ∈ 𝓝 x

Tactic:
hs.isOpen_compl.mem_nhds (mem_compl hx)

Premises used: IsClosed.isOpen_compl, IsOpen.mem_nhds, Set.mem_compl
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
hs : IsOpen[inst] s
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝 x, x ∈ s

Tactic:
IsOpen.mem_nhds hs hx

Premises used: Filter.Eventually, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ x ∈ s ∧ IsOpen[inst] s) fun (s : Set X) ↦ s

Tactic:
nhds_basis_opens x

Premises used: nhds_basis_opens
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
h : ∀ (x_1 : Set X), x_1 ∈ 𝓝 x ∧ IsOpen[inst] x_1 ↔ x ∈ x_1 ∧ IsOpen[inst] x_1
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ IsOpen[inst] s) fun (x : Set X) ↦ x

Tactic:
convert! nhds_basis_opens x using 2

Premises used: nhds_basis_opens
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
x_1 : Set X
⊢ x_1 ∈ 𝓝 x ∧ IsOpen[inst] x_1 ↔ x ∈ x_1 ∧ IsOpen[inst] x_1

Tactic:
and_congr_left_iff.2 IsOpen.mem_nhds_iff

Premises used: Iff.mpr, IsOpen.mem_nhds_iff, and_congr_left_iff
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
x_1 : Set X
⊢ x_1 ∈ 𝓝 x ∧ IsOpen[inst] x_1 ↔ x ∈ x_1 ∧ IsOpen[inst] x_1

Tactic:
exact and_congr_left_iff.2 IsOpen.mem_nhds_iff

Premises used: Iff.mpr, IsOpen.mem_nhds_iff, and_congr_left_iff
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s U : Set X
h : ∀ x ∈ s, U ∈ 𝓝 x
⊢ ∃ (V : Set X), s ⊆ V ∧ IsOpen[inst] V ∧ V ⊆ U

Tactic:
⟨interior U, fun x hx => mem_interior_iff_mem_nhds.2 <| h x hx, isOpen_interior, interior_subset⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, interior_subset, isOpen_interior, And.intro, interior, Exists.intro
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
s U : Set X
h : Membership.mem (γ := Filter X) (⨆ x ∈ s, 𝓝 x) U
⊢ ∀ x ∈ s, U ∈ 𝓝 x

Tactic:
simpa using h
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
p : X → Prop
h : ∀ᶠ (y : X) in 𝓝 x, p y
⊢ ∀ᶠ (y : X) in 𝓝 x, ∀ᶠ (x : X) in 𝓝 y, p x

Tactic:
let ⟨t, htp, hto, ha⟩ := eventually_nhds_iff.1 h
  eventually_nhds_iff.2 ⟨t, fun _x hx => eventually_nhds_iff.2 ⟨t, htp, hto, hx⟩, hto, ha⟩

Premises used: Iff.mpr, Filter.Eventually, nhds, _private.0.Filter.Eventually.eventually_nhds.match_1, eventually_nhds_iff, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
p : X → Prop
⊢ (∀ᶠ (y : X) in 𝓝 x, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (x : X) in 𝓝 x, p x

Tactic:
⟨fun h => h.self_of_nhds, fun h => h.eventually_nhds⟩

Premises used: Filter.Eventually.self_of_nhds, Filter.Eventually.eventually_nhds, Iff.intro
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
p : X → Prop
rw : (¬∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ¬∃ᶠ (x : X) in 𝓝 x, p x
⊢ (∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ∃ᶠ (x : X) in 𝓝 x, p x

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
p : X → Prop
⊢ (¬∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ¬∃ᶠ (x : X) in 𝓝 x, p x

Tactic:
simp only [not_frequently, eventually_eventually_nhds]

Premises used: Filter.not_frequently, eventually_eventually_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ (∀ᶠ (x' : X) in 𝓝 x, s ∈ 𝓝 x') ↔ s ∈ 𝓝 x

Tactic:
eventually_eventually_nhds

Premises used: Set.Mem, Filter.Eventually, setOf, eventually_eventually_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ (𝓝 x).bind 𝓝 = 𝓝 x

Tactic:
Filter.ext fun _ => eventually_eventually_nhds

Premises used: Filter.ext, eventually_eventually_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f g : X → α
⊢ (∀ᶠ (y : X) in 𝓝 x, f =ᶠ[𝓝 y] g) ↔ f =ᶠ[𝓝 x] g

Tactic:
eventually_eventually_nhds

Premises used: Filter.EventuallyEq, eventually_eventually_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f g : X → α
h : f =ᶠ[𝓝 x] g
⊢ f x = g x

Tactic:
h.self_of_nhds

Premises used: Filter.Eventually.self_of_nhds
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
inst_1 : LE α
f g : X → α
⊢ (∀ᶠ (y : X) in 𝓝 x, f ≤ᶠ[𝓝 y] g) ↔ f ≤ᶠ[𝓝 x] g

Tactic:
eventually_eventually_nhds

Premises used: eventually_eventually_nhds, Filter.EventuallyLE
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f g : X → α
h : f =ᶠ[𝓝 x] g
⊢ ∀ᶠ (y : X) in 𝓝 x, f =ᶠ[𝓝 y] g

Tactic:
h.eventually_nhds

Premises used: Filter.Eventually.eventually_nhds, Filter.EventuallyEq
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
inst_1 : LE α
f g : X → α
h : f ≤ᶠ[𝓝 x] g
⊢ ∀ᶠ (y : X) in 𝓝 x, f ≤ᶠ[𝓝 y] g

Tactic:
h.eventually_nhds

Premises used: Filter.Eventually.eventually_nhds, Filter.EventuallyLE
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
P : Set X → Prop
hP : ∀ (s t : Set X), s ⊆ t → P s → P t
⊢ (∀ (i : Set X), x ∈ i ∧ IsOpen[inst] i → P i) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → P s

Tactic:
simp only [@and_comm (x ∈ _), and_imp]

Premises used: and_imp, and_comm
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : Set X → Set α
hf : ∀ (s t : Set X), s ⊆ t → f s ⊆ f t
l : Filter α
⊢ (∀ s ∈ 𝓝 x, f s ∈ l) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → f s ∈ l

Tactic:
all_mem_nhds _ _ fun s t ssubt h => mem_of_superset h (hf s t ssubt)

Premises used: all_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
⊢ Tendsto f l (𝓝 x) ↔ ∀ (s : Set X), IsOpen[inst] s → x ∈ s → f ⁻¹' s ∈ l

Tactic:
all_mem_nhds_filter _ _ (fun _ _ h => preimage_mono h) _

Premises used: Set.Mem, setOf, Set.preimage_mono, Set.preimage, Filter.Tendsto, all_mem_nhds_filter
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
inst_1 : Nonempty α
inst_2 : SemilatticeSup α
f : α → X
⊢ (∀ (ib : Set X), x ∈ ib ∧ IsOpen[inst] ib → ∃ (ia : α), True ∧ ∀ x ∈ Ici ia, f x ∈ ib) ↔
    ∀ (U : Set X), x ∈ U → IsOpen[inst] U → ∃ (N : α), ∀ (n : α), N ≤ n → f n ∈ U

Tactic:
simp only [and_imp, true_and, mem_Ici]

Premises used: and_imp, Set.mem_Ici, true_and
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : Filter α
⊢ Tendsto (fun (x_1 : α) ↦ x) f (𝓝 x)

Tactic:
tendsto_nhds.mpr fun _ _ ha => univ_mem' fun _ => ha

Premises used: Iff.mpr, tendsto_nhds, Filter.univ_mem'
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Type u_2
inst_1 : Preorder ι
u : ι → X
i₀ : ι
h : ∀ i ≥ i₀, u i = x
⊢ Tendsto u atTop (𝓝 x)

Tactic:
Tendsto.congr' (EventuallyEq.symm ((eventually_ge_atTop i₀).mono h)) tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Eventually.mono, Filter.eventually_ge_atTop, Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Type u_2
inst_1 : Preorder ι
u : ι → X
i₀ : ι
h : ∀ i ≤ i₀, u i = x
⊢ Tendsto u atBot (𝓝 x)

Tactic:
tendsto_atTop_of_eventually_const (ι := ιᵒᵈ) h

Premises used: setOf, tendsto_atTop_of_eventually_const, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Neighborhoods
Goal:
X : Type u
inst : TopologicalSpace X
⊢ LE.le.{u} (α := X → Filter X) pure 𝓝

Tactic:
fun _ _ hs => mem_pure.2 <| mem_of_mem_nhds hs

Premises used: Iff.mpr, mem_of_mem_nhds, Filter.mem_pure