awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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
-- 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
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
a₈ 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
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
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
a₈ 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
⊢ 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 → 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
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
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
a₈ 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
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 → 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
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
a₈ 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
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 → Membership.mem (γ := Set X) {x}ᶜ x_2
a₁₂ 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 ∈ C → Membership.mem (γ := Set X) {x}ᶜ x_2 → x_2 ≠ x
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
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
a₈ 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
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 → Membership.mem (γ := Set X) {x}ᶜ x_2
a₁₂ 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
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_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 ∈ C
Tactic: tauto
Cleared hypotheses: this, x_1
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ AccPt x (𝓟 s) ↔ (𝓝[s \ {x}] x).NeBot
have rw : ClusterPt x (𝓟 (s \ {x})) ↔ (𝓝[s \ {x}] x).NeBot
Tactic: rw [accPt_principal_iff_clusterPt, ClusterPt, nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : ClusterPt x (𝓟 (s \ {x})) ↔ (𝓝[s \ {x}] x).NeBot
⊢ AccPt x (𝓟 s) ↔ (𝓝[s \ {x}] x).NeBot
have rw₁ : (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot ↔ (𝓝[s \ {x}] x).NeBot
Tactic: rw [accPt_principal_iff_clusterPt, ClusterPt, nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : ClusterPt x (𝓟 (s \ {x})) ↔ (𝓝[s \ {x}] x).NeBot
rw₁ : (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot ↔ (𝓝[s \ {x}] x).NeBot
⊢ AccPt x (𝓟 s) ↔ (𝓝[s \ {x}] x).NeBot
have rw₂ : (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot ↔ (𝓝 x ⊓ 𝓟 (s \ {x})).NeBot
Tactic: rw [accPt_principal_iff_clusterPt, ClusterPt, nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C)
have mp : ClusterPt x (𝓟 C) → x ∈ C ∨ AccPt x (𝓟 C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
mp : ClusterPt x (𝓟 C) → x ∈ C ∨ AccPt x (𝓟 C)
⊢ ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C)
have mpr : x ∈ C ∨ AccPt x (𝓟 C) → ClusterPt x (𝓟 C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
⊢ x ∈ C ∨ AccPt x (𝓟 C)
have mp : ∀ (hc : x ∉ C ∧ ¬AccPt x (𝓟 C)), False
Tactic: by_contra! hc
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
C : Set X
h : ClusterPt x (𝓟 C)
hc : x ∉ C ∧ ¬AccPt x (𝓟 C)
⊢ False
have hc₁ : x ∉ C ∧ ¬ClusterPt x (𝓟 (C \ {x}))
Tactic: rw [accPt_principal_iff_clusterPt] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
f : Filter X
⊢ IsClosed[inst] {x : X | ClusterPt x f}
have simp : IsClosed[inst] (⋂ i ∈ f, {x : X | x ∈ closure[inst] i})
Tactic: simp only [clusterPt_iff_forall_mem_closure, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∉ closure[inst] s ↔ 𝓝[s] x = ⊥
have rw : ¬(𝓝[s] x).NeBot ↔ 𝓝[s] x = ⊥
Tactic: rw [mem_closure_iff_nhdsWithin_neBot, not_neBot]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : ¬(𝓝[s] x).NeBot ↔ 𝓝[s] x = ⊥
⊢ x ∉ closure[inst] s ↔ 𝓝[s] x = ⊥
have rw₁ : 𝓝[s] x = ⊥ ↔ 𝓝[s] x = ⊥
Tactic: rw [mem_closure_iff_nhdsWithin_neBot, not_neBot]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ interior s ↔ ¬ClusterPt x (𝓟 sᶜ)
have rw : x ∈ interior s ↔ x ∉ closure[inst] sᶜ
Tactic: rw [← mem_closure_iff_clusterPt, closure_compl, mem_compl_iff, not_not]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : x ∈ interior s ↔ x ∉ closure[inst] sᶜ
⊢ x ∈ interior s ↔ ¬ClusterPt x (𝓟 sᶜ)
have rw₁ : x ∈ interior s ↔ x ∉ (interior s)ᶜ
Tactic: rw [← mem_closure_iff_clusterPt, closure_compl, mem_compl_iff, not_not]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : x ∈ interior s ↔ x ∉ closure[inst] sᶜ
rw₁ : x ∈ interior s ↔ x ∉ (interior s)ᶜ
⊢ x ∈ interior s ↔ ¬ClusterPt x (𝓟 sᶜ)
have rw₂ : x ∈ interior s ↔ ¬x ∉ interior s
Tactic: rw [← mem_closure_iff_clusterPt, closure_compl, mem_compl_iff, not_not]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
rw : x ∈ interior s ↔ x ∉ closure[inst] sᶜ
rw₁ : x ∈ interior s ↔ x ∉ (interior s)ᶜ
rw₂ : x ∈ interior s ↔ ¬x ∉ interior s
⊢ x ∈ interior s ↔ ¬ClusterPt x (𝓟 sᶜ)
have rw₃ : x ∈ interior s ↔ x ∈ interior s
Tactic: rw [← mem_closure_iff_clusterPt, closure_compl, mem_compl_iff, not_not]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
inst_1 : (𝓝[≠] x).NeBot
y : X
⊢ Membership.mem (γ := Set X) (closure[inst] {x}ᶜ) y
have inl : ∀ [(𝓝[≠] y).NeBot], Membership.mem (γ := Set X) (closure[inst] {y}ᶜ) y
Tactic: rcases eq_or_ne y x with (rfl | hne)
Cleared hypotheses: x, inst_1
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
inst_1 : (𝓝[≠] x).NeBot
y : X
inl : ∀ [(𝓝[≠] y).NeBot], Membership.mem (γ := Set X) (closure[inst] {y}ᶜ) y
⊢ Membership.mem (γ := Set X) (closure[inst] {x}ᶜ) y
have inr : ∀ (hne : y ≠ x), Membership.mem (γ := Set X) (closure[inst] {x}ᶜ) y
Tactic: rcases eq_or_ne y x with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst] s ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))
have simp_rw : (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))
Tactic: simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
    SetCoe.exists, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.ClusterPt (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
simp_rw :
  (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))
⊢ x ∈ closure[inst] s ↔ NeBot (α := { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝 x))
have simp_rw₁ : (∀ t ∈ 𝓝 x, (t ∩ s).Nonempty) ↔ ∀ t ∈ 𝓝 x, ∃ (a : { x : X // x ∈ s }), (↑a : X) ∈ t
Tactic: simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right,
    SetCoe.exists, exists_prop]