awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
p : (i : ι) → 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})
have h : Eq (α := Set ((i : ι) → X i)) (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})
  (Set.pi (α := X) univ fun (i : ι) ↦ nhdsKer {p i})
Tactic: rw [nhdsKer_singleton_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)
⊢ 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))
have 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))
Tactic: simp_rw [← nhdsKer_biUnion, biUnion_of_singleton]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_4
inst : TopologicalSpace (X × X)
⊢ 𝓝ˢ (diagonal X) = ⨆ (x : X), 𝓝 (x, x)
have rw : Eq.{u_4 + 1} (α := Filter (X × X)) (sSup (range (ι := X) (𝓝 ∘ fun (x : X) ↦ (x, x)))) (⨆ (x : X), 𝓝 (x, x))
Tactic: rw [nhdsSet, ← range_diag, ← range_comp]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ s ∈ 𝓝ˢ t ↔ ∀ x ∈ t, s ∈ 𝓝 x
have simp_rw : s ∈ sSup (𝓝 '' t) ↔ ∀ x ∈ t, s ∈ 𝓝 x
Tactic: simp_rw [nhdsSet, Filter.mem_sSup, forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
simp_rw : s ∈ sSup (𝓝 '' t) ↔ ∀ x ∈ t, s ∈ 𝓝 x
⊢ s ∈ 𝓝ˢ t ↔ ∀ x ∈ t, s ∈ 𝓝 x
have simp_rw₁ : (∀ f ∈ 𝓝 '' t, s ∈ f) ↔ ∀ x ∈ t, s ∈ 𝓝 x
Tactic: simp_rw [nhdsSet, Filter.mem_sSup, forall_mem_image]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ s ⊆ interior t ↔ t ∈ 𝓝ˢ s
have simp_rw : s ⊆ interior t ↔ ∀ x ∈ s, t ∈ 𝓝 x
Tactic: simp_rw [mem_nhdsSet_iff_forall, subset_interior_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure[inst] s) t
have rw : sᶜ ∈ 𝓝ˢ t ↔ Disjoint (closure[inst] s) t
Tactic: rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
    subset_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
rw : sᶜ ∈ 𝓝ˢ t ↔ Disjoint (closure[inst] s) t
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure[inst] s) t
have rw₁ : t ⊆ interior sᶜ ↔ Disjoint (closure[inst] s) t
Tactic: rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
    subset_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
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
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure[inst] s) t
have rw₂ : t ⊆ (closure[inst] s)ᶜ ↔ Disjoint (closure[inst] s) t
Tactic: rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
    subset_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
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
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure[inst] s) t
have rw₃ : Disjoint (closure[inst] s) t ↔ Disjoint (closure[inst] s) t
Tactic: rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
    subset_compl_iff_disjoint_left]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure[inst] t)
have rw : Disjoint (𝓟 t) (𝓝ˢ s) ↔ Disjoint s (closure[inst] t)
Tactic: rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
rw : Disjoint (𝓟 t) (𝓝ˢ s) ↔ Disjoint s (closure[inst] t)
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure[inst] t)
have rw₁ : Disjoint (closure[inst] t) s ↔ Disjoint s (closure[inst] t)
Tactic: rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
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)
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure[inst] t)
have rw₂ : Disjoint s (closure[inst] t) ↔ Disjoint s (closure[inst] t)
Tactic: rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
⊢ s ∈ 𝓝ˢ t ↔ ∃ (U : Set X), IsOpen[inst] U ∧ t ⊆ U ∧ U ⊆ s
have rw : t ⊆ interior s ↔ ∃ (U : Set X), IsOpen[inst] U ∧ t ⊆ U ∧ U ⊆ s
Tactic: rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
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
⊢ s ∈ 𝓝ˢ t ↔ ∃ (U : Set X), IsOpen[inst] U ∧ t ⊆ U ∧ U ⊆ s
have rw₁ : (∃ (U : Set X), IsOpen[inst] U ∧ t ⊆ U ∧ U ⊆ s) ↔ ∃ (U : Set X), IsOpen[inst] U ∧ t ⊆ U ∧ U ⊆ s
Tactic: rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hU : IsOpen[inst] s
⊢ s ∈ 𝓝ˢ t ↔ t ⊆ s
have rw : t ⊆ interior s ↔ t ⊆ s
Tactic: rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
hU : IsOpen[inst] s
rw : t ⊆ interior s ↔ t ⊆ s
⊢ s ∈ 𝓝ˢ t ↔ t ⊆ s
have rw₁ : t ⊆ s ↔ t ⊆ s
Tactic: rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen[inst] s
have rw : 𝓝ˢ s ≤ 𝓟 s ↔ IsOpen[inst] s
Tactic: rw [← principal_le_nhdsSet.ge_iff_eq', le_principal_iff, mem_nhdsSet_iff_forall,
    isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
rw : 𝓝ˢ s ≤ 𝓟 s ↔ IsOpen[inst] s
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen[inst] s
have rw₁ : s ∈ 𝓝ˢ s ↔ IsOpen[inst] s
Tactic: rw [← principal_le_nhdsSet.ge_iff_eq', le_principal_iff, mem_nhdsSet_iff_forall,
    isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
rw : 𝓝ˢ s ≤ 𝓟 s ↔ IsOpen[inst] s
rw₁ : s ∈ 𝓝ˢ s ↔ IsOpen[inst] s
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen[inst] s
have rw₂ : (∀ x ∈ s, s ∈ 𝓝 x) ↔ IsOpen[inst] s
Tactic: rw [← principal_le_nhdsSet.ge_iff_eq', le_principal_iff, mem_nhdsSet_iff_forall,
    isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
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
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen[inst] s
have rw₃ : (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ x ∈ s, s ∈ 𝓝 x
Tactic: rw [← principal_le_nhdsSet.ge_iff_eq', le_principal_iff, mem_nhdsSet_iff_forall,
    isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ Eq.{u_2 + 1} (α := Filter X) (𝓝ˢ ∅) ⊥
have rw : Eq.{u_2 + 1} (α := Filter X) (𝓟 ∅) ⊥
Tactic: rw [isOpen_empty.nhdsSet_eq, principal_empty]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
rw : Eq.{u_2 + 1} (α := Filter X) (𝓟 ∅) ⊥
⊢ Eq.{u_2 + 1} (α := Filter X) (𝓝ˢ ∅) ⊥
have rw₁ : Eq.{u_2 + 1} (α := Filter X) ⊥ ⊥
Tactic: rw [isOpen_empty.nhdsSet_eq, principal_empty]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
⊢ Eq.{u_2 + 1} (α := Filter X) (𝓝ˢ univ) ⊤
have rw : Eq.{u_2 + 1} (α := Filter X) (𝓟 univ) ⊤
Tactic: rw [isOpen_univ.nhdsSet_eq, principal_univ]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
rw : Eq.{u_2 + 1} (α := Filter X) (𝓟 univ) ⊤
⊢ Eq.{u_2 + 1} (α := Filter X) (𝓝ˢ univ) ⊤
have rw₁ : Eq.{u_2 + 1} (α := Filter X) ⊤ ⊤
Tactic: rw [isOpen_univ.nhdsSet_eq, principal_univ]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)
have rw : s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂
Tactic: rw [nhdsSet_union]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
s : Set X
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s
have rw : 𝓝ˢ ({x} ∪ s) = 𝓝 x ⊔ 𝓝ˢ s
Tactic: rw [insert_eq, nhdsSet_union, nhdsSet_singleton]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
s : Set X
rw : 𝓝ˢ ({x} ∪ s) = 𝓝 x ⊔ 𝓝ˢ s
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s
have rw₁ : 𝓝ˢ {x} ⊔ 𝓝ˢ s = 𝓝 x ⊔ 𝓝ˢ s
Tactic: rw [insert_eq, nhdsSet_union, nhdsSet_singleton]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
x : X
s : Set X
rw : 𝓝ˢ ({x} ∪ s) = 𝓝 x ⊔ 𝓝ˢ s
rw₁ : 𝓝ˢ {x} ⊔ 𝓝ˢ s = 𝓝 x ⊔ 𝓝ˢ s
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s
have rw₂ : 𝓝 x ⊔ 𝓝ˢ s = 𝓝 x ⊔ 𝓝ˢ s
Tactic: rw [insert_eq, nhdsSet_union, nhdsSet_singleton]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
⊢ 𝓝ˢ s = 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ)
have rw : 𝓝ˢ s = 𝓝ˢ s
Tactic: rw [Set.inter_union_compl s t]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
⊢ 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)
have rw : 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)
Tactic: rw [nhdsSet_union]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ) ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ
have nth_grw : 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ
Tactic: nth_grw 2 [inter_subset_right]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ = 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
have rw : 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ = 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
Tactic: rw [h.isOpen_compl.nhdsSet_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
h : IsClosed[inst] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (t ∩ s) ⊔ 𝓟 tᶜ
have rw : 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ
Tactic: rw [Set.inter_comm]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
s t : Set X
p : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x
have rw : (∀ᶠ (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]
-- Lean 4 proof step from Mathlib.Topology.NhdsSet (goal)
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
⊢ (∀ᶠ (x : X) in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x
have 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
Tactic: rw [nhdsSet_union, eventually_sup]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x) ↔ ∀ᶠ (x : α) in 𝓝[s] a, p x
have refine : ∀ (h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x), ∀ᶠ (x : α) in 𝓝[s] a, p x
Tactic: refine ⟨fun h => ?_, fun h => (eventually_nhds_nhdsWithin.2 h).filter_mono inf_le_left⟩
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
p : α → Prop
h : ∀ᶠ (y : α) in 𝓝[s] a, ∀ᶠ (x : α) in 𝓝[s] y, p x
⊢ ∀ᶠ (x : α) in 𝓝[s] a, p x
have simp : ∀ (h : ∀ᶠ (x : α) in 𝓝 a, x ∈ s → ∀ᶠ (x : α) in 𝓝 x, x ∈ s → p x), ∀ᶠ (x : α) in 𝓝 a, x ∈ s → p x
Tactic: simp only [eventually_nhdsWithin_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
⊢ 𝓝[univ] a = 𝓝 a
have rw : 𝓝 a ⊓ 𝓟 univ = 𝓝 a
Tactic: rw [nhdsWithin, principal_univ, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝 a ⊓ 𝓟 univ = 𝓝 a
⊢ 𝓝[univ] a = 𝓝 a
have rw₁ : 𝓝 a ⊓ ⊤ = 𝓝 a
Tactic: rw [nhdsWithin, principal_univ, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝 a ⊓ 𝓟 univ = 𝓝 a
rw₁ : 𝓝 a ⊓ ⊤ = 𝓝 a
⊢ 𝓝[univ] a = 𝓝 a
have rw₂ : 𝓝 a = 𝓝 a
Tactic: rw [nhdsWithin, principal_univ, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s \ t' ∈ 𝓝[t \ t'] x
have rw : s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ
Tactic: rw [nhdsWithin, diff_eq, diff_eq, ← inf_principal, ← inf_assoc]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
⊢ t ∈ 𝓝 a
have rcases : ∀ (w : Set α) (Hw : w ∈ 𝓝 a) (hw : w ∩ s ⊆ t), t ∈ 𝓝 a
Tactic: rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
x : α
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t
have simp_rw : (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ s =ᶠ[𝓝 x] s ∩ t
Tactic: simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
x : α
simp_rw : (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ s =ᶠ[𝓝 x] s ∩ t
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t
have simp_rw₁ : (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ ∀ᶠ (x : α) in 𝓝 x, x ∈ s ↔ x ∈ s ∩ t
Tactic: simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
x : α
simp_rw : (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ s =ᶠ[𝓝 x] s ∩ t
simp_rw₁ : (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ ∀ᶠ (x : α) in 𝓝 x, x ∈ s ↔ x ∈ s ∩ t
⊢ t ∈ 𝓝[s] x ↔ s =ᶠ[𝓝 x] s ∩ t
have simp_rw₂ : (∀ᶠ (y : α) in 𝓝 x, y ∈ s → y ∈ t) ↔ ∀ᶠ (x : α) in 𝓝 x, x ∈ s ↔ x ∈ s ∧ x ∈ t
Tactic: simp_rw [mem_nhdsWithin_iff_eventually, eventuallyEq_set, mem_inter_iff, iff_self_and]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
hs : s ∈ 𝓝 (X a)
⊢ X ⁻¹' s ∈ 𝓝[t] a
have lift : ∀ (a : { x : α // x ∈ t }) (hs : s ∈ 𝓝 (X (↑a : α))), X ⁻¹' s ∈ 𝓝[t] (↑a : α)
Tactic: lift a to t using h
Cleared hypotheses: a, h, hs
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : { x : α // x ∈ t }
hs : s ∈ 𝓝 (X (↑a : α))
⊢ X ⁻¹' s ∈ 𝓝[t] (↑a : α)
have hs₁ : (fun (x : (↑t : Type u_1)) ↦ X (↑x : α)) ⁻¹' s ∈ 𝓝 a
Tactic: replace hs : (fun x : t => X x) ⁻¹' s ∈ 𝓝 a := preimage_nhds_coinduced hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : { x : α // x ∈ t }
hs : (fun (x : (↑t : Type u_1)) ↦ X (↑x : α)) ⁻¹' s ∈ 𝓝 a
⊢ X ⁻¹' s ∈ 𝓝[t] (↑a : α)
have rwa : X ⁻¹' s ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (𝓝 a)
Tactic: rwa [← map_nhds_subtype_val, mem_map]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : { x : α // x ∈ t }
hs : (fun (x : (↑t : Type u_1)) ↦ X (↑x : α)) ⁻¹' s ∈ 𝓝 a
rwa : X ⁻¹' s ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (𝓝 a)
⊢ X ⁻¹' s ∈ 𝓝[t] (↑a : α)
have rwa₁ : Subtype.val (p := fun (x : α) ↦ x ∈ t) ⁻¹' X ⁻¹' s ∈ 𝓝 a
Tactic: rwa [← map_nhds_subtype_val, mem_map]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝 a
have rw : 𝓝[s] a ≤ 𝓝[univ] a
Tactic: rw [← nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝[univ] a
have h : univ ∈ 𝓝[s] a
Tactic: apply nhdsWithin_le_of_mem
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a
have rw : 𝓝[t ∩ s] a = 𝓝[u] a
Tactic: rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
rw : 𝓝[t ∩ s] a = 𝓝[u] a
⊢ 𝓝[t] a = 𝓝[u] a
have rw₁ : 𝓝[t ∩ s] a = 𝓝[u ∩ s] a
Tactic: rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
rw : 𝓝[t ∩ s] a = 𝓝[u] a
rw₁ : 𝓝[t ∩ s] a = 𝓝[u ∩ s] a
⊢ 𝓝[t] a = 𝓝[u] a
have rw₂ : 𝓝[u ∩ s] a = 𝓝[u ∩ s] a
Tactic: rw [nhdsWithin_restrict' t hs, nhdsWithin_restrict' u hs, h₂]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen[inst] s
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a
have rw : 𝓝[t ∩ s] a = 𝓝[u] a
Tactic: rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen[inst] s
h₂ : t ∩ s = u ∩ s
rw : 𝓝[t ∩ s] a = 𝓝[u] a
⊢ 𝓝[t] a = 𝓝[u] a
have rw₁ : 𝓝[t ∩ s] a = 𝓝[u ∩ s] a
Tactic: rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t u : Set α
h₀ : a ∈ s
h₁ : IsOpen[inst] s
h₂ : t ∩ s = u ∩ s
rw : 𝓝[t ∩ s] a = 𝓝[u] a
rw₁ : 𝓝[t ∩ s] a = 𝓝[u ∩ s] a
⊢ 𝓝[t] a = 𝓝[u] a
have rw₂ : 𝓝[u ∩ s] a = 𝓝[u ∩ s] a
Tactic: rw [nhdsWithin_restrict t h₀ h₁, nhdsWithin_restrict u h₀ h₁, h₂]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
X : α → β
s : Set β
t : Set α
a : α
h : a ∈ t
ht : IsOpen[inst] t
hs : s ∈ 𝓝 (X a)
⊢ X ⁻¹' s ∈ 𝓝 a
have rw : X ⁻¹' s ∈ 𝓝[t] a
Tactic: rw [← ht.nhdsWithin_eq h]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
⊢ 𝓝[∅] a = ⊥
have rw : 𝓝 a ⊓ 𝓟 ∅ = ⊥
Tactic: rw [nhdsWithin, principal_empty, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝 a ⊓ 𝓟 ∅ = ⊥
⊢ 𝓝[∅] a = ⊥
have rw₁ : 𝓝 a ⊓ ⊥ = ⊥
Tactic: rw [nhdsWithin, principal_empty, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝 a ⊓ 𝓟 ∅ = ⊥
rw₁ : 𝓝 a ⊓ ⊥ = ⊥
⊢ 𝓝[∅] a = ⊥
have rw₂ : Eq.{u_1 + 1} (α := Filter α) ⊥ ⊥
Tactic: rw [nhdsWithin, principal_empty, inf_bot_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t
have rw : 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ (𝓟 s ⊔ 𝓟 t)
Tactic: rw [← inf_sup_left, sup_principal]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
rw : 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ (𝓟 s ⊔ 𝓟 t)
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t
have rw₁ : 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 (s ∪ t)
Tactic: rw [← inf_sup_left, sup_principal]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
b : α
I₁ I₂ : Set α
hI : univ = I₁ ∪ I₂
⊢ 𝓝 b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
have rw : 𝓝[univ] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
Tactic: rw [← nhdsWithin_univ b, hI, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
b : α
I₁ I₂ : Set α
hI : univ = I₁ ∪ I₂
rw : 𝓝[univ] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
⊢ 𝓝 b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
have rw₁ : 𝓝[I₁ ∪ I₂] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
Tactic: rw [← nhdsWithin_univ b, hI, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
b : α
I₁ I₂ : Set α
hI : univ = I₁ ∪ I₂
rw : 𝓝[univ] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
rw₁ : 𝓝[I₁ ∪ I₂] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
⊢ 𝓝 b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
have rw₂ : 𝓝[I₁] b ⊔ 𝓝[I₂] b = 𝓝[I₁] b ⊔ 𝓝[I₂] b
Tactic: rw [← nhdsWithin_univ b, hI, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
b : α
I₁ I₂ : Set α
h : univ = I₁ ∪ I₂
L : Set α
hL : L ∈ 𝓝[I₁] b
R : Set α
hR : R ∈ 𝓝[I₂] b
⊢ L ∪ R ∈ 𝓝 b
have rw : L ∪ R ∈ 𝓝[I₁] b ⊔ 𝓝[I₂] b
Tactic: rw [← nhdsWithin_univ b, h, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
x : α
⊢ 𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x
have rw : 𝓝[Iio x ∪ Ioi x] x = 𝓝[<] x ⊔ 𝓝[>] x
Tactic: rw [← Iio_union_Ioi, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
x : α
rw : 𝓝[Iio x ∪ Ioi x] x = 𝓝[<] x ⊔ 𝓝[>] x
⊢ 𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x
have rw₁ : 𝓝[<] x ⊔ 𝓝[>] x = 𝓝[<] x ⊔ 𝓝[>] x
Tactic: rw [← Iio_union_Ioi, nhdsWithin_union]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_5
I : Set ι
hI : I.Finite
s : ι → Set α
a : α
⊢ 𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a
have empty : 𝓝[⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), s i] a =
  ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), 𝓝[s i] a
Tactic: induction I, hI using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hT => simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_5
I : Set ι
hI : I.Finite
s : ι → Set α
a : α
empty :
  𝓝[⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ i), s i] a =
    ⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ i), 𝓝[s i] a
⊢ 𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a
have insert : ∀ {a_1 : ι} {s_1 : Set ι},
  a_1 ∉ s_1 →
    s_1.Finite →
      ∀ (hT : 𝓝[⋃ i ∈ s_1, s i] a = ⨆ i ∈ s_1, 𝓝[s i] a),
        𝓝[⋃ i ∈ insert a_1 s_1, s i] a = ⨆ i ∈ insert a_1 s_1, 𝓝[s i] a
Tactic: induction I, hI using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hT => simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Set α)
hS : S.Finite
a : α
⊢ 𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a
have rw : 𝓝[⋃ i ∈ S, i] a = ⨆ s ∈ S, 𝓝[s] a
Tactic: rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
S : Set (Set α)
hS : S.Finite
a : α
rw : 𝓝[⋃ i ∈ S, i] a = ⨆ s ∈ S, 𝓝[s] a
⊢ 𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a
have rw₁ : Eq.{u_1 + 1} (α := Filter α) (⨆ i ∈ S, 𝓝[i] a) (⨆ s ∈ S, 𝓝[s] a)
Tactic: rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]