awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen s
rw : s ∩ (closure s \ s) = ∅
⊢ s ∩ frontier s = ∅
have rw₁ : Eq.{u + 1} (α := Set X) ∅ ∅
Tactic: rw [hs.frontier_eq, inter_diff_self]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ Disjoint (frontier s) s ↔ IsOpen s
have rw : Disjoint (frontier s) s ↔ IsClosed sᶜ
Tactic: rw [← isClosed_compl_iff, ← frontier_subset_iff_isClosed,
    frontier_compl, subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : Disjoint (frontier s) s ↔ IsClosed sᶜ
⊢ Disjoint (frontier s) s ↔ IsOpen s
have rw₁ : Disjoint (frontier s) s ↔ frontier sᶜ ⊆ sᶜ
Tactic: rw [← isClosed_compl_iff, ← frontier_subset_iff_isClosed,
    frontier_compl, subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : Disjoint (frontier s) s ↔ IsClosed sᶜ
rw₁ : Disjoint (frontier s) s ↔ frontier sᶜ ⊆ sᶜ
⊢ Disjoint (frontier s) s ↔ IsOpen s
have rw₂ : Disjoint (frontier s) s ↔ frontier s ⊆ sᶜ
Tactic: rw [← isClosed_compl_iff, ← frontier_subset_iff_isClosed,
    frontier_compl, subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : Disjoint (frontier s) s ↔ IsClosed sᶜ
rw₁ : Disjoint (frontier s) s ↔ frontier sᶜ ⊆ sᶜ
rw₂ : Disjoint (frontier s) s ↔ frontier s ⊆ sᶜ
⊢ Disjoint (frontier s) s ↔ IsOpen s
have rw₃ : Disjoint (frontier s) s ↔ Disjoint (frontier s) s
Tactic: rw [← isClosed_compl_iff, ← frontier_subset_iff_isClosed,
    frontier_compl, subset_compl_iff_disjoint_right]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsClosed (frontier s)
have rw : IsClosed (closure s ∩ closure sᶜ)
Tactic: rw [frontier_eq_closure_inter_closure]
-- Lean 4 proof step from Mathlib.Topology.Closure (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
⊢ interior (frontier s) = ∅
have A : frontier s = s \ interior s
Tactic: have A : frontier s = s \ interior s := h.frontier_eq
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) ⊆ interior s
have rw : interior (s \ interior s) ⊆ interior s
Tactic: rw [A]
-- Lean 4 proof step from Mathlib.Topology.Closure (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
⊢ interior (frontier s) = ∅
have B : interior (frontier s) ⊆ interior s
Tactic: have B : interior (frontier s) ⊆ interior s := by rw [A]; exact interior_mono diff_subset
-- Lean 4 proof step from Mathlib.Topology.Closure (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
⊢ interior (frontier s) = ∅
have C : interior (frontier s) ⊆ frontier s
Tactic: have C : interior (frontier s) ⊆ frontier s := interior_subset
-- Lean 4 proof step from Mathlib.Topology.Closure (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) = ∅
have this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)
Tactic: have : interior (frontier s) ⊆ interior s ∩ (s \ interior s) :=
    subset_inter B (by simpa [A] using C)
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)
⊢ interior (frontier s) = ∅
have rwa : ∀ (this : interior (frontier s) ⊆ ∅), interior (frontier s) = ∅
Tactic: rwa [inter_diff_self, subset_empty_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
this : interior (frontier s) ⊆ interior s ∩ (s \ interior s)
rwa : ∀ (this : interior (frontier s) ⊆ ∅), interior (frontier s) = ∅
⊢ interior (frontier s) = ∅
have rwa₁ : ∀ (this : interior (frontier s) = ∅), interior (frontier s) = ∅
Tactic: rwa [inter_diff_self, subset_empty_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
have rw : frontier sᶜ = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
Tactic: rw [← frontier_compl, ← closure_compl, ← diff_eq, closure_diff_interior]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : frontier sᶜ = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
⊢ frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
have rw₁ : frontier sᶜ = closure sᶜ ∩ (interior sᶜ)ᶜ
Tactic: rw [← frontier_compl, ← closure_compl, ← diff_eq, closure_diff_interior]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : frontier sᶜ = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
rw₁ : frontier sᶜ = closure sᶜ ∩ (interior sᶜ)ᶜ
⊢ frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
have rw₂ : frontier sᶜ = closure sᶜ \ interior sᶜ
Tactic: rw [← frontier_compl, ← closure_compl, ← diff_eq, closure_diff_interior]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : frontier sᶜ = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
rw₁ : frontier sᶜ = closure sᶜ ∩ (interior sᶜ)ᶜ
rw₂ : frontier sᶜ = closure sᶜ \ interior sᶜ
⊢ frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
have rw₃ : frontier sᶜ = frontier sᶜ
Tactic: rw [← frontier_compl, ← closure_compl, ← diff_eq, closure_diff_interior]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ (frontier s)ᶜ = interior s ∪ interior sᶜ
have rw : ((interior s)ᶜ ∩ (interior sᶜ)ᶜ)ᶜ = interior s ∪ interior sᶜ
Tactic: rw [frontier_eq_inter_compl_interior]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : F.HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in 𝓝 x, x ∈ s i
have simp : (∀ ⦃i : Set X⦄, i ∈ 𝓝 x → ∀ ⦃j : ι⦄, p j → (id i ∩ s j).Nonempty) ↔
  ∀ (i : ι), p i → ∀ {U : Set X}, U ∈ 𝓝 x → ∃ x ∈ U, x ∈ s i
Tactic: simp only [(𝓝 x).basis_sets.clusterPt_iff hx, Filter.frequently_iff]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ ¬Disjoint (𝓝 x) F
have rw : ClusterPt x F ↔ ¬𝓝 x ⊓ F = ⊥
Tactic: rw [disjoint_iff, ClusterPt, neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
rw : ClusterPt x F ↔ ¬𝓝 x ⊓ F = ⊥
⊢ ClusterPt x F ↔ ¬Disjoint (𝓝 x) F
have rw₁ : (𝓝 x ⊓ F).NeBot ↔ ¬𝓝 x ⊓ F = ⊥
Tactic: rw [disjoint_iff, ClusterPt, neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
rw : ClusterPt x F ↔ ¬𝓝 x ⊓ F = ⊥
rw₁ : (𝓝 x ⊓ F).NeBot ↔ ¬𝓝 x ⊓ F = ⊥
⊢ ClusterPt x F ↔ ¬Disjoint (𝓝 x) F
have rw₂ : 𝓝 x ⊓ F ≠ ⊥ ↔ ¬𝓝 x ⊓ F = ⊥
Tactic: rw [disjoint_iff, ClusterPt, neBot_iff]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hF : F.HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → x ∈ closure[inst] (s i)
have simp : (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) ↔
  ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
Tactic: simp only [(nhds_basis_opens _).clusterPt_iff hF, mem_closure_iff]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hF : F.HasBasis p s
⊢ (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
have mp : (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
  ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hF : F.HasBasis p s
mp :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
⊢ (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
have mpr : (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
  ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hF : F.HasBasis p s
mp :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
mpr :
  (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
    ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
mp₁ mp₂ mp₃ :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
mpr₁ mpr₂ mpr₃ :
  (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
    ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
mp₄ mp₅ mp₆ :
  (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) →
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
⊢ (∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty) ↔
    ∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty
have mpr₄ : (∀ (i : ι), p i → ∀ (o : Set X), IsOpen[inst] o → x ∈ o → (o ∩ s i).Nonempty) →
  ∀ ⦃i : Set X⦄, x ∈ i → IsOpen[inst] i → ∀ ⦃j : ι⦄, p j → (i ∩ s j).Nonempty
Tactic: tauto
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
f : Filter X
H : f ≤ 𝓝 x
inst_1 : f.NeBot
⊢ ClusterPt x f
have rwa : (𝓝 x ⊓ f).NeBot
Tactic: rwa [ClusterPt, inf_eq_right.mpr H]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
α : Type u_1
F : Filter α
inst : TopologicalSpace α
a : α
⊢ MapClusterPt a F id ↔ ClusterPt a F
have rw : ClusterPt a (map id F) ↔ ClusterPt a F
Tactic: rw [MapClusterPt, map_id]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
α : Type u_1
F : Filter α
inst : TopologicalSpace α
a : α
rw : ClusterPt a (map id F) ↔ ClusterPt a F
⊢ MapClusterPt a F id ↔ ClusterPt a F
have rw₁ : ClusterPt a F ↔ ClusterPt a F
Tactic: rw [MapClusterPt, map_id]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
hx : (𝓝 x).HasBasis p s
⊢ MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
have simp_rw : ClusterPt x (Filter.map u F) ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
Tactic: simp_rw [MapClusterPt, hx.clusterPt_iff_frequently, frequently_map]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
F : Filter α
u : α → X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
hx : (𝓝 x).HasBasis p s
simp_rw : ClusterPt x (Filter.map u F) ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
⊢ MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
have simp_rw₁ : (∀ (i : ι), p i → ∃ᶠ (x : X) in Filter.map u F, x ∈ s i) ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
Tactic: simp_rw [MapClusterPt, hx.clusterPt_iff_frequently, frequently_map]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
⊢ AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
have rw : (𝓝[≠] x ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
Tactic: rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
rw : (𝓝[≠] x ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
⊢ AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
have rw₁ : (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
Tactic: rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
rw : (𝓝[≠] x ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
rw₁ : (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
⊢ AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
have rw₂ : (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ (𝓝 x ⊓ (𝓟 {x}ᶜ ⊓ F)).NeBot
Tactic: rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
F : Filter X
rw : (𝓝[≠] x ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
rw₁ : (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
rw₂ : (𝓝 x ⊓ 𝓟 {x}ᶜ ⊓ F).NeBot ↔ (𝓝 x ⊓ (𝓟 {x}ᶜ ⊓ F)).NeBot
⊢ AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)
have rw₃ : (𝓝 x ⊓ (𝓟 {x}ᶜ ⊓ F)).NeBot ↔ (𝓝 x ⊓ (𝓟 {x}ᶜ ⊓ F)).NeBot
Tactic: rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
have rw : ClusterPt x (𝓟 {x}ᶜ ⊓ 𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
Tactic: rw [accPt_iff_clusterPt, inf_principal, inter_comm, diff_eq]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ 𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
⊢ AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
have rw₁ : ClusterPt x (𝓟 ({x}ᶜ ∩ C)) ↔ ClusterPt x (𝓟 (C \ {x}))
Tactic: rw [accPt_iff_clusterPt, inf_principal, inter_comm, diff_eq]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ 𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
rw₁ : ClusterPt x (𝓟 ({x}ᶜ ∩ C)) ↔ ClusterPt x (𝓟 (C \ {x}))
⊢ AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
have rw₂ : ClusterPt x (𝓟 (C ∩ {x}ᶜ)) ↔ ClusterPt x (𝓟 (C \ {x}))
Tactic: rw [accPt_iff_clusterPt, inf_principal, inter_comm, diff_eq]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
rw : ClusterPt x (𝓟 {x}ᶜ ⊓ 𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
rw₁ : ClusterPt x (𝓟 ({x}ᶜ ∩ C)) ↔ ClusterPt x (𝓟 (C \ {x}))
rw₂ : ClusterPt x (𝓟 (C ∩ {x}ᶜ)) ↔ ClusterPt x (𝓟 (C \ {x}))
⊢ AccPt x (𝓟 C) ↔ ClusterPt x (𝓟 (C \ {x}))
have rw₃ : ClusterPt x (𝓟 (C ∩ {x}ᶜ)) ↔ ClusterPt x (𝓟 (C ∩ {x}ᶜ))
Tactic: rw [accPt_iff_clusterPt, inf_principal, inter_comm, diff_eq]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (hypothesis)
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝[≠] x, y ∈ C
have this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
Tactic: have : (∃ᶠ z in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ z in 𝓝 x, z ∈ C ∧ z ∈ ({x} : Set X)ᶜ :=
    frequently_inf_principal.trans <| by simp only [and_comm]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝[≠] x, y ∈ C
have rw : (∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
Tactic: rw [accPt_iff_frequently, this]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
⊢ (∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
have a : ∀ (x_1 : X), x_1 ≠ x ∧ x_1 ∈ C ↔ x_1 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_1
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
x_1 : X
⊢ x_1 ≠ x ∧ x_1 ∈ C ↔ x_1 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_1
have a : ∀ (x_2 : X),
  (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
    (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
      (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
Tactic: tauto
Cleared hypotheses: this, x_1
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
x_1 : X
a :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
⊢ x_1 ≠ x ∧ x_1 ∈ C ↔ x_1 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_1
have a₁ : ∀ (x_2 : X),
  (¬∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
    (¬∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
      (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
Tactic: tauto
Cleared hypotheses: this, x_1
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
x_1 : X
a :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₁ :
  ∀ (x_2 : X),
    (¬∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (¬∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₂ :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₃ :
  ∀ (x_2 : X),
    (¬∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (¬∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
⊢ x_1 ≠ x ∧ x_1 ∈ C ↔ x_1 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_1
have a₄ : ∀ (x_2 : X),
  (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
    (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
      x_2 ≠ x ∧ x_2 ∈ C → x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2
Tactic: tauto
Cleared hypotheses: this, x_1
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
x_1 : X
a :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₁ :
  ∀ (x_2 : X),
    (¬∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (¬∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₂ :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₃ :
  ∀ (x_2 : X),
    (¬∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (¬∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₄ :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        x_2 ≠ x ∧ x_2 ∈ C → x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2
⊢ x_1 ≠ x ∧ x_1 ∈ C ↔ x_1 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_1
have a₅ : ∀ (x_2 : X),
  (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
    (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
      x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2 → x_2 ≠ x ∧ x_2 ∈ C
Tactic: tauto
Cleared hypotheses: this, x_1
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u_3
inst : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z
x_1 : X
a :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₁ :
  ∀ (x_2 : X),
    (¬∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (¬∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₂ :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₃ :
  ∀ (x_2 : X),
    (¬∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (¬∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        (x_2 ≠ x ∧ x_2 ∈ C ↔ x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2)
a₄ :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        x_2 ≠ x ∧ x_2 ∈ C → x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2
a₅ :
  ∀ (x_2 : X),
    (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
      (∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
        x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2 → x_2 ≠ x ∧ x_2 ∈ C
⊢ x_1 ≠ x ∧ x_1 ∈ C ↔ x_1 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_1
have a₆ : ∀ (x_2 : X),
  (¬∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) →
    (¬∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ z) →
      x_2 ≠ x ∧ x_2 ∈ C → x_2 ∈ C ∧ Membership.mem (γ := Set X) {x}ᶜ x_2
Tactic: tauto
Cleared hypotheses: this, x_1