[STATEMENT]
lemma lipschitz_extend_closure:
  fixes f::"('a::metric_space) \<Rightarrow> ('b::complete_space)"
  assumes "C-lipschitz_on U f"
  shows "\<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
obtain g where g: "\<And>x. x \<in> U \<Longrightarrow> g x = f x" "uniformly_continuous_on (closure U) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>x. x \<in> U \<Longrightarrow> g x = f x; uniformly_continuous_on (closure U) g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using uniformly_continuous_on_extension_on_closure[OF lipschitz_on_uniformly_continuous[OF assms]]
[PROOF STATE]
proof (prove)
using this:
(\<And>g. \<lbrakk>uniformly_continuous_on (closure U) g; \<And>x. x \<in> U \<Longrightarrow> f x = g x; \<And>Y h x. \<lbrakk>U \<subseteq> Y; Y \<subseteq> closure U; continuous_on Y h; \<And>x. x \<in> U \<Longrightarrow> f x = h x; x \<in> Y\<rbrakk> \<Longrightarrow> h x = g x\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<And>x. x \<in> U \<Longrightarrow> g x = f x; uniformly_continuous_on (closure U) g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x \<in> U \<Longrightarrow> g ?x = f ?x
uniformly_continuous_on (closure U) g

goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
have "C-lipschitz_on (closure U) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C-lipschitz_on (closure U) g
[PROOF STEP]
apply (rule lipschitz_on_closure, rule lipschitz_on_transform[OF assms])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> U \<Longrightarrow> g x = f x
 2. continuous_on (closure U) g
[PROOF STEP]
using g uniformly_continuous_imp_continuous[OF g(2)]
[PROOF STATE]
proof (prove)
using this:
?x \<in> U \<Longrightarrow> g ?x = f ?x
uniformly_continuous_on (closure U) g
continuous_on (closure U) g

goal (2 subgoals):
 1. \<And>x. x \<in> U \<Longrightarrow> g x = f x
 2. continuous_on (closure U) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C-lipschitz_on (closure U) g

goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C-lipschitz_on (closure U) g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C-lipschitz_on (closure U) g

goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
using g(1)
[PROOF STATE]
proof (prove)
using this:
C-lipschitz_on (closure U) g
?x \<in> U \<Longrightarrow> g ?x = f ?x

goal (1 subgoal):
 1. \<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)

goal:
No subgoals!
[PROOF STEP]
qed