[STATEMENT]
lemma perfect_choose_dist: "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
  for x :: "'a::{perfect_space,metric_space}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r
[PROOF STEP]
using islimpt_UNIV [of x]
[PROOF STATE]
proof (prove)
using this:
x islimpt UNIV

goal (1 subgoal):
 1. 0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r
[PROOF STEP]
by (simp add: islimpt_approachable)