-- 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
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
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