Countable isolated

theorem countable_isolated (S : Set ℝ) :    Set.Countable {x ∈ S | ∃ ε > 0, ∀ y ∈ S, dist y x < ε → y = x} := by  set T := {x ∈ S | ∃ ε > 0, ∀ y ∈ S, dist y x < ε → y = x}  apply Set.Countable.mono (show T ⊆    ⋃ p : ℚ, ⋃ q : ℚ, {x ∈ S | (p : ℝ) < x ∧ x < q ∧ ∀ y ∈ S, (p : ℝ) < y → y < q → y = x}    from ?_)  · apply Set.countable_iUnion; intro p    apply Set.countable_iUnion; intro q    rcases Set.eq_empty_or_nonempty      {x ∈ S | (p : ℝ) < x ∧ x < q ∧ ∀ y ∈ S, (p : ℝ) < y → y < q → y = x} with h | ⟨z, hz⟩    · rw [h]; exact Set.countable_empty    · apply (Set.countable_singleton z).mono      intro y hy      simp only [Set.mem_sep_iff] at hy hz      exact hz.2.2.2 y hy.1 hy.2.1 hy.2.2.1  · intro x ⟨hxS, ε, hε, hiso⟩    simp only [Set.mem_iUnion, Set.mem_sep_iff]    obtain ⟨p, hp1, hp2⟩ := exists_rat_btwn (show x - ε < x by linarith)    obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn (show x < x + ε by linarith)    exact ⟨p, q, hxS, hp2, hq1, fun y hyS hpy hyq => hiso y hyS (by      rw [Real.dist_eq, abs_lt]; constructor <;> linarith)⟩