awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t
have h₁ : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x_1 : X |
      Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ s ↔ x ∈ t) x} x_1 →
        Membership.mem (γ := Set X) {x_2 : X | (fun (x_3 : X) ↦ x_3 = x ∨ x_3 ∈ s ↔ x_3 = x ∨ x_3 ∈ t) x_2} x_1}
    a
Tactic: filter_upwards [nhdsWithin_compl_singleton_le x y h] with y using or_congr (Iff.rfl)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
h₁ :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x_1 : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ s ↔ x ∈ t) x} x_1 →
          Membership.mem (γ := Set X) {x_2 : X | (fun (x_3 : X) ↦ x_3 = x ∨ x_3 ∈ s ↔ x_3 = x ∨ x_3 ∈ t) x_2} x_1}
      a
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t
have h₂ : ∀ (a : X), (a ∈ s ↔ a ∈ t) → (a = x ∨ a ∈ s ↔ a = x ∨ a ∈ t)
Tactic: filter_upwards [nhdsWithin_compl_singleton_le x y h] with y using or_congr (Iff.rfl)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
⊢ Eq (α := Set X) (⋂ (i : ι), ⋂ (_ : p i), s i) {x}
have rw : (𝓝 x).ker = {x}
Tactic: rw [← h.ker, ker_nhds]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
rw : (𝓝 x).ker = {x}
⊢ Eq (α := Set X) (⋂ (i : ι), ⋂ (_ : p i), s i) {x}
have rw₁ : Eq (α := Set X) {x} {x}
Tactic: rw [← h.ker, ker_nhds]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
⊢ {x}ᶜ ∈ 𝓝ˢ s ↔ x ∉ s
have rw : s ⊆ {x}ᶜ ↔ x ∉ s
Tactic: rw [isOpen_compl_singleton.mem_nhdsSet, subset_compl_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
rw : s ⊆ {x}ᶜ ↔ x ∉ s
⊢ {x}ᶜ ∈ 𝓝ˢ s ↔ x ∉ s
have rw₁ : x ∉ s ↔ x ∉ s
Tactic: rw [isOpen_compl_singleton.mem_nhdsSet, subset_compl_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
⊢ 𝓝ˢ s ≤ 𝓝ˢ t ↔ s ⊆ t
have refine : 𝓝ˢ s ≤ 𝓝ˢ t → s ⊆ t
Tactic: refine ⟨?_, fun h => monotone_nhdsSet h⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
h : ∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s
x : X
hx : x ∈ s
⊢ x ∈ t
have h₁ : {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s
Tactic: specialize h {x}ᶜ
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : {x}ᶜ ∈ 𝓝ˢ t → {x}ᶜ ∈ 𝓝ˢ s
⊢ x ∈ t
have h₁ : x ∉ t → x ∉ s
Tactic: simp_rw [compl_singleton_mem_nhdsSet_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
x : X
hx : x ∈ s
h : x ∉ t → x ∉ s
⊢ x ∈ t
have by_contra : ∀ (hxt : x ∉ t), False
Tactic: by_contra hxt
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s t : Set X
⊢ 𝓝ˢ s = 𝓝ˢ t ↔ s = t
have simp_rw : 𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ≤ t ∧ t ≤ s
Tactic: simp_rw [le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x : X
⊢ 𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s
have rw : 𝓝ˢ {x} ≤ 𝓝ˢ s ↔ x ∈ s
Tactic: rw [← nhdsSet_singleton, nhdsSet_le_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x : X
rw : 𝓝ˢ {x} ≤ 𝓝ˢ s ↔ x ∈ s
⊢ 𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s
have rw₁ : {x} ⊆ s ↔ x ∈ s
Tactic: rw [← nhdsSet_singleton, nhdsSet_le_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
s : Set X
x : X
rw : 𝓝ˢ {x} ≤ 𝓝ˢ s ↔ x ∈ s
rw₁ : {x} ⊆ s ↔ x ∈ s
⊢ 𝓝 x ≤ 𝓝ˢ s ↔ x ∈ s
have rw₂ : x ∈ s ↔ x ∈ s
Tactic: rw [← nhdsSet_singleton, nhdsSet_le_iff, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a : X
s_1 : Finset X
h : a ∉ s_1
ih : Dense (s \ (↑s_1 : Set X))
⊢ Dense (s \ (↑(insert a s_1) : Set X))
have insert : Dense ((s \ (↑s_1 : Set X)) \ {a})
Tactic: rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
⊢ Dense (s \ (↑t : Set X))
have empty : Dense (s \ (↑∅ : Set X))
Tactic: induction t using Finset.induction_on with
  | empty => simpa using hs
  | insert _ _ _ ih =>
    rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
    exact ih.diff_singleton _
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
empty : Dense (s \ (↑∅ : Set X))
⊢ Dense (s \ (↑t : Set X))
have insert : ∀ (a : X) (s_1 : Finset X), a ∉ s_1 → ∀ (ih : Dense (s \ (↑s_1 : Set X))), Dense (s \ (↑(insert a s_1) : Set X))
Tactic: induction t using Finset.induction_on with
  | empty => simpa using hs
  | insert _ _ _ ih =>
    rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
    exact ih.diff_singleton _
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
⊢ Dense (s \ (↑t : Set X))
have empty : Dense (s \ (↑∅ : Set X))
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simpa using hs
  | insert _ _ _ ih =>
    rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
    exact ih.diff_singleton _
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Finset X
empty : Dense (s \ (↑∅ : Set X))
⊢ Dense (s \ (↑t : Set X))
have insert : ∀ (a : X) (s_1 : Finset X), a ∉ s_1 → ∀ (ih : Dense (s \ (↑s_1 : Set X))), Dense (s \ (↑(insert a s_1) : Set X))
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simpa using hs
  | insert _ _ _ ih =>
    rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
    exact ih.diff_singleton _
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ Dense (s \ t)
have h : t = (↑(ht.toFinset (s := t)) : Set X)
Tactic: convert! hs.diff_finset ht.toFinset
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (x : X) in 𝓝[s] a, p x
have nth_rw : (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
Tactic: nth_rw 2 [← eventually_eventually_nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
have mp : (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
mp : (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
⊢ (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x) ↔ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
have mpr : (∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x) → ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
⊢ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
have h₁ : ∀ (a : X) (hy : ∀ᶠ (x : X) in 𝓝 a, p x), ∀ᶠ (x : X) in 𝓝[s] a, p x
Tactic: filter_upwards [h] with _ hy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝[s] y, p x
⊢ ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
have h₁ : ∀ (a : X), (∀ᶠ (x : X) in 𝓝[s] a, p x) → a ∈ s → ∀ᶠ (x : X) in 𝓝 a, p x
Tactic: filter_upwards [h, eventually_nhdsWithin_of_forall fun _ a ↦ a] with _ _ _
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x y : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
have inl : ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x
Tactic: rcases eq_or_ne x y with (rfl | h)
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x y : X
s : Set X
f : X → Y
inl : ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
have inr : ∀ (h : x ≠ y), ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
Tactic: rcases eq_or_ne x y with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x y : X
s : Set X
f : X → Y
⊢ ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x
have rw : ContinuousWithinAt f (insert y (s \ {y})) x ↔ ContinuousWithinAt f s x
Tactic: rw [← continuousWithinAt_insert, insert_diff_singleton, continuousWithinAt_insert]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x y : X
s : Set X
f : X → Y
rw : ContinuousWithinAt f (insert y (s \ {y})) x ↔ ContinuousWithinAt f s x
rw₁ : X
⊢ ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x
have rw₂ : ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
Tactic: rw [← continuousWithinAt_insert, insert_diff_singleton, continuousWithinAt_insert]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x y : X
s : Set X
f : X → Y
rw : ContinuousWithinAt f (insert y (s \ {y})) x ↔ ContinuousWithinAt f s x
rw₁ : X
rw₂ : ContinuousWithinAt f (insert y s) x ↔ ContinuousWithinAt f s x
⊢ ContinuousWithinAt f (s \ {y}) x ↔ ContinuousWithinAt f s x
have rw₃ : ContinuousWithinAt f s x ↔ ContinuousWithinAt f s x
Tactic: rw [← continuousWithinAt_insert, insert_diff_singleton, continuousWithinAt_insert]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x
have rw : ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f (insert x t) x
Tactic: rw [← continuousWithinAt_insert_self (s := s), ← continuousWithinAt_insert_self (s := t)]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
f : X → Y
s : Set X
x : X
c : Y
h : ContinuousWithinAt f s x
hx : x ∈ closure[inst] s
ht : ∀ y ∈ s, f y = c
⊢ f x = c
have rw : Membership.mem (γ := Set Y) (closure[inst_1] {c}) (f x)
Tactic: rw [← Set.mem_singleton_iff, ← closure_singleton]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T1Space Y
f : X → Y
x : X
y : Y
h : Tendsto f (𝓝 x) (𝓝 y)
⊢ ContinuousAt f x
have rwa : Tendsto f (𝓝 x) (𝓝 (f x))
Tactic: rwa [ContinuousAt, eq_of_tendsto_nhds h]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
l : Filter Y
inst_2 : l.NeBot
c d : X
⊢ Tendsto (fun (x : Y) ↦ c) l (𝓝 d) ↔ c = d
have simp_rw : map (fun (x : Y) ↦ c) l ≤ 𝓝 d ↔ c = d
Tactic: simp_rw [Tendsto, Filter.map_const, pure_le_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
l : Filter Y
inst_2 : l.NeBot
c d : X
simp_rw : map (fun (x : Y) ↦ c) l ≤ 𝓝 d ↔ c = d
⊢ Tendsto (fun (x : Y) ↦ c) l (𝓝 d) ↔ c = d
have simp_rw₁ : pure c ≤ 𝓝 d ↔ c = d
Tactic: simp_rw [Tendsto, Filter.map_const, pure_le_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ IsOpen[inst] {x}
have A : {x} ⊆ s
Tactic: have A : {x} ⊆ s := by simp only [singleton_subset_iff, mem_of_mem_nhds hs]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
⊢ IsOpen[inst] {x}
have B : IsClosed[inst] (s \ {x})
Tactic: have B : IsClosed (s \ {x}) := (hsf.subset diff_subset).isClosed
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst] (s \ {x})
⊢ IsOpen[inst] {x}
have C : (s \ {x})ᶜ ∈ 𝓝 x
Tactic: have C : (s \ {x})ᶜ ∈ 𝓝 x := B.isOpen_compl.mem_nhds fun h => h.2 rfl
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
⊢ IsOpen[inst] {x}
have D : {x} ∈ 𝓝 x
Tactic: have D : {x} ∈ 𝓝 x := by simpa only [← diff_eq, diff_diff_cancel_left A] using inter_mem hs C
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ∈ 𝓝 x
⊢ IsOpen[inst] {x}
have rwa : ∀ (D : Membership.mem (γ := Set X) (interior {x}) x), IsOpen[inst] {x}
Tactic: rwa [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, subset_interior_iff_isOpen] at D
Cleared hypotheses: D
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ∈ 𝓝 x
rwa : ∀ (D : Membership.mem (γ := Set X) (interior {x}) x), IsOpen[inst] {x}
⊢ IsOpen[inst] {x}
have rwa₁ : ∀ (D : Subset (α := Set X) {x} (interior {x})), IsOpen[inst] {x}
Tactic: rwa [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, subset_interior_iff_isOpen] at D
Cleared hypotheses: D
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
A : {x} ⊆ s
B : IsClosed[inst] (s \ {x})
C : (s \ {x})ᶜ ∈ 𝓝 x
D : {x} ∈ 𝓝 x
rwa : ∀ (D : Membership.mem (γ := Set X) (interior {x}) x), IsOpen[inst] {x}
rwa₁ : ∀ (D : Subset (α := Set X) {x} (interior {x})), IsOpen[inst] {x}
⊢ IsOpen[inst] {x}
have rwa₂ : ∀ (D : IsOpen[inst] {x}), IsOpen[inst] {x}
Tactic: rwa [← mem_interior_iff_mem_nhds, ← singleton_subset_iff, subset_interior_iff_isOpen] at D
Cleared hypotheses: D
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
⊢ s.Infinite
have refine : ∀ (hsf : s.Finite), 𝓝[≠] x = ⊥
Tactic: refine fun hsf => hx.1 ?_
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
inst_1 : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ 𝓝[≠] x = ⊥
have rw : IsOpen[inst] {x}
Tactic: rw [← isOpen_singleton_iff_punctured_nhds]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
⊢ ContinuousOn f s
have rw : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ Y) f)
Tactic: rw [continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : T1Space X
inst_2 : TopologicalSpace Y
s : Set X
hs : s.Finite
f : X → Y
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : X) ↦ Y) f)
have this : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: have : Finite s := hs
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ T1Space.{u_1} (SeparationQuotient X) ↔ R0Space X
have rw : (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Symmetric.{u_1 + 1} (α := X) Specializes
Tactic: rw [r0Space_iff, ((t1Space_TFAE (SeparationQuotient X)).out 0 9 :)]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Symmetric.{u_1 + 1} (α := X) Specializes
have mp : (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) → Symmetric.{u_1 + 1} (α := X) Specializes
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
mp : (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) → Symmetric.{u_1 + 1} (α := X) Specializes
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Symmetric.{u_1 + 1} (α := X) Specializes
have mpr : Symmetric.{u_1 + 1} (α := X) Specializes → ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
x y : X
xspecy : x ⤳ y
⊢ y ⤳ x
have mp : ∀ (xspecy : Specializes (X := SeparationQuotient X) (mk x) (mk y)),
  Specializes (X := SeparationQuotient X) (mk y) (mk x)
Tactic: rw [← IsInducing.specializes_iff isInducing_mk, h xspecy] at *
Cleared hypotheses: xspecy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
x y : X
xspecy : x ⤳ y
mp :
  ∀ (xspecy : Specializes (X := SeparationQuotient X) (mk x) (mk y)),
    Specializes (X := SeparationQuotient X) (mk y) (mk x)
⊢ y ⤳ x
have mp₁ : ∀ (xspecy : Specializes (X := SeparationQuotient X) (mk y) (mk y)),
  Specializes (X := SeparationQuotient X) (mk y) (mk y)
Tactic: rw [← IsInducing.specializes_iff isInducing_mk, h xspecy] at *
Cleared hypotheses: xspecy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : Symmetric.{u_1 + 1} (α := X) Specializes
x_1 : SeparationQuotient X
x : X
y_1 : SeparationQuotient X
y : X
sxspecsy :
  Specializes (X := SeparationQuotient X) (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) x)
    (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) y)
⊢ Eq (α := SeparationQuotient X) (mk x) (mk y)
have xspecy : x ⤳ y
Tactic: have xspecy : x ⤳ y := isInducing_mk.specializes_iff.mp sxspecsy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : Symmetric.{u_1 + 1} (α := X) Specializes
x_1 : SeparationQuotient X
x : X
y_1 : SeparationQuotient X
y : X
sxspecsy :
  Specializes (X := SeparationQuotient X) (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) x)
    (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) y)
xspecy : x ⤳ y
⊢ Eq (α := SeparationQuotient X) (mk x) (mk y)
have yspecx : y ⤳ x
Tactic: have yspecx : y ⤳ x := h xspecy
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : Symmetric.{u_1 + 1} (α := X) Specializes
x_1 : SeparationQuotient X
x : X
y_1 : SeparationQuotient X
y : X
sxspecsy :
  Specializes (X := SeparationQuotient X) (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) x)
    (Quot.mk (⇑(inseparableSetoid X) : X → X → Prop) y)
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ Eq (α := SeparationQuotient X) (mk x) (mk y)
have mpr : x ⤳ y ∧ y ⤳ x
Tactic: rw [mk_eq_mk, inseparable_iff_specializes_and]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ {x} ∈ 𝓝[s] x
have rw : ∀ (hs : DiscreteTopology.{u_1} (↑s : Type u_1)) {x : X} (hx : x ∈ s), {x} ∈ 𝓝[s] x
Tactic: rw [isDiscrete_iff_discreteTopology] at hs
Cleared hypotheses: hs, x, hx
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : DiscreteTopology.{u_1} (↑s : Type u_1)
x : X
hx : x ∈ s
⊢ {x} ∈ 𝓝[s] x
have this : {Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx} ∈ 𝓝 (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx)
Tactic: have : ({⟨x, hx⟩} : Set s) ∈ 𝓝 (⟨x, hx⟩ : s) := by simp [nhds_discrete]
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
ι : Type u_3
p : ι → Prop
t : ι → Set X
s : Set X
hs : IsDiscrete s
x : X
hb : (𝓝 x).HasBasis p t
hx : x ∈ s
⊢ ∃ (i : ι), p i ∧ t i ∩ s = {x}
have rcases : ∀ (i : ι) (hi : p i) (hix : t i ∩ s ⊆ {x}), ∃ (i : ι), p i ∧ t i ∩ s = {x}
Tactic: rcases (nhdsWithin_hasBasis hb s).mem_iff.1 (singleton_mem_nhdsWithin_of_mem_discrete hs hx) with
    ⟨i, hi, hix⟩
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ U ∩ s = {x}
have obtain : ∀ (U : Set X) (hU_nhds : U ∈ 𝓝 x) (hU_inter : U ∩ s = {x}), ∃ (U : Set X), IsOpen[inst] U ∧ U ∩ s = {x}
Tactic: obtain ⟨U, hU_nhds, hU_inter⟩ := nhds_inter_eq_singleton_of_mem_discrete hs hx
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
U : Set X
hU_nhds : U ∈ 𝓝 x
hU_inter : U ∩ s = {x}
⊢ ∃ (U : Set X), IsOpen[inst] U ∧ U ∩ s = {x}
have obtain : ∀ (t : Set X) (ht_sub : t ⊆ U) (ht_open : IsOpen[inst] t) (ht_x : x ∈ t), ∃ (U : Set X), IsOpen[inst] U ∧ U ∩ s = {x}
Tactic: obtain ⟨t, ht_sub, ht_open, ht_x⟩ := mem_nhds_iff.mp hU_nhds
-- Lean 4 proof step from Mathlib.Topology.Separation.Basic (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsDiscrete s
x : X
hx : x ∈ s
V : Set X
h : V ∈ 𝓝 x
h' : V ∩ s = {x}
⊢ {x}ᶜ ∩ V ∩ s = ∅
have rw : {x}ᶜ ∩ (V ∩ s) = ∅
Tactic: rw [inter_assoc, h', compl_inter_self]