awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
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
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
have neg : ∀ (V W : Set X) (hVo : IsOpen[inst] V) (hWo : IsOpen[inst] W) (hyV : y ∈ V) (hxW : x ∈ W) (hVW : Disjoint V W),
  ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
Tactic: rcases t2_separation hyx with ⟨V, W, hVo, hWo, hyV, hxW, hVW⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
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
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
have neg : IsOpen[inst] (V ∩ ⋂ U ∈ S, interior Uᶜ)
Tactic: refine ⟨V ∩ ⋂ U ∈ S, interior (Uᶜ), ⟨⟨y, hyV, hyU⟩, ?_, ?_⟩, fun U hU ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
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 : IsOpen[inst] (V ∩ ⋂ U ∈ S, interior Uᶜ)
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
have neg₁ : (V ∩ ⋂ U ∈ S, interior Uᶜ)ᶜ ∈ 𝓝 x
Tactic: refine ⟨V ∩ ⋂ U ∈ S, interior (Uᶜ), ⟨⟨y, hyV, hyU⟩, ?_, ?_⟩, fun U hU ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
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 : IsOpen[inst] (V ∩ ⋂ U ∈ S, interior Uᶜ)
neg₁ : (V ∩ ⋂ U ∈ S, interior Uᶜ)ᶜ ∈ 𝓝 x
⊢ ∃ (y : Set X), (fun (U : Set X) ↦ U.Nonempty ∧ IsOpen[inst] U ∧ Uᶜ ∈ 𝓝 x) y ∧ ∀ x ∈ S, Disjoint x y
have neg₂ : ∀ (U : Set X) (hU : U ∈ S), Disjoint U (V ∩ ⋂ U ∈ S, interior Uᶜ)
Tactic: refine ⟨V ∩ ⋂ U ∈ S, interior (Uᶜ), ⟨⟨y, hyV, hyU⟩, ?_, ?_⟩, fun U hU ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
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
⊢ (V ∩ ⋂ U ∈ S, interior Uᶜ)ᶜ ∈ 𝓝 x
have 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
Tactic: refine mem_of_superset (hWo.mem_nhds hxW) fun z hzW ⟨hzV, _⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
⊢ ∃ (f : ℕ → X), IsEmbedding f
have rcases : ∀ (U : ℕ → Set X) (hUi : ∀ (n : ℕ), (U n).Infinite) (hUo : ∀ (n : ℕ), IsOpen[inst] (U n))
  (hd : Pairwise (Disjoint on U)), ∃ (f : ℕ → X), IsEmbedding f
Tactic: rcases exists_seq_infinite_isOpen_pairwise_disjoint X with ⟨U, hUi, hUo, hd⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
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 : ℕ → X), IsEmbedding f
have choose : ∀ (f : (n : ℕ) → X) (hf : ∀ (n : ℕ), f n ∈ U n), ∃ (f : ℕ → X), IsEmbedding f
Tactic: choose f hf using fun n ↦ (hUi n).nonempty
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
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
have refine : ∀ (n : ℕ), f ⁻¹' U n = {n}
Tactic: refine ⟨f, IsInducing.isEmbedding ⟨Eq.symm (eq_bot_of_singletons_open fun n ↦ ⟨U n, hUo n, ?_⟩)⟩⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
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}
have refine : ∀ (m : ℕ) (hm : m ∈ f ⁻¹' U n), m = n
Tactic: refine eq_singleton_iff_unique_mem.2 ⟨hf _, fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : Infinite X
⊢ ∃ (s : Set X), s.Infinite ∧ DiscreteTopology.{u_1} (↑s : Type u_1)
have rcases : ∀ (f : ℕ → X) (hf : IsEmbedding f), ∃ (s : Set X), s.Infinite ∧ DiscreteTopology.{u_1} (↑s : Type u_1)
Tactic: rcases exists_topology_isEmbedding_nat X with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Topology.NatEmbedding (goal)
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)
have refine : DiscreteTopology.{u_1} (↑(range f) : Type u_1)
Tactic: refine ⟨range f, infinite_range_of_injective hf.injective, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
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
have 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
Tactic: rw [nhds_def]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
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
⊢ 𝓝 x ≤ f
have rw : ⨅ (s : Set X), ⨅ (_ : Membership.mem (γ := Set (Set X)) {s : Set X | x ∈ s ∧ IsOpen[inst] s} s), 𝓟 s ≤ f
Tactic: rw [nhds_def]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ s ∈ 𝓝 x ∧ IsOpen[inst] s) fun (x : Set X) ↦ x
have h : ∀ (x_1 : Set X), x_1 ∈ 𝓝 x ∧ IsOpen[inst] x_1 ↔ x ∈ x_1 ∧ IsOpen[inst] x_1
Tactic: convert! nhds_basis_opens x using 2
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
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
have rw : (¬∃ᶠ (x' : X) in 𝓝 x, ∃ᶠ (x'' : X) in 𝓝 x', p x'') ↔ ¬∃ᶠ (x : X) in 𝓝 x, p x
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s ⊆ interior s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
have simp_rw : s ⊆ {x : X | 𝓝 x ≤ 𝓟 s} ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
Tactic: simp_rw [interior_eq_nhds, subset_def, mem_setOf]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
simp_rw : s ⊆ {x : X | 𝓝 x ≤ 𝓟 s} ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
⊢ s ⊆ interior s ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
have simp_rw₁ : (∀ x ∈ s, Membership.mem (γ := Set X) {x : X | 𝓝 x ≤ 𝓟 s} x) ↔ ∀ x ∈ s, 𝓝 x ≤ 𝓟 s
Tactic: simp_rw [interior_eq_nhds, subset_def, mem_setOf]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
⊢ t = t'
have a : ∀ (x : Set X), IsOpen[t] x ↔ IsOpen[t'] x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u_2
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x : Set X
⊢ IsOpen[t] x ↔ IsOpen[t'] x
have a : (∀ x_1 ∈ x, 𝓝 x_1 ≤ 𝓟 x) ↔ ∀ x_1 ∈ x, 𝓝 x_1 ≤ 𝓟 x
Tactic: simp_rw [@isOpen_iff_nhds _ _ _, H]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ IsOpen[inst] {x} ↔ 𝓝[≠] x = ⊥
have rw : 𝓝 x ≤ pure x ∧ pure x ≤ 𝓝 x ↔ {x} ∈ 𝓝 x
Tactic: rw [isOpen_singleton_iff_nhds_eq_pure, nhdsWithin, ← mem_iff_inf_principal_compl,
      le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst] s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s
have rw : 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]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : x ∈ closure[inst] s ↔ ¬∀ᶠ (x : X) in 𝓝 x, x ∉ s
⊢ x ∈ closure[inst] s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s
have rw₁ : x ∈ closure[inst] s ↔ {x : X | x ∉ s} ∉ 𝓝 x
Tactic: rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
    closure_eq_compl_interior_compl, mem_compl_iff, compl_def]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
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
⊢ x ∈ closure[inst] s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s
have rw₂ : x ∈ closure[inst] s ↔ x ∉ interior {x : X | x ∉ s}
Tactic: rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
    closure_eq_compl_interior_compl, mem_compl_iff, compl_def]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
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}
⊢ x ∈ closure[inst] s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s
have rw₃ : x ∈ (interior sᶜ)ᶜ ↔ x ∉ interior {x : X | x ∉ s}
Tactic: rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
    closure_eq_compl_interior_compl, mem_compl_iff, compl_def]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
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}
⊢ x ∈ closure[inst] s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s
have rw₄ : x ∉ interior sᶜ ↔ x ∉ interior {x : X | x ∉ s}
Tactic: rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
    closure_eq_compl_interior_compl, mem_compl_iff, compl_def]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
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}
⊢ x ∈ closure[inst] s ↔ ∃ᶠ (x : X) in 𝓝 x, x ∈ s
have rw₅ : x ∉ interior {x : X | x ∉ s} ↔ x ∉ interior {x : X | x ∉ s}
Tactic: rw [Filter.Frequently, Filter.Eventually, ← mem_interior_iff_mem_nhds,
    closure_eq_compl_interior_compl, mem_compl_iff, compl_def]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClosed[inst] s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
have rw : closure[inst] s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
Tactic: rw [← closure_subset_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure[inst] s ⊆ s ↔ ∀ (x : X), (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
have refine : ∀ (x : X), x ∈ closure[inst] s → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
Tactic: refine forall_congr' fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ closure[inst] s → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
have rw : (∃ᶠ (x : X) in 𝓝 x, x ∈ s) → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
Tactic: rw [mem_closure_iff_frequently]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ (𝓝[s] x).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty
have 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
Tactic: rw [nhdsWithin, inf_neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : Dense s
ht : IsOpen[inst] t
⊢ t = t ∩ closure[inst] s
have rw : t = t ∩ univ
Tactic: rw [hs.closure_eq, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : Dense s
ht : IsOpen[inst] t
rw : t = t ∩ univ
⊢ t = t ∩ closure[inst] s
have rw₁ : t = t
Tactic: rw [hs.closure_eq, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ Tendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Tendsto f l (𝓝 x)
have rw : l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)
Tactic: rw [tendsto_iff_comap, tendsto_iff_comap]
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (hypothesis)
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ᶜ
⊢ x ∈ U
have this : f x ∈ t
Tactic: have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)
have h₁ : 𝓟 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (goal)
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)
have refine : ∀ (h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)), l ≤ comap f (𝓝 x)
Tactic: refine ⟨fun h' => ?_, le_trans inf_le_left⟩
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (hypothesis)
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 ≤ comap f (𝓝 x)
have this : l ⊓ 𝓟 s ⊔ 𝓟 sᶜ ≤ comap f (𝓝 x)
Tactic: have := sup_le h' h
-- Lean 4 proof step from Mathlib.Topology.Neighborhoods (hypothesis)
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)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x y : X
⊢ Membership.mem (γ := Set X) (nhdsKer {y}) x ↔ x ⤳ y
have rw : x ∈ (𝓝 y).ker ↔ x ⤳ y
Tactic: rw [nhdsKer_singleton_eq_ker_nhds, ker_nhds_eq_specializes, mem_setOf]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x y : X
rw : x ∈ (𝓝 y).ker ↔ x ⤳ y
⊢ Membership.mem (γ := Set X) (nhdsKer {y}) x ↔ x ⤳ y
have rw₁ : Membership.mem (γ := Set X) {y_1 : X | y_1 ⤳ y} x ↔ x ⤳ y
Tactic: rw [nhdsKer_singleton_eq_ker_nhds, ker_nhds_eq_specializes, mem_setOf]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
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
⊢ Membership.mem (γ := Set X) (nhdsKer {y}) x ↔ x ⤳ y
have rw₂ : x ⤳ y ↔ x ⤳ y
Tactic: rw [nhdsKer_singleton_eq_ker_nhds, ker_nhds_eq_specializes, mem_setOf]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsOpen[inst] t
⊢ nhdsKer s ⊆ t
have rw : ⋂₀ {t : Set X | IsOpen[inst] t ∧ s ⊆ t} ⊆ t
Tactic: rw [nhdsKer_def]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ (nhdsKer s) = 𝓝ˢ s
have refine : ∀ (i' : Set X), IsOpen[inst] i' ∧ s ⊆ i' → i' ∈ 𝓝ˢ (nhdsKer s)
Tactic: refine le_antisymm ((hasBasis_nhdsSet _).ge_iff.2 ?_) (nhdsSet_mono subset_nhdsKer)
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
x : X
y : Y
⊢ nhdsKer {(x, y)} = SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {x}) (nhdsKer {y})
have simp_rw : (𝓝 (x, y)).ker = (𝓝 x).ker ×ˢ (𝓝 y).ker
Tactic: simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_prod_eq, ker_prod]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
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
⊢ nhdsKer {(x, y)} = SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {x}) (nhdsKer {y})
have simp_rw₁ : (𝓝 x ×ˢ 𝓝 y).ker = (𝓝 x).ker ×ˢ (𝓝 y).ker
Tactic: simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_prod_eq, ker_prod]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
| nhdsKer (s ×ˢ t)
have rw : ⋃ i ∈ s ×ˢ t, nhdsKer {i}
Tactic: rw [← biUnion_of_singleton (s ×ˢ t), nhdsKer_biUnion]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
⊢ nhdsKer (s ×ˢ t) = ⋃ p ∈ s ×ˢ t, nhdsKer {p}
have conv_lhs : nhdsKer (s ×ˢ t) = ⋃ p ∈ s ×ˢ t, nhdsKer {p}
Tactic: conv_lhs => rw [← biUnion_of_singleton (s ×ˢ t), nhdsKer_biUnion]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
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}
⊢ nhdsKer (s ×ˢ t) = ⋃ p ∈ s ×ˢ t, nhdsKer {p}
have conv_lhs₁ : Eq (α := Set (X × Y)) (⋃ i ∈ s ×ˢ t, nhdsKer {i}) (⋃ p ∈ s ×ˢ t, nhdsKer {p})
Tactic: conv_lhs => rw [← biUnion_of_singleton (s ×ˢ t), nhdsKer_biUnion]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
⊢ Eq (α := Set (X × Y)) (⋃ p ∈ s ×ˢ t, nhdsKer {p})
    (⋃ p ∈ s ×ˢ t, SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {p.1}) (nhdsKer {p.2}))
have 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})
Tactic: congr! with ⟨x, y⟩ _
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
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 : (x, y) ∈ s ×ˢ t
⊢ nhdsKer {(x, y)} = SProd.sprod (α := Set X) (β := Set Y) (nhdsKer {(x, y).1}) (nhdsKer {(x, y).2})
have 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})
Tactic: rw [nhdsKer_pair]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
Y : Type u_3
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
⊢ SProd.sprod (α := Set X) (β := Set Y) (⋃ x ∈ s, nhdsKer {x}) (⋃ y ∈ t, nhdsKer {y}) = nhdsKer s ×ˢ nhdsKer t
have simp_rw : SProd.sprod (α := Set X) (β := Set Y) (nhdsKer (⋃ i ∈ s, {i})) (nhdsKer (⋃ i ∈ t, {i})) = nhdsKer s ×ˢ nhdsKer t
Tactic: simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
p : (i : ι) → X i
⊢ Eq (α := Set ((i : ι) → X i)) (nhdsKer {p}) (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})
have simp_rw : (𝓝 p).ker = Set.pi (α := X) univ fun (i : ι) ↦ (𝓝 (p i)).ker
Tactic: simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_pi, ker_pi]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
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
⊢ Eq (α := Set ((i : ι) → X i)) (nhdsKer {p}) (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})
have simp_rw₁ : Eq (α := Set ((i : ι) → X i)) (ker (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (p i)))
  (Set.pi (α := X) univ fun (i : ι) ↦ (𝓝 (p i)).ker)
Tactic: simp_rw [nhdsKer_singleton_eq_ker_nhds, nhds_pi, ker_pi]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
| nhdsKer (Set.pi (α := X) univ s)
have rw : ⋃ i ∈ Set.pi (α := X) univ s, nhdsKer {i}
Tactic: rw [← biUnion_of_singleton (univ.pi s), nhdsKer_biUnion]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
⊢ nhdsKer (Set.pi (α := X) univ s) = ⋃ p ∈ Set.pi (α := X) univ s, nhdsKer {p}
have conv_lhs : 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]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
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}
⊢ nhdsKer (Set.pi (α := X) univ s) = ⋃ p ∈ Set.pi (α := X) univ s, nhdsKer {p}
have conv_lhs₁ : Eq (α := Set ((i : ι) → X i)) (⋃ i ∈ Set.pi (α := X) univ s, nhdsKer {i}) (⋃ p ∈ Set.pi (α := X) univ s, nhdsKer {p})
Tactic: conv_lhs => rw [← biUnion_of_singleton (univ.pi s), nhdsKer_biUnion]
-- Lean 4 proof step from Mathlib.Topology.NhdsKer (goal)
Goal:
ι : Type u_3
X : ι → Type u_4
inst : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X 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})
have h : ∀ p ∈ Set.pi (α := X) univ s,
  Eq (α := Set ((i : ι) → X i)) (nhdsKer {p}) (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})
Tactic: congr! with p _