-- Mathlib/Topology/Perfect.lean
theorem preperfect_iff_perfect_closure [T1Space α] : Preperfect C ↔ Perfect (closure C)

Proof state:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
y : α
hyx : y ≠ x
yC : y ∈ closure C
⊢ y ∈ closure C

Tactic:
exact yC

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : AccPt x (𝓟 (closure C))
⊢ AccPt x (𝓟 C)

Tactic:
rw [accPt_iff_frequently] at *

Result:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C

Proof state:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C

Tactic:
have : ∀ y, y ≠ x ∧ y ∈ closure C → ∃ᶠ z in 𝓝 y, z ≠ x ∧ z ∈ C := by
  rintro y ⟨hyx, yC⟩
  simp only [← mem_compl_singleton_iff, and_comm, ← frequently_nhdsWithin_iff,
    hyx.nhdsWithin_compl_singleton, ← mem_closure_iff_frequently]
  exact yC

Result:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C

Proof state:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
y : α
hyx : y ≠ x
yC : y ∈ closure C
⊢ ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C

Tactic:
simp only [← mem_compl_singleton_iff, and_comm, ← frequently_nhdsWithin_iff,
  hyx.nhdsWithin_compl_singleton, ← mem_closure_iff_frequently]

Result:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
y : α
hyx : y ≠ x
yC : y ∈ closure C
⊢ y ∈ closure C

Proof state:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
⊢ ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ C

Tactic:
rw [← frequently_frequently_nhds]

Result:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
⊢ ∃ᶠ (x' : α) in 𝓝 x, ∃ᶠ (x'' : α) in 𝓝 x', x'' ≠ x ∧ x'' ∈ C

Proof state:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
⊢ AccPt x (𝓟 C)

Tactic:
have H : AccPt x (𝓟 (closure C)) := h.acc _ (subset_closure xC)

Result:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : AccPt x (𝓟 (closure C))
⊢ AccPt x (𝓟 C)

Proof state:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
⊢ Preperfect C

Tactic:
intro x xC

Result:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
⊢ AccPt x (𝓟 C)

Proof state:
case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Preperfect C
⊢ Perfect (closure C)

Tactic:
exact h.perfect_closure

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
this : ∀ (y : α), y ≠ x ∧ y ∈ closure C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C
⊢ ∃ᶠ (x' : α) in 𝓝 x, ∃ᶠ (x'' : α) in 𝓝 x', x'' ≠ x ∧ x'' ∈ C

Tactic:
exact H.mono this

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
⊢ ∀ (y : α), y ≠ x ∧ y ∈ closure C → ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C

Tactic:
rintro y ⟨hyx, yC⟩

Result:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
x : α
xC : x ∈ C
H : ∃ᶠ (y : α) in 𝓝 x, y ≠ x ∧ y ∈ closure C
y : α
hyx : y ≠ x
yC : y ∈ closure C
⊢ ∃ᶠ (z : α) in 𝓝 y, z ≠ x ∧ z ∈ C

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
⊢ Preperfect C ↔ Perfect (closure C)

Tactic:
constructor <;> intro h

Result:
case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Preperfect C
⊢ Perfect (closure C)

case mpr
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : T1Space α
h : Perfect (closure C)
⊢ Preperfect C