awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_5
inst_1 : Finite ι
s : ι → Set α
a : α
⊢ 𝓝[⋃ (i : ι), s i] a = ⨆ (i : ι), 𝓝[s i] a
have rw : 𝓝[⋃₀ range s] a = ⨆ (i : ι), 𝓝[s i] a
Tactic: rw [← sUnion_range, nhdsWithin_sUnion (finite_range s), iSup_range]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_5
inst_1 : Finite ι
s : ι → Set α
a : α
rw : 𝓝[⋃₀ range s] a = ⨆ (i : ι), 𝓝[s i] a
⊢ 𝓝[⋃ (i : ι), s i] a = ⨆ (i : ι), 𝓝[s i] a
have rw₁ : Eq.{u_1 + 1} (α := Filter α) (⨆ s_1 ∈ range s, 𝓝[s_1] a) (⨆ (i : ι), 𝓝[s i] a)
Tactic: rw [← sUnion_range, nhdsWithin_sUnion (finite_range s), iSup_range]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_5
inst_1 : Finite ι
s : ι → Set α
a : α
rw : 𝓝[⋃₀ range s] a = ⨆ (i : ι), 𝓝[s i] a
rw₁ : Eq.{u_1 + 1} (α := Filter α) (⨆ s_1 ∈ range s, 𝓝[s_1] a) (⨆ (i : ι), 𝓝[s i] a)
⊢ 𝓝[⋃ (i : ι), s i] a = ⨆ (i : ι), 𝓝[s i] a
have rw₂ : Eq.{u_1 + 1} (α := Filter α) (⨆ (i : ι), 𝓝[s i] a) (⨆ (i : ι), 𝓝[s i] a)
Tactic: rw [← sUnion_range, nhdsWithin_sUnion (finite_range s), iSup_range]
-- 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 ⊓ (𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t)
Tactic: rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
rw : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t)
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)
have rw₁ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t))
Tactic: rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
rw : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t)
rw₁ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t))
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)
have rw₂ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 (s ∩ t))
Tactic: rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
rw : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t)
rw₁ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t))
rw₂ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 (s ∩ t))
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)
have rw₃ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓝 a ⊓ 𝓟 (s ∩ t)
Tactic: rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
rw : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t)
rw₁ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t))
rw₂ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ (𝓝 a ⊓ 𝓟 (s ∩ t))
rw₃ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓝 a ⊓ 𝓟 (s ∩ t)
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ (𝓝 a ⊓ 𝓟 t)
have rw₄ : 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 (s ∩ t)
Tactic: rw [inf_left_comm, inf_assoc, inf_principal, ← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t
have rw : 𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t
Tactic: rw [← inf_principal, inf_assoc]
-- 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 ⊓ 𝓟 t
have rw₁ : 𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t) = 𝓝 a ⊓ (𝓟 s ⊓ 𝓟 t)
Tactic: rw [← inf_principal, inf_assoc]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : s ∈ 𝓝[t] a
⊢ 𝓝[s ∩ t] a = 𝓝[t] a
have rw : 𝓝[t] a ≤ 𝓝[s] a
Tactic: rw [nhdsWithin_inter, inf_eq_right]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ 𝓝[s ∩ t] a = 𝓝[s] a
have rw : 𝓝[t ∩ s] a = 𝓝[s] a
Tactic: rw [inter_comm, nhdsWithin_inter_of_mem h]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
rw : 𝓝[t ∩ s] a = 𝓝[s] a
⊢ 𝓝[s ∩ t] a = 𝓝[s] a
have rw₁ : 𝓝[s] a = 𝓝[s] a
Tactic: rw [inter_comm, nhdsWithin_inter_of_mem h]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
⊢ 𝓝[{a}] a = pure a
have rw : 𝓝 a ⊓ 𝓟 {a} = pure a
Tactic: rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝 a ⊓ 𝓟 {a} = pure a
⊢ 𝓝[{a}] a = pure a
have rw₁ : 𝓝 a ⊓ pure a = pure a
Tactic: rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝 a ⊓ 𝓟 {a} = pure a
rw₁ : 𝓝 a ⊓ pure a = pure a
⊢ 𝓝[{a}] a = pure a
have rw₂ : Eq (α := Filter α) (pure a) (pure a)
Tactic: rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a
have rw : 𝓝[{a} ∪ s] a = pure a ⊔ 𝓝[s] a
Tactic: rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
rw : 𝓝[{a} ∪ s] a = pure a ⊔ 𝓝[s] a
⊢ 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a
have rw₁ : 𝓝[{a}] a ⊔ 𝓝[s] a = pure a ⊔ 𝓝[s] a
Tactic: rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
s : Set α
rw : 𝓝[{a} ∪ s] a = pure a ⊔ 𝓝[s] a
rw₁ : 𝓝[{a}] a ⊔ 𝓝[s] a = pure a ⊔ 𝓝[s] a
⊢ 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a
have rw₂ : pure a ⊔ 𝓝[s] a = pure a ⊔ 𝓝[s] a
Tactic: rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
⊢ 𝓝[≠] a ⊔ pure a = 𝓝 a
have rw : 𝓝[≠] a ⊔ 𝓝[{a}] a = 𝓝 a
Tactic: rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝[≠] a ⊔ 𝓝[{a}] a = 𝓝 a
⊢ 𝓝[≠] a ⊔ pure a = 𝓝 a
have rw₁ : 𝓝[{a}ᶜ ∪ {a}] a = 𝓝 a
Tactic: rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝[≠] a ⊔ 𝓝[{a}] a = 𝓝 a
rw₁ : 𝓝[{a}ᶜ ∪ {a}] a = 𝓝 a
⊢ 𝓝[≠] a ⊔ pure a = 𝓝 a
have rw₂ : 𝓝[univ] a = 𝓝 a
Tactic: rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝[≠] a ⊔ 𝓝[{a}] a = 𝓝 a
rw₁ : 𝓝[{a}ᶜ ∪ {a}] a = 𝓝 a
rw₂ : 𝓝[univ] a = 𝓝 a
⊢ 𝓝[≠] a ⊔ pure a = 𝓝 a
have rw₃ : 𝓝 a = 𝓝 a
Tactic: rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
⊢ pure a ⊔ 𝓝[≠] a = 𝓝 a
have rw : 𝓝[≠] a ⊔ pure a = 𝓝 a
Tactic: rw [← sup_comm, nhdsNE_sup_pure]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
a : α
rw : 𝓝[≠] a ⊔ pure a = 𝓝 a
⊢ pure a ⊔ 𝓝[≠] a = 𝓝 a
have rw₁ : 𝓝 a = 𝓝 a
Tactic: rw [← sup_comm, nhdsNE_sup_pure]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)
have rw : u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b
Tactic: rw [nhdsWithin_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
x : α
s t : Set α
hst : s =ᶠ[𝓝 x] t
h : x ∈ interior s
⊢ x ∈ interior t
have hst₁ : 𝓝[s] x = 𝓝[t] x
Tactic: rw [← nhdsWithin_eq_iff_eventuallyEq] at hst
Cleared hypotheses: hst, h
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ 𝓝[I.pi (α := X) s] x =
    (⨅ i ∈ I, comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝[s i] x i)) ⊓
      ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i))
have simp : Eq (α := Filter ((i : ι) → X i)) ((⨅ (i : ι), comap (eval (β := X) i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval (β := X) i ⁻¹' s i))
  ((⨅ i ∈ I, comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun (x : (i : ι) → X i) ↦ x i) ⁻¹' s i)) ⊓
    ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)))
Tactic: simp only [nhdsWithin, nhds_pi, Filter.pi, pi_def, ← iInf_principal_finite hI, comap_inf,
    comap_principal]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
ι : Type u_5
X : ι → Type u_6
inst : (i : ι) → TopologicalSpace (X i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (X i)
x : (i : ι) → X i
⊢ Eq (α := Filter ((i : ι) → X i))
    ((⨅ (i : ι), comap (eval (β := X) i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval (β := X) i ⁻¹' s i))
    ((⨅ i ∈ I, comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun (x : (i : ι) → X i) ↦ x i) ⁻¹' s i)) ⊓
      ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)))
have rw : Eq (α := Filter ((i : ι) → X i))
  (((⨅ i ∈ I, comap (eval (β := X) i) (𝓝 (x i))) ⊓ ⨅ i ∈ I, 𝓟 (eval (β := X) i ⁻¹' s i)) ⊓
    ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (eval (β := X) i) (𝓝 (x i)))
  ((⨅ i ∈ I, comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)) ⊓ 𝓟 ((fun (x : (i : ι) → X i) ↦ x i) ⁻¹' s i)) ⊓
    ⨅ (i : ι), ⨅ (_ : i ∉ I), comap (fun (x : (i : ι) → X i) ↦ x i) (𝓝 (x i)))
Tactic: rw [iInf_split _ fun i => i ∈ I, inf_right_comm]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
t : Set α
inst_1 : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto (t.piecewise (β := fun (a : α) ↦ β) f g) (𝓝[s] a) l
have h₂ : Tendsto f (𝓝[s] a ⊓ 𝓟 t) l
Tactic: apply Tendsto.piecewise
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
t : Set α
inst_1 : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
h₂ : Tendsto f (𝓝[s] a ⊓ 𝓟 t) l
⊢ Tendsto (t.piecewise (β := fun (a : α) ↦ β) f g) (𝓝[s] a) l
have h₃ : Tendsto g (𝓝[s] a ⊓ 𝓟 tᶜ) l
Tactic: apply Tendsto.piecewise
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ᶠ (i : β) in l, f i ∈ s
have h₁ : ∀ (i : Set α) (i_1 : a ∈ i ∧ IsOpen[inst] i), (∀ᶠ (x : β) in l, f x ∈ i) ∧ ∀ᶠ (x : β) in l, f x ∈ s
Tactic: simp_rw [nhdsWithin_eq, tendsto_iInf, mem_setOf_eq, tendsto_principal, mem_inter_iff,
    eventually_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
ι : Type u_5
X : ι → Type u_6
Y : ι → Type u_7
inst : (i : ι) → TopologicalSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), DenseRange (f i)
⊢ DenseRange (Pi.map (α := X) (β := Y) f)
have rw : Dense (X := (i : ι) → Y i) (Set.pi (α := Y) univ fun (i : ι) ↦ range (f i))
Tactic: rw [DenseRange, Set.range_piMap]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f g : α → β
a : α
h₁ : f =ᶠ[𝓝[≠] a] g
h₂ : f a = g a
⊢ f =ᶠ[𝓝 a] g
have h : ∀ (a_1 : α), (Membership.mem (γ := Set α) {a}ᶜ a_1 → f a_1 = g a_1) → f a_1 = g a_1
Tactic: filter_upwards [eventually_nhdsWithin_iff.1 h₁]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : { x : α // x ∈ s }
t u : Set { x : α // x ∈ s }
⊢ t ∈ 𝓝[u] a ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
have rw : t ∈ 𝓝 a ⊓ 𝓟 u ↔
  Membership.mem (γ := Filter { x : α // x ∈ s })
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
Tactic: rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : { x : α // x ∈ s }
t u : Set { x : α // x ∈ s }
rw :
  t ∈ 𝓝 a ⊓ 𝓟 u ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
⊢ t ∈ 𝓝[u] a ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
have rw₁ : t ∈ comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α)) ⊓ 𝓟 u ↔
  Membership.mem (γ := Filter { x : α // x ∈ s })
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
Tactic: rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : { x : α // x ∈ s }
t u : Set { x : α // x ∈ s }
rw :
  t ∈ 𝓝 a ⊓ 𝓟 u ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₁ :
  t ∈ comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α)) ⊓ 𝓟 u ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
⊢ t ∈ 𝓝[u] a ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
have rw₂ : Membership.mem (γ := Filter { x : α // x ∈ s })
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α)) ⊓
      comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u)))
    t ↔
  Membership.mem (γ := Filter { x : α // x ∈ s })
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
Tactic: rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : { x : α // x ∈ s }
t u : Set { x : α // x ∈ s }
rw :
  t ∈ 𝓝 a ⊓ 𝓟 u ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₁ :
  t ∈ comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α)) ⊓ 𝓟 u ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₂ :
  Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α)) ⊓
        comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u)))
      t ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
⊢ t ∈ 𝓝[u] a ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
have rw₃ : Membership.mem (γ := Filter { x : α // x ∈ s })
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α) ⊓ 𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u))) t ↔
  Membership.mem (γ := Filter { x : α // x ∈ s })
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
Tactic: rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : { x : α // x ∈ s }
t u : Set { x : α // x ∈ s }
rw :
  t ∈ 𝓝 a ⊓ 𝓟 u ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₁ :
  t ∈ comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α)) ⊓ 𝓟 u ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₂ :
  Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α)) ⊓
        comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u)))
      t ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
rw₃ :
  Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (↑a : α) ⊓ 𝓟 (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u)))
      t ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
⊢ t ∈ 𝓝[u] a ↔
    Membership.mem (γ := Filter { x : α // x ∈ s })
      (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
have rw₄ : Membership.mem (γ := Filter { x : α // x ∈ s })
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t ↔
  Membership.mem (γ := Filter { x : α // x ∈ s })
    (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝[Subtype.val (p := fun (x : α) ↦ x ∈ s) '' u] (↑a : α))) t
Tactic: rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : (↑s : Type u_1)
t : Set (↑s : Type u_1)
⊢ t ∈ 𝓝 a ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t ∈ 𝓝[s] (↑a : α)
have rw : t ∈ 𝓝 a ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)
Tactic: rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
a : (↑s : Type u_1)
t : Set (↑s : Type u_1)
rw : t ∈ 𝓝 a ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)
⊢ t ∈ 𝓝 a ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t ∈ 𝓝[s] (↑a : α)
have rw₁ : t ∈ 𝓝 a ↔ t ∈ 𝓝 a
Tactic: rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
a : (↑s : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] (↑a : α)
have rw : Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a ↔ t ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)
Tactic: rw [← map_nhds_subtype_val, mem_map]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
a : (↑s : Type u_1)
rw : Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a ↔ t ∈ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a ↔ t ∈ 𝓝[s] (↑a : α)
have rw₁ : Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a ↔ Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t ∈ 𝓝 a
Tactic: rw [← map_nhds_subtype_val, mem_map]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
s : Set α
a : α
h : a ∈ s
f : α → β
l : Filter β
⊢ Tendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict (π := fun (a : α) ↦ β) f) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a h)) l
have rw : Tendsto (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a h)) l ↔
  Tendsto (s.restrict (π := fun (a : α) ↦ β) f) (𝓝 (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a h)) l
Tactic: rw [nhdsWithin_eq_map_subtype_coe h, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in 𝓝[t] (↑a : α), ∃ (h : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h ∈ J
have rw : (∃ᶠ (b : α) in 𝓝 (↑a : α), ∃ (a : (↑s : Type u_1)), (↑a : α) = b ∧ a ∈ J) ↔
  ∃ᶠ (b : α) in 𝓝 (↑a : α),
    ∃ (a : { x : α // x ∈ t }),
      (↑a : α) = b ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J
Tactic: rw [nhdsWithin_eq_map_subtype_coe (hst a.prop), Filter.frequently_map,
    clusterPt_principal_iff_frequently,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap,
    Topology.IsInducing.subtypeVal.nhds_eq_comap, Filter.frequently_comap, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
⊢ (∃ᶠ (b : α) in 𝓝 (↑a : α), ∃ (a : (↑s : Type u_1)), (↑a : α) = b ∧ a ∈ J) ↔
    ∃ᶠ (b : α) in 𝓝 (↑a : α),
      ∃ (a : { x : α // x ∈ t }),
        (↑a : α) = b ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J
have h : ∀ᶠ (x : α) in 𝓝 (↑a : α),
  (∃ (a : (↑s : Type u_1)), (↑a : α) = x ∧ a ∈ J) ↔
    ∃ (a : { x : α // x ∈ t }),
      (↑a : α) = x ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J
Tactic: apply frequently_congr
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
⊢ ∀ᶠ (x : α) in 𝓝 (↑a : α),
    (∃ (a : (↑s : Type u_1)), (↑a : α) = x ∧ a ∈ J) ↔
      ∃ (a : { x : α // x ∈ t }),
        (↑a : α) = x ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J
have h : ∀ (x : α),
  (∃ (a : (↑s : Type u_1)), (↑a : α) = x ∧ a ∈ J) ↔
    ∃ (a : { x : α // x ∈ t }),
      (↑a : α) = x ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J
Tactic: apply Eventually.of_forall
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set (↑s : Type u_1)
a : (↑s : Type u_1)
x : α
⊢ (∃ (a : (↑s : Type u_1)), (↑a : α) = x ∧ a ∈ J) ↔
    ∃ (a : { x : α // x ∈ t }),
      (↑a : α) = x ∧ ∃ (h : (↑a : α) ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑a : α) h ∈ J
have h : (∃ (x_1 : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x sorry ∈ J) ↔
  ∃ (x_1 : x ∈ t) (h : x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) x sorry ∈ J
Tactic: simp only [SetCoe.exists, exists_and_left, exists_eq_left]
-- Lean 4 proof step from Mathlib.Topology.NhdsWithin (goal)
Goal:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ u ∈ 𝓝ˢ s ↔ ∃ v ∈ 𝓝ˢ (f '' s), f ⁻¹' v ⊆ u
have simp_rw : (∃ (U : Set α), (∃ (t_1 : Set β), IsOpen[t] t_1 ∧ f ⁻¹' t_1 = U) ∧ s ⊆ U ∧ U ⊆ u) ↔
  ∃ (v : Set β), (∃ (U : Set β), IsOpen[t] U ∧ f '' s ⊆ U ∧ U ⊆ v) ∧ f ⁻¹' v ⊆ u
Tactic: simp_rw [mem_nhdsSet_iff_exists, isOpen_induced_iff]