[STATEMENT]
lemma continuous_onE:
    assumes "continuous_on s f" "x\<in>s" "e>0"
    obtains d where "d>0"  "\<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_on s f
x \<in> s
0 < e

goal (1 subgoal):
 1. (\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: continuous_on_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis; \<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e; x \<in> s; 0 < e\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (elim ballE allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis; x \<in> s; 0 < e; 0 < ?e6 \<longrightarrow> (\<exists>d>0. \<forall>x'\<in>s. dist x' ?x5 < d \<longrightarrow> dist (f x') (f ?x5) < ?e6)\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>d. \<lbrakk>0 < d; \<And>x'. \<lbrakk>x' \<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e\<rbrakk> \<Longrightarrow> thesis; x \<in> s; 0 < e; ?x5 \<notin> s\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto intro: that [where d="d/2" for d])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done