diff --git a/thys/Gromov_Hyperbolicity/Library_Complements.thy b/thys/Gromov_Hyperbolicity/Library_Complements.thy
--- a/thys/Gromov_Hyperbolicity/Library_Complements.thy
+++ b/thys/Gromov_Hyperbolicity/Library_Complements.thy
@@ -1,1760 +1,1684 @@
 (*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
     License: BSD
 *)
 
 section \<open>Additions to the library\<close>
 
 theory Library_Complements
   imports "HOL-Analysis.Analysis" "HOL-Cardinals.Cardinal_Order_Relation"
 begin
 
 subsection \<open>Mono intros\<close>
 
 text \<open>We have a lot of (large) inequalities to prove. It is very convenient to have a set of
 introduction rules for this purpose (a lot should be added to it, I have put here all the ones
 I needed).
 
 The typical use case is when one wants to prove some inequality, say
 $ \exp (x*x) \leq y + \exp(1 + z * z + y)$, assuming $y \geq 0$ and $0 \leq x \leq z$.
 One would write it has
 \begin{verbatim}
 have "0 + \exp(0 + x * x + 0) < = y + \exp(1 + z * z + y)"
 using `y > = 0` `x < = z` by (intro mono_intros)
 \end{verbatim}
 When the left and right hand terms are written in completely analogous ways as above, then the
 introduction rules (that contain monotonicity of addition, of the exponential, and so on) reduce
 this to comparison of elementary terms in the formula. This is a very naive strategy, that fails
 in many situations, but that is very efficient when used correctly.
 \<close>
 
 named_theorems mono_intros "structural introduction rules to prove inequalities"
 declare le_imp_neg_le [mono_intros]
 declare add_left_mono [mono_intros]
 declare add_right_mono [mono_intros]
 declare add_strict_left_mono [mono_intros]
 declare add_strict_right_mono [mono_intros]
 declare add_mono [mono_intros]
 declare add_less_le_mono [mono_intros]
 declare diff_right_mono [mono_intros]
 declare diff_left_mono [mono_intros]
 declare diff_mono [mono_intros]
 declare mult_left_mono [mono_intros]
 declare mult_right_mono [mono_intros]
 declare mult_mono [mono_intros]
 declare max.mono [mono_intros]
 declare min.mono [mono_intros]
 declare power_mono [mono_intros]
 declare ln_ge_zero [mono_intros]
 declare ln_le_minus_one [mono_intros]
 declare ennreal_minus_mono [mono_intros]
 declare ennreal_leI [mono_intros]
 declare e2ennreal_mono [mono_intros]
 declare enn2ereal_nonneg [mono_intros]
 declare zero_le [mono_intros]
 declare top_greatest [mono_intros]
 declare bot_least [mono_intros]
 declare dist_triangle [mono_intros]
 declare dist_triangle2 [mono_intros]
 declare dist_triangle3 [mono_intros]
 declare exp_ge_add_one_self [mono_intros]
 declare exp_gt_one [mono_intros]
 declare exp_less_mono [mono_intros]
 declare dist_triangle [mono_intros]
 declare abs_triangle_ineq [mono_intros]
 declare abs_triangle_ineq2 [mono_intros]
 declare abs_triangle_ineq2_sym [mono_intros]
 declare abs_triangle_ineq3 [mono_intros]
 declare abs_triangle_ineq4 [mono_intros]
 declare Liminf_le_Limsup [mono_intros]
 declare ereal_liminf_add_mono [mono_intros]
 declare le_of_int_ceiling [mono_intros]
 declare ereal_minus_mono [mono_intros]
 declare infdist_triangle [mono_intros]
 declare divide_right_mono [mono_intros]
 declare self_le_power [mono_intros]
 
 lemma ln_le_cancelI [mono_intros]:
   assumes "(0::real) < x" "x \<le> y"
   shows "ln x \<le> ln y"
 using assms by auto
 
 lemma exp_le_cancelI [mono_intros]:
   assumes "x \<le> (y::real)"
   shows "exp x \<le> exp y"
 using assms by simp
 
 lemma mult_ge1_mono [mono_intros]:
   assumes "a \<ge> (0::'a::linordered_idom)" "b \<ge> 1"
   shows "a \<le> a * b" "a \<le> b * a"
 using assms mult_le_cancel_left1 mult_le_cancel_right1 by force+
 
 text \<open>A few convexity inequalities we will need later on.\<close>
 
 lemma xy_le_uxx_vyy [mono_intros]:
   assumes "u > 0" "u * v = (1::real)"
   shows "x * y \<le> u * x^2/2 + v * y^2/2"
 proof -
   have "v > 0" using assms
     by (metis (full_types) dual_order.strict_implies_order le_less_linear mult_nonneg_nonpos not_one_le_zero)
   then have *: "sqrt u * sqrt v = 1"
     using assms by (metis real_sqrt_mult real_sqrt_one)
   have "(sqrt u * x - sqrt v * y)^2 \<ge> 0" by auto
   then have "u * x^2 + v * y^2 - 2 * 1 * x * y \<ge> 0"
     unfolding power2_eq_square *[symmetric] using \<open>u > 0\<close> \<open>v > 0\<close> by (auto simp add: algebra_simps)
   then show ?thesis by (auto simp add: algebra_simps divide_simps)
 qed
 
 lemma xy_le_xx_yy [mono_intros]:
   "x * y \<le> x^2/2 + y^2/2" for x y::real
 using xy_le_uxx_vyy[of 1 1] by auto
 
 lemma ln_squared_bound [mono_intros]:
   "(ln x)^2 \<le> 2 * x - 2" if "x \<ge> 1" for x::real
 proof -
   define f where "f = (\<lambda>x::real. 2 * x - 2 - ln x * ln x)"
   have *: "DERIV f x :> 2 - 2 * ln x / x" if "x > 0" for x::real
     unfolding f_def using that by (auto intro!: derivative_eq_intros)
   have "f 1 \<le> f x" if "x \<ge> 1" for x
   proof (rule DERIV_nonneg_imp_nondecreasing[OF that])
     fix t::real assume "t \<ge> 1"
     show "\<exists>y. (f has_real_derivative y) (at t) \<and> 0 \<le> y"
       apply (rule exI[of _ "2 - 2 * ln t / t"])
       using *[of t] \<open>t \<ge> 1\<close> by (auto simp add: divide_simps ln_bound)
   qed
   then show ?thesis unfolding f_def power2_eq_square using that by auto
 qed
 
 text \<open>In the next lemma, the assumptions are too strong (negative numbers
 less than $-1$ also work well to have a square larger than $1$), but in practice one proves
 inequalities with nonnegative numbers, so this version is really the useful one for
 \verb+mono_intros+.\<close>
 
 lemma mult_ge1_powers [mono_intros]:
   assumes "a \<ge> (1::'a::linordered_idom)"
   shows "1 \<le> a * a" "1 \<le> a * a * a" "1 \<le> a * a * a * a"
 using assms by (meson assms dual_order.trans mult_ge1_mono(1) zero_le_one)+
 
 lemmas [mono_intros] = ln_bound
 
 lemma mono_cSup:
   fixes f :: "'a::conditionally_complete_lattice \<Rightarrow> 'b::conditionally_complete_lattice"
   assumes "bdd_above A" "A \<noteq> {}" "mono f"
   shows "Sup (f`A) \<le> f (Sup A)"
 by (metis assms(1) assms(2) assms(3) cSUP_least cSup_upper mono_def)
 
 lemma mono_cSup_bij:
   fixes f :: "'a::conditionally_complete_linorder \<Rightarrow> 'b::conditionally_complete_linorder"
   assumes "bdd_above A" "A \<noteq> {}" "mono f" "bij f"
   shows "Sup (f`A) = f(Sup A)"
 proof -
   have "Sup ((inv f)`(f`A)) \<le> (inv f) (Sup (f`A))"
     apply (rule mono_cSup)
     using mono_inv[OF assms(3) assms(4)] assms(2) bdd_above_image_mono[OF assms(3) assms(1)] by auto
   then have "f (Sup ((inv f)`(f`A))) \<le> Sup (f`A)"
     using assms mono_def by (metis (no_types, hide_lams) bij_betw_imp_surj_on surj_f_inv_f)
   moreover have "f (Sup ((inv f)`(f`A))) = f(Sup A)"
     using assms by (simp add: bij_is_inj)
   ultimately show ?thesis using mono_cSup[OF assms(1) assms(2) assms(3)] by auto
 qed
 
 subsection \<open>More topology\<close>
 
 text \<open>In situations of interest to us later on, convergence is well controlled only for sequences
 living in some dense subset of the space (but the limit can be anywhere). This is enough to
 establish continuity of the function, if the target space is well enough separated.
 
 The statement we give below is very general,
 as we do not assume that the function is continuous inside the original set $S$, it will typically
 only be continuous at a set $T$ contained in the closure of $S$. In many applications, $T$ will
 be the closure of $S$, but we are also thinking of the case where one constructs an extension
 of a function inside a space, to its boundary, and the behaviour at the boundary is better than
 inside the space. The example we have in mind is the extension of a quasi-isometry to the boundary
 of a Gromov hyperbolic space.
 
 In the following criterion, we assume that if $u_n$ inside $S$ converges to a point at the boundary
 $T$, then $f(u_n)$ converges (where $f$ is some function inside). Then, we can extend the function $f$ at
 the boundary, by picking the limit value of $f(u_n)$ for some sequence converging to $u_n$. Then
 the lemma asserts that $f$ is continuous at every point $b$ on the boundary.
 
 The proof is done in two steps:
 \begin{enumerate}
 \item First, if $v_n$ is another inside sequence tending to
 the same point $b$ on the boundary, then $f(v_n)$ converges to the same value as $f(u_n)$: this is
 proved by considering the sequence $w$ equal to $u$ at even times and to $v$ at odd times, and
 saying that $f(w_n)$ converges. Its limit is equal to the limit of $f(u_n)$ and of $f(v_n)$, so they
 have to coincide.
 \item Now, consider a general sequence $v$ (in the space or the boundary) converging to $b$. We want
 to show that $f(v_n)$ tends to $f(b)$. If $v_n$ is inside $S$, we have already done it in the first
 step. If it is on the boundary, on the other hand, we can approximate it by an inside point $w_n$
 for which $f(w_n)$ is very close to $f(v_n)$. Then $w_n$ is an inside sequence converging to $b$,
 hence $f(w_n)$ converges to $f(b)$ by the first step, and then $f(v_n)$ also converges to $f(b)$.
 The precise argument is more conveniently written by contradiction. It requires good separation
 properties of the target space.
 \end{enumerate}\<close>
 
 text \<open>First, we introduce the material to interpolate between two sequences, one at even times
 and the other one at odd times.\<close>
 
 definition even_odd_interpolate::"(nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
   where "even_odd_interpolate u v n = (if even n then u (n div 2) else v (n div 2))"
 
 lemma even_odd_interpolate_compose:
   "even_odd_interpolate (f o u) (f o v) = f o (even_odd_interpolate u v)"
   unfolding even_odd_interpolate_def comp_def by auto
 
 lemma even_odd_interpolate_filterlim:
   "filterlim u F sequentially \<and> filterlim v F sequentially \<longleftrightarrow> filterlim (even_odd_interpolate u v) F sequentially"
 proof (auto)
   assume H: "filterlim (even_odd_interpolate u v) F sequentially"
   define r::"nat \<Rightarrow> nat" where "r = (\<lambda>n. 2 * n)"
   have "strict_mono r" unfolding r_def strict_mono_def by auto
   then have "filterlim r sequentially sequentially"
     by (simp add: filterlim_subseq)
   have "filterlim (\<lambda>n. (even_odd_interpolate u v) (r n)) F sequentially"
     by (rule filterlim_compose[OF H filterlim_subseq[OF \<open>strict_mono r\<close>]])
   moreover have "even_odd_interpolate u v (r n) = u n" for n
     unfolding r_def even_odd_interpolate_def by auto
   ultimately show "filterlim u F sequentially" by auto
   define r::"nat \<Rightarrow> nat" where "r = (\<lambda>n. 2 * n + 1)"
   have "strict_mono r" unfolding r_def strict_mono_def by auto
   then have "filterlim r sequentially sequentially"
     by (simp add: filterlim_subseq)
   have "filterlim (\<lambda>n. (even_odd_interpolate u v) (r n)) F sequentially"
     by (rule filterlim_compose[OF H filterlim_subseq[OF \<open>strict_mono r\<close>]])
   moreover have "even_odd_interpolate u v (r n) = v n" for n
     unfolding r_def even_odd_interpolate_def by auto
   ultimately show "filterlim v F sequentially" by auto
 next
   assume H: "filterlim u F sequentially" "filterlim v F sequentially"
   show "filterlim (even_odd_interpolate u v) F sequentially"
   unfolding filterlim_iff eventually_sequentially proof (auto)
     fix P assume *: "eventually P F"
     obtain N1 where N1: "\<And>n. n \<ge> N1 \<Longrightarrow> P (u n)"
       using H(1) unfolding filterlim_iff eventually_sequentially using * by auto
     obtain N2 where N2: "\<And>n. n \<ge> N2 \<Longrightarrow> P (v n)"
       using H(2) unfolding filterlim_iff eventually_sequentially using * by auto
     have "P (even_odd_interpolate u v n)" if "n \<ge> 2 * N1 + 2 * N2" for n
     proof (cases "even n")
       case True
       have "n div 2 \<ge> N1" using that by auto
       then show ?thesis unfolding even_odd_interpolate_def using True N1 by auto
     next
       case False
       have "n div 2 \<ge> N2" using that by auto
       then show ?thesis unfolding even_odd_interpolate_def using False N2 by auto
     qed
     then show "\<exists>N. \<forall>n \<ge> N. P (even_odd_interpolate u v n)" by auto
   qed
 qed
 
 text \<open>Then, we prove the continuity criterion for extensions of functions to the boundary $T$ of a set
 $S$. The first assumption is that $f(u_n)$ converges when $f$ converges to the boundary, and the
 second one that the extension of $f$ to the boundary has been defined using the limit along some
 sequence tending to the point under consideration. The following criterion is the most general one,
 but this is not the version that is most commonly applied so we use a prime in its name.\<close>
 
 lemma continuous_at_extension_sequentially':
   fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::t3_space"
   assumes "b \<in> T"
           "\<And>u b. (\<forall>n. u n \<in> S) \<Longrightarrow> b \<in> T \<Longrightarrow> u \<longlonglongrightarrow> b \<Longrightarrow> convergent (\<lambda>n. f (u n))"
           "\<And>b. b \<in> T \<Longrightarrow> \<exists>u. (\<forall>n. u n \<in> S) \<and> u \<longlonglongrightarrow> b \<and> ((\<lambda>n. f (u n)) \<longlonglongrightarrow> f b)"
   shows "continuous (at b within (S \<union> T)) f"
 proof -
   have first_step: "(\<lambda>n. f (u n)) \<longlonglongrightarrow> f c" if "\<And>n. u n \<in> S" "u \<longlonglongrightarrow> c" "c \<in> T" for u c
   proof -
     obtain v where v: "\<And>n. v n \<in> S" "v \<longlonglongrightarrow> c" "(\<lambda>n. f (v n)) \<longlonglongrightarrow> f c"
       using assms(3)[OF \<open>c \<in> T\<close>] by blast
     then have A: "even_odd_interpolate u v \<longlonglongrightarrow> c"
       unfolding even_odd_interpolate_filterlim[symmetric] using \<open>u \<longlonglongrightarrow> c\<close> by auto
     moreover have B: "\<forall>n. even_odd_interpolate u v n \<in> S"
       using \<open>\<And>n. u n \<in> S\<close> \<open>\<And>n. v n \<in> S\<close> unfolding even_odd_interpolate_def by auto
     have "convergent (\<lambda>n. f (even_odd_interpolate u v n))"
       by (rule assms(2)[OF B \<open>c \<in> T\<close> A])
     then obtain m where "(\<lambda>n. f (even_odd_interpolate u v n)) \<longlonglongrightarrow> m"
       unfolding convergent_def by auto
     then have "even_odd_interpolate (f o u) (f o v) \<longlonglongrightarrow> m"
       unfolding even_odd_interpolate_compose unfolding comp_def by auto
     then have "(f o u) \<longlonglongrightarrow> m" "(f o v) \<longlonglongrightarrow> m"
       unfolding even_odd_interpolate_filterlim[symmetric] by auto
     then have "m = f c" using v(3) unfolding comp_def using LIMSEQ_unique by auto
     then show ?thesis using \<open>(f o u) \<longlonglongrightarrow> m\<close> unfolding comp_def by auto
   qed
   show "continuous (at b within (S \<union> T)) f"
   proof (rule ccontr)
     assume "\<not> ?thesis"
     then obtain U where U: "open U" "f b \<in> U" "\<not>(\<forall>\<^sub>F x in at b within S \<union> T. f x \<in> U)"
       unfolding continuous_within tendsto_def[where l = "f b"] using sequentially_imp_eventually_nhds_within by auto
     have "\<exists>V W. open V \<and> open W \<and> f b \<in> V \<and> (UNIV - U) \<subseteq> W \<and> V \<inter> W = {}"
       apply (rule t3_space) using U by auto
     then obtain V W where VW: "open V" "open W" "f b \<in> V" "UNIV - U \<subseteq> W" "V \<inter> W = {}"
       by auto
 
     obtain A :: "nat \<Rightarrow> 'a set" where *:
       "\<And>i. open (A i)"
       "\<And>i. b \<in> A i"
       "\<And>F. \<forall>n. F n \<in> A n \<Longrightarrow> F \<longlonglongrightarrow> b"
       by (rule first_countable_topology_class.countable_basis) blast
     with * U(3) have "\<exists>F. \<forall>n. F n \<in> S \<union> T \<and> F n \<in> A n \<and> \<not> (f(F n) \<in> U)"
       unfolding at_within_def eventually_inf_principal eventually_nhds
       by (intro choice) (meson DiffE)
     then obtain F where F: "\<And>n. F n \<in> S \<union> T" "\<And>n. F n \<in> A n" "\<And>n. f(F n) \<notin> U"
       by auto
 
     have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> f y \<in> W" for n
     proof (cases "F n \<in> S")
       case True
       show ?thesis apply (rule exI[of _ "F n"]) using F VW True by auto
     next
       case False
       then have "F n \<in> T" using \<open>F n \<in> S \<union> T\<close> by auto
       obtain u where u: "\<And>p. u p \<in> S" "u \<longlonglongrightarrow> F n" "(\<lambda>p. f (u p)) \<longlonglongrightarrow> f(F n)"
         using assms(3)[OF \<open>F n \<in> T\<close>] by auto
       moreover have "f(F n) \<in> W" using F VW by auto
       ultimately have "eventually (\<lambda>p. f (u p) \<in> W) sequentially"
         using \<open>open W\<close> by (simp add: tendsto_def)
       moreover have "eventually (\<lambda>p. u p \<in> A n) sequentially"
         using \<open>F n \<in> A n\<close> u \<open>open (A n)\<close> by (simp add: tendsto_def)
       ultimately have "\<exists>p. f(u p) \<in> W \<and> u p \<in> A n"
         using eventually_False_sequentially eventually_elim2 by blast
       then show ?thesis using u(1) by auto
     qed
     then have "\<exists>u. \<forall>n. u n \<in> S \<and> u n \<in> A n \<and> f (u n) \<in> W"
       by (auto intro: choice)
     then obtain u where u: "\<And>n. u n \<in> S" "\<And>n. u n \<in> A n" "\<And>n. f (u n) \<in> W"
       by blast
     then have "u \<longlonglongrightarrow> b" using *(3) by auto
     then have "(\<lambda>n. f (u n)) \<longlonglongrightarrow> f b" using first_step assms u by auto
     then have "eventually (\<lambda>n. f (u n) \<in> V) sequentially"
       using VW by (simp add: tendsto_def)
     then have "\<exists>n. f (u n) \<in> V"
       using eventually_False_sequentially eventually_elim2 by blast
     then show False
       using u(3) \<open>V \<inter> W = {}\<close> by auto
   qed
 qed
 
 text \<open>We can specialize the previous statement to the common case where one already knows the
 sequential continuity of $f$ along sequences in $S$ converging to a point in $T$. This will be the
 case in most --but not all-- applications. This is a straightforward application of the above
 criterion.\<close>
 
 proposition continuous_at_extension_sequentially:
   fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::t3_space"
   assumes "a \<in> T"
           "T \<subseteq> closure S"
           "\<And>u b. (\<forall>n. u n \<in> S) \<Longrightarrow> b \<in> T \<Longrightarrow> u \<longlonglongrightarrow> b \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f b"
   shows "continuous (at a within (S \<union> T)) f"
 apply (rule continuous_at_extension_sequentially'[OF \<open>a \<in> T\<close>])
 using assms(3) convergent_def apply blast
 by (metis assms(2) assms(3) closure_sequential subset_iff)
 
 text \<open>We also give global versions. We can only express the continuity on $T$, so
 this is slightly weaker than the previous statements since we are not saying anything on inside
 sequences tending to $T$ -- but in cases where $T$ contains $S$ these statements contain all the
 information.\<close>
 
 lemma continuous_on_extension_sequentially':
   fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::t3_space"
   assumes "\<And>u b. (\<forall>n. u n \<in> S) \<Longrightarrow> b \<in> T \<Longrightarrow> u \<longlonglongrightarrow> b \<Longrightarrow> convergent (\<lambda>n. f (u n))"
           "\<And>b. b \<in> T \<Longrightarrow> \<exists>u. (\<forall>n. u n \<in> S) \<and> u \<longlonglongrightarrow> b \<and> ((\<lambda>n. f (u n)) \<longlonglongrightarrow> f b)"
   shows "continuous_on T f"
 unfolding continuous_on_eq_continuous_within apply (auto intro!: continuous_within_subset[of _ "S \<union> T" f T])
 by (intro continuous_at_extension_sequentially'[OF _ assms], auto)
 
 lemma continuous_on_extension_sequentially:
   fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::t3_space"
   assumes "T \<subseteq> closure S"
           "\<And>u b. (\<forall>n. u n \<in> S) \<Longrightarrow> b \<in> T \<Longrightarrow> u \<longlonglongrightarrow> b \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f b"
   shows "continuous_on T f"
 unfolding continuous_on_eq_continuous_within apply (auto intro!: continuous_within_subset[of _ "S \<union> T" f T])
 by (intro continuous_at_extension_sequentially[OF _ assms], auto)
 
 
 subsubsection \<open>Homeomorphisms\<close>
 
-lemma homeomorphism_cong:
-  "homeomorphism X' Y' f' g'" if "homeomorphism X Y f g"
-    "X' = X" "Y' = Y" "\<And>x. x \<in> X \<Longrightarrow> f' x = f x" "\<And>y. y \<in> Y \<Longrightarrow> g' y = g y"
-  using that by (auto simp add: homeomorphism_def)
-
-lemma homeomorphism_empty [simp]:
-  "homeomorphism {} {} f g"
-unfolding homeomorphism_def by auto
-
 text \<open>A variant around the notion of homeomorphism, which is only expressed in terms of the
 function and not of its inverse.\<close>
 
 definition homeomorphism_on::"'a set \<Rightarrow> ('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
   where "homeomorphism_on S f = (\<exists>g. homeomorphism S (f`S) f g)"
 
 lemma homeomorphism_on_continuous:
   assumes "homeomorphism_on S f"
   shows "continuous_on S f"
 using assms unfolding homeomorphism_on_def homeomorphism_def by auto
 
 lemma homeomorphism_on_bij:
   assumes "homeomorphism_on S f"
   shows "bij_betw f S (f`S)"
 using assms unfolding homeomorphism_on_def homeomorphism_def by auto (metis inj_on_def inj_on_imp_bij_betw)
 
 lemma homeomorphism_on_homeomorphic:
   assumes "homeomorphism_on S f"
   shows "S homeomorphic (f`S)"
 using assms unfolding homeomorphism_on_def homeomorphic_def by auto
 
 lemma homeomorphism_on_compact:
   fixes f::"'a::topological_space \<Rightarrow> 'b::t2_space"
   assumes "continuous_on S f"
           "compact S"
           "inj_on f S"
   shows "homeomorphism_on S f"
 unfolding homeomorphism_on_def using homeomorphism_compact[OF assms(2) assms(1) _ assms(3)] by auto
 
 lemma homeomorphism_on_subset:
   assumes "homeomorphism_on S f"
           "T \<subseteq> S"
   shows "homeomorphism_on T f"
 using assms homeomorphism_of_subsets unfolding homeomorphism_on_def by blast
 
 lemma homeomorphism_on_empty [simp]:
   "homeomorphism_on {} f"
 unfolding homeomorphism_on_def using homeomorphism_empty[of f] by auto
 
 lemma homeomorphism_on_cong:
   assumes "homeomorphism_on X f"
           "X' = X" "\<And>x. x \<in> X \<Longrightarrow> f' x = f x"
   shows "homeomorphism_on X' f'"
 proof -
   obtain g where g:"homeomorphism X (f`X) f g"
     using assms unfolding homeomorphism_on_def by auto
   have "homeomorphism X' (f'`X') f' g"
     apply (rule homeomorphism_cong[OF g]) using assms by (auto simp add: rev_image_eqI)
   then show ?thesis
     unfolding homeomorphism_on_def by auto
 qed
 
 lemma homeomorphism_on_inverse:
   fixes f::"'a::topological_space \<Rightarrow> 'b::topological_space"
   assumes "homeomorphism_on X f"
   shows "homeomorphism_on (f`X) (inv_into X f)"
 proof -
   obtain g where g: "homeomorphism X (f`X) f g"
     using assms unfolding homeomorphism_on_def by auto
   then have "g`f`X = X"
     by (simp add: homeomorphism_def)
   then have "homeomorphism_on (f`X) g"
     unfolding homeomorphism_on_def using homeomorphism_symD[OF g] by auto
   moreover have "g x = inv_into X f x" if "x \<in> f`X" for x
     using g that unfolding homeomorphism_def by (auto, metis f_inv_into_f inv_into_into that)
   ultimately show ?thesis
     using homeomorphism_on_cong by force
 qed
 
 text \<open>Characterization of homeomorphisms in terms of sequences: a map is a homeomorphism if and
 only if it respects convergent sequences.\<close>
 
 lemma homeomorphism_on_compose:
   assumes "homeomorphism_on S f"
           "x \<in> S"
           "eventually (\<lambda>n. u n \<in> S) F"
   shows "(u \<longlongrightarrow> x) F \<longleftrightarrow> ((\<lambda>n. f (u n)) \<longlongrightarrow> f x) F"
 proof
   assume "(u \<longlongrightarrow> x) F"
   then show "((\<lambda>n. f (u n)) \<longlongrightarrow> f x) F"
     using continuous_on_tendsto_compose[OF homeomorphism_on_continuous[OF assms(1)] _ assms(2) assms(3)] by simp
 next
   assume *: "((\<lambda>n. f (u n)) \<longlongrightarrow> f x) F"
   have I: "inv_into S f (f y) = y" if "y \<in> S" for y
     using homeomorphism_on_bij[OF assms(1)] by (meson bij_betw_inv_into_left that)
   then have A: "eventually (\<lambda>n. u n = inv_into S f (f (u n))) F"
     using assms eventually_mono by force
   have "((\<lambda>n. (inv_into S f) (f (u n))) \<longlongrightarrow> (inv_into S f) (f x)) F"
     apply (rule continuous_on_tendsto_compose[OF homeomorphism_on_continuous[OF homeomorphism_on_inverse[OF assms(1)]] *])
     using assms eventually_mono by (auto) fastforce
   then show "(u \<longlongrightarrow> x) F"
     unfolding tendsto_cong[OF A] I[OF \<open>x \<in> S\<close>] by simp
 qed
 
 lemma homeomorphism_on_sequentially:
   fixes f::"'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::{first_countable_topology, t2_space}"
   assumes "\<And>x u. x \<in> S \<Longrightarrow> (\<forall>n. u n \<in> S) \<Longrightarrow> u \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f x"
   shows "homeomorphism_on S f"
 proof -
   have "x = y" if "f x = f y" "x \<in> S" "y \<in> S" for x y
   proof -
     have "(\<lambda>n. f x) \<longlonglongrightarrow> f y" using that by auto
     then have "(\<lambda>n. x) \<longlonglongrightarrow> y" using assms(1) that by auto
     then show "x = y" using LIMSEQ_unique by auto
   qed
   then have "inj_on f S" by (simp add: inj_on_def)
 
   have Cf: "continuous_on S f"
     apply (rule continuous_on_sequentiallyI) using assms by auto
   define g where "g = inv_into S f"
   have Cg: "continuous_on (f`S) g"
   proof (rule continuous_on_sequentiallyI)
     fix v b assume H: "\<forall>n. v n \<in> f ` S" "b \<in> f ` S" "v \<longlonglongrightarrow> b"
     define u where "u = (\<lambda>n. g (v n))"
     define a where "a = g b"
     have "u n \<in> S" "f (u n) = v n" for n
       unfolding u_def g_def using H(1) by (auto simp add: inv_into_into f_inv_into_f)
     have "a \<in> S" "f a = b"
       unfolding a_def g_def using H(2) by (auto simp add: inv_into_into f_inv_into_f)
     show "(\<lambda>n. g(v n)) \<longlonglongrightarrow> g b"
       unfolding u_def[symmetric] a_def[symmetric] apply (rule iffD2[OF assms])
       using \<open>\<And>n. u n \<in> S\<close> \<open>a \<in> S\<close> \<open>v \<longlonglongrightarrow> b\<close>
       unfolding \<open>\<And>n. f (u n) = v n\<close> \<open>f a = b\<close> by auto
   qed
   have "homeomorphism S (f`S) f g"
     apply (rule homeomorphismI[OF Cf Cg]) unfolding g_def using \<open>inj_on f S\<close> by auto
   then show ?thesis
     unfolding homeomorphism_on_def by auto
 qed
 
 lemma homeomorphism_on_UNIV_sequentially:
   fixes f::"'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::{first_countable_topology, t2_space}"
   assumes "\<And>x u. u \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f x"
   shows "homeomorphism_on UNIV f"
 using assms by (auto intro!: homeomorphism_on_sequentially)
 
 text \<open>Now, we give similar characterizations in terms of sequences living in a dense subset. As
 in the sequential continuity criteria above, we first give a very general criterion, where the map
 does not have to be continuous on the approximating set $S$, only on the limit set $T$, without
 any a priori identification of the limit. Then, we specialize this statement to a less general
 but often more usable version.\<close>
 
 lemma homeomorphism_on_extension_sequentially_precise:
   fixes f::"'a::{first_countable_topology, t3_space} \<Rightarrow> 'b::{first_countable_topology, t3_space}"
   assumes "\<And>u b. (\<forall>n. u n \<in> S) \<Longrightarrow> b \<in> T \<Longrightarrow> u \<longlonglongrightarrow> b \<Longrightarrow> convergent (\<lambda>n. f (u n))"
           "\<And>u c. (\<forall>n. u n \<in> S) \<Longrightarrow> c \<in> f`T \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> c \<Longrightarrow> convergent u"
           "\<And>b. b \<in> T \<Longrightarrow> \<exists>u. (\<forall>n. u n \<in> S) \<and> u \<longlonglongrightarrow> b \<and> ((\<lambda>n. f (u n)) \<longlonglongrightarrow> f b)"
           "\<And>n. u n \<in> S \<union> T" "l \<in> T"
   shows "u \<longlonglongrightarrow> l \<longleftrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f l"
 proof
   assume H: "u \<longlonglongrightarrow> l"
   have "continuous (at l within (S \<union> T)) f"
     apply (rule continuous_at_extension_sequentially'[OF \<open>l \<in> T\<close>]) using assms(1) assms(3) by auto
   then show "(\<lambda>n. f (u n)) \<longlonglongrightarrow> f l"
     apply (rule continuous_within_tendsto_compose) using H assms(4) by auto
 next
   text \<open>For the reverse implication, we would like to use the continuity criterion
   \verb+ continuous_at_extension_sequentially'+ applied to the inverse of $f$. Unfortunately, this
   inverse is only well defined on $T$, while our sequence takes values in $S \cup T$. So, instead,
   we redo by hand the proof of the continuity criterion, but in the opposite direction.\<close>
   assume H: "(\<lambda>n. f (u n)) \<longlonglongrightarrow> f l"
   show "u \<longlonglongrightarrow> l"
   proof (rule ccontr)
     assume "\<not> ?thesis"
     then obtain U where U: "open U" "l \<in> U" "\<not>(\<forall>\<^sub>F n in sequentially. u n \<in> U)"
       unfolding continuous_within tendsto_def[where l = l] using sequentially_imp_eventually_nhds_within by auto
     obtain A :: "nat \<Rightarrow> 'b set" where *:
       "\<And>i. open (A i)"
       "\<And>i. f l \<in> A i"
       "\<And>F. \<forall>n. F n \<in> A n \<Longrightarrow> F \<longlonglongrightarrow> f l"
       by (rule first_countable_topology_class.countable_basis) blast
     have B: "eventually (\<lambda>n. f (u n) \<in> A i) sequentially" for i
       using \<open>open (A i)\<close> \<open>f l \<in> A i\<close> H topological_tendstoD by fastforce
     have M: "\<exists>r. r \<ge> N \<and> (u r \<notin> U) \<and> f (u r) \<in> A i" for N i
       using U(3) B[of i] unfolding eventually_sequentially by (meson dual_order.trans le_cases)
     have "\<exists>r. \<forall>n. (u (r n) \<notin> U \<and> f (u (r n)) \<in> A n) \<and> r (Suc n) \<ge> r n + 1"
       apply (rule dependent_nat_choice) using M by auto
     then obtain r where r: "\<And>n. u (r n) \<notin> U" "\<And>n. f (u (r n)) \<in> A n" "\<And>n. r (Suc n) \<ge> r n + 1"
       by auto
     then have "strict_mono r"
       by (metis Suc_eq_plus1 Suc_le_lessD strict_monoI_Suc)
 
     have "\<exists>V W. open V \<and> open W \<and> l \<in> V \<and> (UNIV - U) \<subseteq> W \<and> V \<inter> W = {}"
       apply (rule t3_space) using U by auto
     then obtain V W where VW: "open V" "open W" "l \<in> V" "UNIV - U \<subseteq> W" "V \<inter> W = {}"
       by auto
 
     have "\<exists>z. z \<in> S \<and> f z \<in> A n \<and> z \<in> W" for n
     proof -
       define z where "z = u (r n)"
       have "f z \<in> A n" unfolding z_def using r(2) by auto
       have "z \<in> S \<union> T" "z \<notin> U"
         unfolding z_def using r(1) assms(4) by auto
       then have "z \<in> W" using VW by auto
       show ?thesis
       proof (cases "z \<in> T")
         case True
         obtain u::"nat \<Rightarrow> 'a" where u: "\<And>p. u p \<in> S" "u \<longlonglongrightarrow> z" "(\<lambda>p. f (u p)) \<longlonglongrightarrow> f z"
           using assms(3)[OF \<open>z \<in> T\<close>] by auto
         then have "eventually (\<lambda>p. f (u p) \<in> A n) sequentially"
           using \<open>open (A n)\<close> \<open>f z \<in> A n\<close> unfolding tendsto_def by simp
         moreover have "eventually (\<lambda>p. u p \<in> W) sequentially"
           using \<open>open W\<close> \<open>z \<in> W\<close> u unfolding tendsto_def by simp
         ultimately have "\<exists>p. u p \<in> W \<and> f (u p) \<in> A n"
           using eventually_False_sequentially eventually_elim2 by blast
         then show ?thesis using u(1) by auto
       next
         case False
         then have "z \<in> S" using \<open>z \<in> S \<union> T\<close> by auto
         then show ?thesis using \<open>f z \<in> A n\<close> \<open>z \<in> W\<close> by auto
       qed
     qed
     then have "\<exists>v. \<forall>n. v n \<in> S \<and> f (v n) \<in> A n \<and> v n \<in> W"
       by (auto intro: choice)
     then obtain v where v: "\<And>n. v n \<in> S" "\<And>n. f (v n) \<in> A n" "\<And>n. v n \<in> W"
       by blast
     then have I: "(\<lambda>n. f (v n)) \<longlonglongrightarrow> f l" using *(3) by auto
 
     obtain w where w: "\<And>n. w n \<in> S" "w \<longlonglongrightarrow> l" "((\<lambda>n. f (w n)) \<longlonglongrightarrow> f l)"
       using assms(3)[OF \<open>l \<in> T\<close>] by auto
     have "even_odd_interpolate (f o v) (f o w) \<longlonglongrightarrow> f l"
       unfolding even_odd_interpolate_filterlim[symmetric] comp_def using v w I by auto
     then have *: "(\<lambda>n. f (even_odd_interpolate v w n)) \<longlonglongrightarrow> f l"
       unfolding even_odd_interpolate_compose unfolding comp_def by auto
     have "convergent (even_odd_interpolate v w)"
       apply (rule assms(2)[OF _ _ *])
       unfolding even_odd_interpolate_def using v(1) w(1) \<open>l \<in> T\<close> by auto
     then obtain z where "even_odd_interpolate v w \<longlonglongrightarrow> z"
       unfolding convergent_def by auto
     then have *: "v \<longlonglongrightarrow> z" "w \<longlonglongrightarrow> z" unfolding even_odd_interpolate_filterlim[symmetric] by auto
     then have "z = l" using v(2) w(2) LIMSEQ_unique by auto
     then have "v \<longlonglongrightarrow> l" using * by simp
     then have "eventually (\<lambda>n. v n \<in> V) sequentially"
       using VW by (simp add: tendsto_def)
     then have "\<exists>n. v n \<in> V"
       using eventually_False_sequentially eventually_elim2 by blast
     then show False
       using v(3) \<open>V \<inter> W = {}\<close> by auto
   qed
 qed
 
 lemma homeomorphism_on_extension_sequentially':
   fixes f::"'a::{first_countable_topology, t3_space} \<Rightarrow> 'b::{first_countable_topology, t3_space}"
   assumes "\<And>u b. (\<forall>n. u n \<in> S) \<Longrightarrow> b \<in> T \<Longrightarrow> u \<longlonglongrightarrow> b \<Longrightarrow> convergent (\<lambda>n. f (u n))"
           "\<And>u c. (\<forall>n. u n \<in> S) \<Longrightarrow> c \<in> f`T \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> c \<Longrightarrow> convergent u"
           "\<And>b. b \<in> T \<Longrightarrow> \<exists>u. (\<forall>n. u n \<in> S) \<and> u \<longlonglongrightarrow> b \<and> ((\<lambda>n. f (u n)) \<longlonglongrightarrow> f b)"
   shows "homeomorphism_on T f"
 apply (rule homeomorphism_on_sequentially, rule homeomorphism_on_extension_sequentially_precise[of S T])
 using assms by auto
 
 proposition homeomorphism_on_extension_sequentially:
   fixes f::"'a::{first_countable_topology, t3_space} \<Rightarrow> 'b::{first_countable_topology, t3_space}"
   assumes "\<And>u b. (\<forall>n. u n \<in> S) \<Longrightarrow> u \<longlonglongrightarrow> b \<longleftrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f b"
           "T \<subseteq> closure S"
   shows "homeomorphism_on T f"
 apply (rule homeomorphism_on_extension_sequentially'[of S])
 using assms(1) convergent_def apply fastforce
 using assms(1) convergent_def apply blast
 by (metis assms(1) assms(2) closure_sequential subsetCE)
 
 lemma homeomorphism_on_UNIV_extension_sequentially:
   fixes f::"'a::{first_countable_topology, t3_space} \<Rightarrow> 'b::{first_countable_topology, t3_space}"
   assumes "\<And>u b. (\<forall>n. u n \<in> S) \<Longrightarrow> u \<longlonglongrightarrow> b \<longleftrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f b"
           "closure S = UNIV"
   shows "homeomorphism_on UNIV f"
 apply (rule homeomorphism_on_extension_sequentially[of S]) using assms by auto
 
 
 subsubsection \<open>Proper spaces\<close>
 
 text \<open>Proper spaces, i.e., spaces in which every closed ball is compact -- or, equivalently,
 any closed bounded set is compact.\<close>
 
 definition proper::"('a::metric_space) set \<Rightarrow> bool"
   where "proper S \<equiv> (\<forall> x r. compact (cball x r \<inter> S))"
 
 lemma properI:
   assumes "\<And>x r. compact (cball x r \<inter> S)"
   shows "proper S"
 using assms unfolding proper_def by auto
 
 lemma proper_compact_cball:
   assumes "proper (UNIV::'a::metric_space set)"
   shows "compact (cball (x::'a) r)"
 using assms unfolding proper_def by auto
 
 lemma proper_compact_bounded_closed:
   assumes "proper (UNIV::'a::metric_space set)" "closed (S::'a set)" "bounded S"
   shows "compact S"
 proof -
   obtain x r where "S \<subseteq> cball x r"
     using \<open>bounded S\<close> bounded_subset_cball by blast
   then have *: "S = S \<inter> cball x r"
     by auto
   show ?thesis
     apply (subst *, rule closed_Int_compact) using assms unfolding proper_def by auto
 qed
 
 lemma proper_real [simp]:
   "proper (UNIV::real set)"
 unfolding proper_def by auto
 
 lemma complete_of_proper:
   assumes "proper S"
   shows "complete S"
 proof -
   have "\<exists>l\<in>S. u \<longlonglongrightarrow> l" if "Cauchy u" "\<And>n. u n \<in> S" for u
   proof -
     have "bounded (range u)"
       using \<open>Cauchy u\<close> cauchy_imp_bounded by auto
     then obtain x r where *: "\<And>n. dist x (u n) \<le> r"
       unfolding bounded_def by auto
     then have "u n \<in> (cball x r) \<inter> S" for n using \<open>u n \<in> S\<close> by auto
     moreover have "complete ((cball x r) \<inter> S)"
       apply (rule compact_imp_complete) using assms unfolding proper_def by auto
     ultimately show ?thesis
       unfolding complete_def using \<open>Cauchy u\<close> by auto
   qed
   then show ?thesis
     unfolding complete_def by auto
 qed
 
 lemma proper_of_compact:
   assumes "compact S"
   shows "proper S"
 using assms by (auto intro: properI)
 
 lemma proper_Un:
   assumes "proper A" "proper B"
   shows "proper (A \<union> B)"
 using assms unfolding proper_def by (auto simp add: compact_Un inf_sup_distrib1)
 
 subsubsection \<open>Miscellaneous topology\<close>
 
 text \<open>When manipulating the triangle inequality, it is very frequent to deal with 4 points
 (and automation has trouble doing it automatically). Even sometimes with 5 points...\<close>
 
 lemma dist_triangle4 [mono_intros]:
   "dist x t \<le> dist x y + dist y z + dist z t"
 using dist_triangle[of x z y] dist_triangle[of x t z] by auto
 
 lemma dist_triangle5 [mono_intros]:
   "dist x u \<le> dist x y + dist y z + dist z t + dist t u"
 using dist_triangle4[of x u y z] dist_triangle[of z u t] by auto
 
 text \<open>A thickening of a compact set is closed.\<close>
 
 lemma compact_has_closed_thickening:
   assumes "compact C"
           "continuous_on C f"
   shows "closed (\<Union>x\<in>C. cball x (f x))"
 proof (auto simp add: closed_sequential_limits)
   fix u l assume *: "\<forall>n::nat. \<exists>x\<in>C. dist x (u n) \<le> f x" "u \<longlonglongrightarrow> l"
   have "\<exists>x::nat\<Rightarrow>'a. \<forall>n. x n \<in> C \<and> dist (x n) (u n) \<le> f (x n)"
     apply (rule choice) using * by auto
   then obtain x::"nat \<Rightarrow> 'a" where x: "\<And>n. x n \<in> C" "\<And>n. dist (x n) (u n) \<le> f (x n)"
     by blast
   obtain r c where "strict_mono r" "c \<in> C" "(x o r) \<longlonglongrightarrow> c"
     using x(1) \<open>compact C\<close> by (meson compact_eq_seq_compact_metric seq_compact_def)
   then have "c \<in> C" using x(1) \<open>compact C\<close> by auto
   have lim: "(\<lambda>n. f (x (r n)) - dist (x (r n)) (u (r n))) \<longlonglongrightarrow> f c - dist c l"
     apply (intro tendsto_intros, rule continuous_on_tendsto_compose[of C f])
     using *(2) x(1) \<open>(x o r) \<longlonglongrightarrow> c\<close> \<open>continuous_on C f\<close> \<open>c \<in> C\<close> \<open>strict_mono r\<close> LIMSEQ_subseq_LIMSEQ
     unfolding comp_def by auto
   have "f c - dist c l \<ge> 0" apply (rule LIMSEQ_le_const[OF lim]) using x(2) by auto
   then show "\<exists>x\<in>C. dist x l \<le> f x" using \<open>c \<in> C\<close> by auto
 qed
 
 text \<open>congruence rule for continuity. The assumption that $f y = g y$ is necessary since \verb+at x+
 is the pointed neighborhood at $x$.\<close>
 
 lemma continuous_within_cong:
   assumes "continuous (at y within S) f"
           "eventually (\<lambda>x. f x = g x) (at y within S)"
           "f y = g y"
   shows "continuous (at y within S) g"
-using assms(1) assms(2) Lim_transform_eventually unfolding continuous_within assms(3) by auto
+  using assms continuous_within filterlim_cong by fastforce
 
 text \<open>A function which tends to infinity at infinity, on a proper set, realizes its infimum\<close>
 
 lemma continuous_attains_inf_proper:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::linorder_topology"
   assumes "proper s" "a \<in> s"
           "continuous_on s f"
           "\<And>z. z \<in> s - cball a r \<Longrightarrow> f z \<ge> f a"
   shows "\<exists>x\<in>s. \<forall>y\<in>s. f x \<le> f y"
 proof (cases "r \<ge> 0")
   case True
   have "\<exists>x\<in>cball a r \<inter> s. \<forall>y \<in> cball a r \<inter> s. f x \<le> f y"
     apply (rule continuous_attains_inf) using assms True unfolding proper_def apply (auto simp add: continuous_on_subset)
     using centre_in_cball by blast
   then obtain x where x: "x \<in> cball a r \<inter> s" "\<And>y. y \<in> cball a r \<inter> s \<Longrightarrow> f x \<le> f y"
     by auto
   have "f x \<le> f y" if "y \<in> s" for y
   proof (cases "y \<in> cball a r")
     case True
     then show ?thesis using x(2) that by auto
   next
     case False
     have "f x \<le> f a"
       apply (rule x(2)) using assms True by auto
     then show ?thesis using assms(4)[of y] that False by auto
   qed
   then show ?thesis using x(1) by auto
 next
   case False
   show ?thesis
     apply (rule bexI[of _ a]) using assms False by auto
 qed
 
 subsubsection \<open>Measure of balls\<close>
 
-text \<open>The image of a ball by an affine map is still a ball, with explicit center and radius.\<close>
+text \<open>The image of a ball by an affine map is still a ball, with explicit center and radius. (Now unused)\<close>
 
 lemma affine_image_ball [simp]:
   "(\<lambda>y. R *\<^sub>R y + x) ` cball 0 1 = cball (x::('a::real_normed_vector)) \<bar>R\<bar>"
 proof
   have "dist x (R *\<^sub>R y + x) \<le> \<bar>R\<bar>" if "dist 0 y \<le> 1" for y
   proof -
     have "dist x (R *\<^sub>R y + x) = norm ((R *\<^sub>R y + x) - x)" by (simp add: dist_norm)
     also have "... = \<bar>R\<bar> * norm y" by auto
     finally show ?thesis using that by (simp add: mult_left_le)
   qed
   then show "(\<lambda>y. R *\<^sub>R y + x) ` cball 0 1 \<subseteq> cball x \<bar>R\<bar>" by auto
 
   show "cball x \<bar>R\<bar> \<subseteq> (\<lambda>y. R *\<^sub>R y + x) ` cball 0 1"
   proof (cases "\<bar>R\<bar> = 0")
     case True
     then have "cball x \<bar>R\<bar> = {x}" by auto
     moreover have "x = R *\<^sub>R 0 + x \<and> 0 \<in> cball 0 1" by auto
     ultimately show ?thesis by auto
   next
     case False
     have "z \<in> (\<lambda>y. R *\<^sub>R y + x) ` cball 0 1" if "z \<in> cball x \<bar>R\<bar>" for z
     proof -
       define y where "y = (z - x) /\<^sub>R R"
       have "R *\<^sub>R y + x = z" unfolding y_def using False by auto
       moreover have "y \<in> cball 0 1"
         using \<open>z \<in> cball x \<bar>R\<bar>\<close> False unfolding y_def by (auto simp add: dist_norm[symmetric] divide_simps dist_commute)
       ultimately show ?thesis by auto
     qed
     then show ?thesis by auto
   qed
 qed
 
 text \<open>From the rescaling properties of Lebesgue measure in a euclidean space, it follows that
 the measure of any ball can be expressed in terms of the measure of the unit ball.\<close>
 
 lemma lebesgue_measure_ball:
   assumes "R \<ge> 0"
   shows "measure lborel (cball (x::('a::euclidean_space)) R) = R^(DIM('a)) * measure lborel (cball (0::'a) 1)"
         "emeasure lborel (cball (x::('a::euclidean_space)) R) = R^(DIM('a)) * emeasure lborel (cball (0::'a) 1)"
-using measure_lebesgue_affine[of R x "cball 0 1"] emeasure_lebesgue_affine[of R x "cball 0 1"] assms
-unfolding affine_image_ball by (auto simp add: ennreal_power)
+  apply (simp add: assms content_cball)
+  by (simp add: assms emeasure_cball ennreal_mult' ennreal_power mult.commute)
 
 text \<open>We show that the unit ball has positive measure -- this is obvious, but useful. We could
 show it by arguing that it contains a box, whose measure can be computed, but instead we say
 that if the measure vanished then the measure of any ball would also vanish, contradicting the
 fact that the space has infinite measure. This avoids all computations.\<close>
 
 lemma lebesgue_measure_ball_pos:
   "emeasure lborel (cball (0::'a::euclidean_space) 1) > 0"
   "measure lborel (cball (0::'a::euclidean_space) 1) > 0"
 proof -
   show "emeasure lborel (cball (0::'a::euclidean_space) 1) > 0"
   proof (rule ccontr)
     assume "\<not>(emeasure lborel (cball (0::'a::euclidean_space) 1) > 0)"
     then have "emeasure lborel (cball (0::'a) 1) = 0" by auto
     then have "emeasure lborel (cball (0::'a) n) = 0" for n::nat
       using lebesgue_measure_ball(2)[of "real n" 0] by (metis mult_zero_right of_nat_0_le_iff)
     then have "emeasure lborel (\<Union>n. cball (0::'a) (real n)) = 0"
       by (metis (mono_tags, lifting) borel_closed closed_cball emeasure_UN_eq_0 imageE sets_lborel subsetI)
     moreover have "(\<Union>n. cball (0::'a) (real n)) = UNIV" by (auto simp add: real_arch_simple)
     ultimately show False
       by simp
   qed
   moreover have "emeasure lborel (cball (0::'a::euclidean_space) 1) < \<infinity>"
     by (rule emeasure_bounded_finite, auto)
   ultimately show "measure lborel (cball (0::'a::euclidean_space) 1) > 0"
     by (metis borel_closed closed_cball ennreal_0 has_integral_iff_emeasure_lborel has_integral_measure_lborel less_irrefl order_refl zero_less_measure_iff)
 qed
 
 subsubsection \<open>infdist and closest point projection\<close>
 
 text \<open>The distance to a union of two sets is the minimum of the distance to the two sets.\<close>
 
 lemma infdist_union_min [mono_intros]:
   assumes "A \<noteq> {}" "B \<noteq> {}"
   shows "infdist x (A \<union> B) = min (infdist x A) (infdist x B)"
 using assms by (simp add: infdist_def cINF_union inf_real_def)
 
 text \<open>The distance to a set is non-increasing with the set.\<close>
 
 lemma infdist_mono [mono_intros]:
   assumes "A \<subseteq> B" "A \<noteq> {}"
   shows "infdist x B \<le> infdist x A"
-proof -
-  have "(INF a\<in>B. dist x a) \<le> (INF a\<in>A. dist x a)"
-    by (rule cINF_superset_mono[OF assms(2) _ assms(1)], auto)
-  then show ?thesis
-    unfolding infdist_def using assms by auto
-qed
+  by (simp add: assms infdist_eq_setdist setdist_subset_right)
 
 text \<open>If a set is proper, then the infimum of the distances to this set is attained.\<close>
 
 lemma infdist_proper_attained:
   assumes "proper C" "C \<noteq> {}"
   shows "\<exists>c\<in>C. infdist x C = dist x c"
 proof -
   obtain a where "a \<in> C" using assms by auto
   have *: "dist x a \<le> dist x z" if "dist a z \<ge> 2 * dist a x" for z
   proof -
     have "2 * dist a x \<le> dist a z" using that by simp
     also have "... \<le> dist a x + dist x z" by (intro mono_intros)
     finally show ?thesis by (simp add: dist_commute)
   qed
   have "\<exists>c\<in>C. \<forall>d\<in>C. dist x c \<le> dist x d"
     apply (rule continuous_attains_inf_proper[OF assms(1) \<open>a \<in> C\<close>, of _ "2 * dist a x"])
     using * by (auto intro: continuous_intros)
   then show ?thesis unfolding infdist_def using \<open>C \<noteq> {}\<close>
     by (metis antisym bdd_below_image_dist cINF_lower le_cINF_iff)
 qed
 
 lemma infdist_almost_attained:
   assumes "infdist x X < a" "X \<noteq> {}"
   shows "\<exists>y\<in>X. dist x y < a"
 using assms using cInf_less_iff[of "(dist x)`X"] unfolding infdist_def by auto
 
 lemma infdist_triangle_abs [mono_intros]:
   "\<bar>infdist x A - infdist y A\<bar> \<le> dist x y"
 by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle)
 
 text \<open>The next lemma is missing in the library, contrary to its cousin \verb+continuous_infdist+.\<close>
 
 text \<open>The infimum of the distance to a singleton set is simply the distance to the unique
 member of the set.\<close>
 
-lemma infdist_point [simp]:
-  "infdist x {y} = dist x y"
-unfolding infdist_def by (metis cInf_singleton image_empty image_insert insert_not_empty)
-
 text \<open>The closest point projection of $x$ on $A$. It is not unique, so we choose one point realizing the minimal
 distance. And if there is no such point, then we use $x$, to make some statements true without any
 assumption.\<close>
 
 definition proj_set::"'a::metric_space \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where "proj_set x A = {y \<in> A. dist x y = infdist x A}"
 
 definition distproj::"'a::metric_space \<Rightarrow> 'a set \<Rightarrow> 'a"
   where "distproj x A = (if proj_set x A \<noteq> {} then SOME y. y \<in> proj_set x A else x)"
 
 lemma proj_setD:
   assumes "y \<in> proj_set x A"
   shows "y \<in> A" "dist x y = infdist x A"
 using assms unfolding proj_set_def by auto
 
 lemma proj_setI:
   assumes "y \<in> A" "dist x y \<le> infdist x A"
   shows "y \<in> proj_set x A"
 using assms infdist_le[OF \<open>y \<in> A\<close>, of x] unfolding proj_set_def by auto
 
 lemma proj_setI':
   assumes "y \<in> A" "\<And>z. z \<in> A \<Longrightarrow> dist x y \<le> dist x z"
   shows "y \<in> proj_set x A"
 proof (rule proj_setI[OF \<open>y \<in> A\<close>])
   show "dist x y \<le> infdist x A"
     apply (subst infdist_notempty)
     using assms by (auto intro!: cInf_greatest)
 qed
 
 lemma distproj_in_proj_set:
   assumes "proj_set x A \<noteq> {}"
   shows "distproj x A \<in> proj_set x A"
         "distproj x A \<in> A"
         "dist x (distproj x A) = infdist x A"
 proof -
   show "distproj x A \<in> proj_set x A"
     using assms unfolding distproj_def using some_in_eq by auto
   then show "distproj x A \<in> A" "dist x (distproj x A) = infdist x A"
     unfolding proj_set_def by auto
 qed
 
 lemma proj_set_nonempty_of_proper:
   assumes "proper A" "A \<noteq> {}"
   shows "proj_set x A \<noteq> {}"
 proof -
   have "\<exists>y. y \<in> A \<and> dist x y = infdist x A"
     using infdist_proper_attained[OF assms, of x] by auto
   then show "proj_set x A \<noteq> {}" unfolding proj_set_def by auto
 qed
 
 lemma distproj_self [simp]:
   assumes "x \<in> A"
   shows "proj_set x A = {x}"
         "distproj x A = x"
 proof -
   show "proj_set x A = {x}"
     unfolding proj_set_def using assms by auto
   then show "distproj x A = x"
     unfolding distproj_def by auto
 qed
 
 lemma distproj_closure [simp]:
   assumes "x \<in> closure A"
   shows "distproj x A = x"
 proof (cases "proj_set x A \<noteq> {}")
   case True
   show ?thesis
     using distproj_in_proj_set(3)[OF True] assms
     by (metis closure_empty dist_eq_0_iff distproj_self(2) in_closure_iff_infdist_zero)
 next
   case False
   then show ?thesis unfolding distproj_def by auto
 qed
 
 lemma distproj_le:
   assumes "y \<in> A"
   shows "dist x (distproj x A) \<le> dist x y"
 proof (cases "proj_set x A \<noteq> {}")
   case True
   show ?thesis using distproj_in_proj_set(3)[OF True] infdist_le[OF assms] by auto
 next
   case False
   then show ?thesis unfolding distproj_def by auto
 qed
 
 lemma proj_set_dist_le:
   assumes "y \<in> A" "p \<in> proj_set x A"
   shows "dist x p \<le> dist x y"
   using assms infdist_le unfolding proj_set_def by auto
 
 subsection \<open>Material on ereal and ennreal\<close>
 
 text \<open>We add the simp rules that we needed to make all computations become more or less automatic.\<close>
 
 lemma ereal_of_real_of_ereal_iff [simp]:
   "ereal(real_of_ereal x) = x \<longleftrightarrow> x \<noteq> \<infinity> \<and> x \<noteq> - \<infinity>"
   "x = ereal(real_of_ereal x) \<longleftrightarrow> x \<noteq> \<infinity> \<and> x \<noteq> - \<infinity>"
 by (metis MInfty_neq_ereal(1) PInfty_neq_ereal(2) real_of_ereal.elims)+
 
-lemma inverse_eq_infinity_iff_eq_zero [simp]:
-  "1/(x::ereal) = \<infinity> \<longleftrightarrow> x = 0"
-by (simp add: divide_ereal_def)
-
 declare ereal_inverse_eq_0 [simp]
 declare ereal_0_gt_inverse [simp]
 declare ereal_inverse_le_0_iff [simp]
 declare ereal_divide_eq_0_iff [simp]
 declare ereal_mult_le_0_iff [simp]
 declare ereal_zero_le_0_iff [simp]
 declare ereal_mult_less_0_iff [simp]
 declare ereal_zero_less_0_iff [simp]
 declare ereal_uminus_eq_reorder [simp]
 declare ereal_minus_le_iff [simp]
 
 lemma ereal_inverse_noteq_minus_infinity [simp]:
   "1/(x::ereal) \<noteq> -\<infinity>"
 by (simp add: divide_ereal_def)
 
 lemma ereal_inverse_positive_iff_nonneg_not_infinity [simp]:
   "0 < 1/(x::ereal) \<longleftrightarrow> (x \<ge> 0 \<and> x \<noteq> \<infinity>)"
 by (cases x, auto simp add: one_ereal_def)
 
 lemma ereal_inverse_negative_iff_nonpos_not_infinity' [simp]:
   "0 > inverse (x::ereal) \<longleftrightarrow> (x < 0 \<and> x \<noteq> -\<infinity>)"
 by (cases x, auto simp add: one_ereal_def)
 
 lemma ereal_divide_pos_iff [simp]:
   "0 < x/(y::ereal) \<longleftrightarrow> (y \<noteq> \<infinity> \<and> y \<noteq> -\<infinity>) \<and> ((x > 0 \<and> y > 0) \<or> (x < 0 \<and> y < 0) \<or> (y = 0 \<and> x > 0))"
 unfolding divide_ereal_def by auto
 
 lemma ereal_divide_neg_iff [simp]:
   "0 > x/(y::ereal) \<longleftrightarrow> (y \<noteq> \<infinity> \<and> y \<noteq> -\<infinity>) \<and> ((x > 0 \<and> y < 0) \<or> (x < 0 \<and> y > 0) \<or> (y = 0 \<and> x < 0))"
 unfolding divide_ereal_def by auto
 
-lemma ereal_distrib_left:
-  fixes a b c :: ereal
-  assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>"
-    and "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>"
-    and "\<bar>c\<bar> \<noteq> \<infinity>"
-  shows "c * (a + b) = c * a + c * b"
-using assms
-by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
-
-lemma ereal_distrib_minus_left:
-  fixes a b c :: ereal
-  assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
-    and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
-    and "\<bar>c\<bar> \<noteq> \<infinity>"
-  shows "c * (a - b) = c * a - c * b"
-using assms
-by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
-
-lemma ereal_distrib_minus_right:
-  fixes a b c :: ereal
-  assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
-    and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
-    and "\<bar>c\<bar> \<noteq> \<infinity>"
-  shows "(a - b) * c = a * c - b * c"
-using assms
-by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
-
-text \<open>The next one is missing close to its friend \verb+Liminf_ereal_mult_right+.\<close>
-
-lemma Liminf_ereal_mult_left:
-  assumes "F \<noteq> bot" "(c::real) \<ge> 0"
-    shows "Liminf F (\<lambda>n. ereal c * f n) = ereal c * Liminf F f"
-using Liminf_ereal_mult_right[OF assms] by (subst (1 2) mult.commute)
-
-
 text \<open>More additions to \verb+mono_intros+.\<close>
 
 lemma ereal_leq_imp_neg_leq [mono_intros]:
   fixes x y::ereal
   assumes "x \<le> y"
   shows "-y \<le> -x"
 using assms by auto
 
 lemma ereal_le_imp_neg_le [mono_intros]:
   fixes x y::ereal
   assumes "x < y"
   shows "-y < -x"
 using assms by auto
 
 declare ereal_mult_left_mono [mono_intros]
 declare ereal_mult_right_mono [mono_intros]
 declare ereal_mult_strict_right_mono [mono_intros]
 declare ereal_mult_strict_left_mono [mono_intros]
 
 text \<open>Monotonicity of basic inclusions.\<close>
 
 lemma ennreal_mono':
   "mono ennreal"
 by (simp add: ennreal_leI monoI)
 
 lemma enn2ereal_mono':
   "mono enn2ereal"
 by (simp add: less_eq_ennreal.rep_eq mono_def)
 
 lemma e2ennreal_mono':
   "mono e2ennreal"
 by (simp add: e2ennreal_mono mono_def)
 
 lemma enn2ereal_mono [mono_intros]:
   assumes "x \<le> y"
   shows "enn2ereal x \<le> enn2ereal y"
 using assms less_eq_ennreal.rep_eq by auto
 
 lemma ereal_mono:
   "mono ereal"
 unfolding mono_def by auto
 
 lemma ereal_strict_mono:
   "strict_mono ereal"
 unfolding strict_mono_def by auto
 
 lemma ereal_mono2 [mono_intros]:
   assumes "x \<le> y"
   shows "ereal x \<le> ereal y"
 by (simp add: assms)
 
 lemma ereal_strict_mono2 [mono_intros]:
   assumes "x < y"
   shows "ereal x < ereal y"
 using assms by auto
 
 lemma enn2ereal_a_minus_b_plus_b [mono_intros]:
   "enn2ereal a \<le> enn2ereal (a - b) + enn2ereal b"
 by (metis diff_add_self_ennreal less_eq_ennreal.rep_eq linear plus_ennreal.rep_eq)
 
 text \<open>The next lemma follows from the same assertion in ereals.\<close>
 
 lemma enn2ereal_strict_mono [mono_intros]:
   assumes "x < y"
   shows "enn2ereal x < enn2ereal y"
 using assms less_ennreal.rep_eq by auto
 
 declare ennreal_mult_strict_left_mono [mono_intros]
 declare ennreal_mult_strict_right_mono [mono_intros]
 
 lemma ennreal_ge_0 [mono_intros]:
   assumes "0 < x"
   shows "0 < ennreal x"
 by (simp add: assms)
 
 
 text \<open>The next lemma is true and useful in ereal. Note that variants such as $a + b \leq c + d$
 implies $a-d \leq c -b$ are not true -- take $a = c = \infty$ and $b = d = 0$...\<close>
 
 lemma ereal_minus_le_minus_plus [mono_intros]:
   fixes a b c::ereal
   assumes "a \<le> b + c"
   shows "-b \<le> -a + c"
   using assms apply (cases a, cases b, cases c, auto)
   using ereal_infty_less_eq2(2) ereal_plus_1(4) by fastforce
 
 lemma tendsto_ennreal_0 [tendsto_intros]:
   assumes "(u \<longlongrightarrow> 0) F"
   shows "((\<lambda>n. ennreal(u n)) \<longlongrightarrow> 0) F"
 unfolding ennreal_0[symmetric] by (intro tendsto_intros assms)
 
 lemma tendsto_ennreal_1 [tendsto_intros]:
   assumes "(u \<longlongrightarrow> 1) F"
   shows "((\<lambda>n. ennreal(u n)) \<longlongrightarrow> 1) F"
 unfolding ennreal_1[symmetric] by (intro tendsto_intros assms)
 
 subsection \<open>Miscellaneous\<close>
 
-declare lim_1_over_n [tendsto_intros]
-declare lim_ln_over_n [tendsto_intros]
-
-lemma lim_log_over_n [tendsto_intros]:
-  "(\<lambda>n. log k n/n) \<longlonglongrightarrow> 0"
-proof -
-  have *: "log k n/n = (1/ln k) * (ln n / n)" for n
-    unfolding log_def by auto
-  have "(\<lambda>n. (1/ln k) * (ln n / n)) \<longlonglongrightarrow> (1/ln k) * 0"
-    by (intro tendsto_intros)
-  then show ?thesis
-    unfolding * by auto
-qed
-
 lemma lim_ceiling_over_n [tendsto_intros]:
   assumes "(\<lambda>n. u n/n) \<longlonglongrightarrow> l"
   shows "(\<lambda>n. ceiling(u n)/n) \<longlonglongrightarrow> l"
 proof (rule tendsto_sandwich[of "\<lambda>n. u n/n" _ _ "\<lambda>n. u n/n + 1/n"])
   show "\<forall>\<^sub>F n in sequentially. u n / real n \<le> real_of_int \<lceil>u n\<rceil> / real n"
     unfolding eventually_sequentially by (rule exI[of _ 1], auto simp add: divide_simps)
   show "\<forall>\<^sub>F n in sequentially. real_of_int \<lceil>u n\<rceil> / real n \<le> u n / real n + 1 / real n"
     unfolding eventually_sequentially by (rule exI[of _ 1], auto simp add: divide_simps)
   have "(\<lambda>n. u n / real n + 1 / real n) \<longlonglongrightarrow> l + 0"
     by (intro tendsto_intros assms)
   then show "(\<lambda>n. u n / real n + 1 / real n) \<longlonglongrightarrow> l" by auto
 qed (simp add: assms)
 
-lemma power4_eq_xxxx:
-  fixes x::"'a::monoid_mult"
-  shows "x^4 = x * x * x * x"
-by (simp add: mult.assoc power_numeral_even)
-
 subsubsection \<open>Liminfs and Limsups\<close>
 
 text \<open>More facts on liminfs and limsups\<close>
 
 lemma Limsup_obtain':
   fixes u::"'a \<Rightarrow> 'b::complete_linorder"
   assumes "Limsup F u > c" "eventually P F"
   shows "\<exists>n. P n \<and> u n > c"
 proof -
   have *: "(INF P\<in>{P. eventually P F}. SUP x\<in>{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
   have **: "c < (SUP x\<in>{x. P x}. u x)" using less_INF_D[OF *, of P] assms by auto
   then show ?thesis by (simp add: less_SUP_iff)
 qed
 
 lemma limsup_obtain:
   fixes u::"nat \<Rightarrow> 'a :: complete_linorder"
   assumes "limsup u > c"
   shows "\<exists>n \<ge> N. u n > c"
 using Limsup_obtain'[OF assms, of "\<lambda>n. n \<ge> N"] unfolding eventually_sequentially by auto
 
 lemma Liminf_obtain':
   fixes u::"'a \<Rightarrow> 'b::complete_linorder"
   assumes "Liminf F u < c" "eventually P F"
   shows "\<exists>n. P n \<and> u n < c"
 proof -
   have *: "(SUP P\<in>{P. eventually P F}. INF x\<in>{x. P x}. u x) < c" using assms by (simp add: Liminf_def)
   have **: "(INF x\<in>{x. P x}. u x) < c" using SUP_lessD[OF *, of P] assms by auto
   then show ?thesis by (simp add: INF_less_iff)
 qed
 
 lemma liminf_obtain:
   fixes u::"nat \<Rightarrow> 'a :: complete_linorder"
   assumes "liminf u < c"
   shows "\<exists>n \<ge> N. u n < c"
 using Liminf_obtain'[OF assms, of "\<lambda>n. n \<ge> N"] unfolding eventually_sequentially by auto
 
 text \<open>The Liminf of a minimum is the minimum of the Liminfs.\<close>
 
 lemma Liminf_min_eq_min_Liminf:
   fixes u v::"nat \<Rightarrow> 'a::complete_linorder"
   shows "Liminf F (\<lambda>n. min (u n) (v n)) = min (Liminf F u) (Liminf F v)"
 proof (rule order_antisym)
   show "Liminf F (\<lambda>n. min (u n) (v n)) \<le> min (Liminf F u) (Liminf F v)"
     by (auto simp add: Liminf_mono)
 
   have "Liminf F (\<lambda>n. min (u n) (v n)) > w" if H: "min (Liminf F u) (Liminf F v) > w" for w
   proof (cases "{w<..<min (Liminf F u) (Liminf F v)} = {}")
     case True
     have "eventually (\<lambda>n. u n > w) F" "eventually (\<lambda>n. v n > w) F"
       using H le_Liminf_iff by fastforce+
     then have "eventually (\<lambda>n. min (u n) (v n) > w) F"
       apply auto using eventually_elim2 by fastforce
     moreover have "z > w \<Longrightarrow> z \<ge> min (Liminf F u) (Liminf F v)" for z
       using H True not_le_imp_less by fastforce
     ultimately have "eventually (\<lambda>n. min (u n) (v n) \<ge> min (Liminf F u) (Liminf F v)) F"
       by (simp add: eventually_mono)
     then have "min (Liminf F u) (Liminf F v) \<le> Liminf F (\<lambda>n. min (u n) (v n))"
       by (metis Liminf_bounded)
     then show ?thesis using H less_le_trans by blast
   next
     case False
     then obtain z where "z \<in> {w<..<min (Liminf F u) (Liminf F v)}"
       by blast
     then have H: "w < z" "z < min (Liminf F u) (Liminf F v)"
       by auto
     then have "eventually (\<lambda>n. u n > z) F" "eventually (\<lambda>n. v n > z) F"
       using le_Liminf_iff by fastforce+
     then have "eventually (\<lambda>n. min (u n) (v n) > z) F"
       apply auto using eventually_elim2 by fastforce
     then have "Liminf F (\<lambda>n. min (u n) (v n)) \<ge> z"
       by (simp add: Liminf_bounded eventually_mono less_imp_le)
     then show ?thesis using H(1)
       by auto
   qed
   then show "min (Liminf F u) (Liminf F v) \<le> Liminf F (\<lambda>n. min (u n) (v n))"
     using not_le_imp_less by blast
 qed
 
 text \<open>The Limsup of a maximum is the maximum of the Limsups.\<close>
 
 lemma Limsup_max_eq_max_Limsup:
   fixes u::"'a \<Rightarrow> 'b::complete_linorder"
   shows "Limsup F (\<lambda>n. max (u n) (v n)) = max (Limsup F u) (Limsup F v)"
 proof (rule order_antisym)
   show "max (Limsup F u) (Limsup F v) \<le> Limsup F (\<lambda>n. max (u n) (v n))"
     by (auto intro: Limsup_mono)
 
   have "Limsup F (\<lambda>n. max (u n) (v n)) < e" if "max (Limsup F u) (Limsup F v) < e" for e
   proof (cases "\<exists>t. max (Limsup F u) (Limsup F v) < t \<and> t < e")
     case True
     then obtain t where t: "t < e" "max (Limsup F u) (Limsup F v) < t" by auto
     then have "Limsup F u < t" "Limsup F v < t" using that max_def by auto
     then have *: "eventually (\<lambda>n. u n < t) F" "eventually (\<lambda>n. v n < t) F"
       by (auto simp: Limsup_lessD)
     have "eventually (\<lambda>n. max (u n) (v n) < t) F"
       using eventually_mono[OF eventually_conj[OF *]] by auto
     then have "Limsup F (\<lambda>n. max (u n) (v n)) \<le> t"
       by (meson Limsup_obtain' not_le_imp_less order.asym)
     then show ?thesis
       using t by auto
   next
     case False
     have "Limsup F u < e" "Limsup F v < e" using that max_def by auto
     then have *: "eventually (\<lambda>n. u n < e) F" "eventually (\<lambda>n. v n < e) F"
       by (auto simp: Limsup_lessD)
     have "eventually (\<lambda>n. max (u n) (v n) \<le> max (Limsup F u) (Limsup F v)) F"
       apply (rule eventually_mono[OF eventually_conj[OF *]]) using False not_le_imp_less by force
     then have "Limsup F (\<lambda>n. max (u n) (v n)) \<le> max (Limsup F u) (Limsup F v)"
       by (meson Limsup_obtain' leD leI)
     then show ?thesis using that le_less_trans by blast
   qed
   then show "Limsup F (\<lambda>n. max (u n) (v n)) \<le> max (Limsup F u) (Limsup F v)"
     using not_le_imp_less by blast
 qed
 
 subsubsection \<open>Bounding the cardinality of a finite set\<close>
 
 text \<open>A variation with real bounds.\<close>
 
 lemma finite_finite_subset_caract':
   fixes C::real
   assumes "\<And>G. G \<subseteq> F \<Longrightarrow> finite G \<Longrightarrow> card G \<le> C"
   shows "finite F \<and> card F \<le> C"
 by (meson assms finite_if_finite_subsets_card_bdd le_nat_floor order_refl)
 
 text \<open>To show that a set has cardinality at most one, it suffices to show that any two of its
 elements coincide.\<close>
 
 lemma finite_at_most_singleton:
   assumes "\<And>x y. x \<in> F \<Longrightarrow> y \<in> F \<Longrightarrow> x = y"
   shows "finite F \<and> card F \<le> 1"
 proof (cases "F = {}")
   case True
   then show ?thesis by auto
 next
   case False
   then obtain x where "x \<in> F" by auto
   then have "F = {x}" using assms by auto
   then show ?thesis by auto
 qed
 
 text \<open>Bounded sets of integers are finite.\<close>
 
 lemma finite_real_int_interval [simp]:
   "finite (range real_of_int \<inter> {a..b})"
 proof -
   have "range real_of_int \<inter> {a..b} \<subseteq> real_of_int`{floor a..ceiling b}"
     by (auto, metis atLeastAtMost_iff ceiling_mono ceiling_of_int floor_mono floor_of_int image_eqI)
   then show ?thesis using finite_subset by blast
 qed
 
 text \<open>Well separated sets of real numbers are finite, with controlled cardinality.\<close>
 
 lemma separated_in_real_card_bound:
   assumes "T \<subseteq> {a..(b::real)}" "d > 0" "\<And>x y. x \<in> T \<Longrightarrow> y \<in> T \<Longrightarrow> y > x \<Longrightarrow> y \<ge> x + d"
   shows "finite T" "card T \<le> nat (floor ((b-a)/d) + 1)"
 proof -
   define f where "f = (\<lambda>x. floor ((x-a) / d))"
   have "f`{a..b} \<subseteq> {0..floor ((b-a)/d)}"
     unfolding f_def using \<open>d > 0\<close> by (auto simp add: floor_mono frac_le)
   then have *: "f`T \<subseteq> {0..floor ((b-a)/d)}" using \<open>T \<subseteq> {a..b}\<close> by auto
   then have "finite (f`T)" by (rule finite_subset, auto)
   have "card (f`T) \<le> card {0..floor ((b-a)/d)}" apply (rule card_mono) using * by auto
   then have card_le: "card (f`T) \<le> nat (floor ((b-a)/d) + 1)" using card_atLeastAtMost_int by auto
 
   have *: "f x \<noteq> f y" if "y \<ge> x + d" for x y
   proof -
     have "(y-a)/d \<ge> (x-a)/d + 1" using \<open>d > 0\<close> that by (auto simp add: divide_simps)
     then show ?thesis unfolding f_def by linarith
   qed
   have "inj_on f T"
     unfolding inj_on_def using * assms(3) by (auto, metis not_less_iff_gr_or_eq)
   show "finite T"
     using \<open>finite (f`T)\<close> \<open>inj_on f T\<close> finite_image_iff by blast
   have "card T = card (f`T)"
     using \<open>inj_on f T\<close> by (simp add: card_image)
   then show "card T \<le> nat (floor ((b-a)/d) + 1)"
     using card_le by auto
 qed
 
 
 subsection \<open>Manipulating finite ordered sets\<close>
 
-text \<open>We will need below to contruct finite sets of real numbers with good properties expressed
+text \<open>We will need below to construct finite sets of real numbers with good properties expressed
 in terms of consecutive elements of the set. We introduce tools to manipulate such sets,
 expressing in particular the next and the previous element of the set and controlling how they
 evolve when one inserts a new element in the set. It works in fact in any linorder, and could
 also prove useful to construct sets of integer numbers.
 
 Manipulating the next and previous elements work well, except at the top (respectively bottom).
 In our constructions, these will be fixed and called $b$ and $a$.\<close>
 
 text \<open>Notations for the next and the previous elements.\<close>
 
 definition next_in::"'a set \<Rightarrow> 'a \<Rightarrow> ('a::linorder)"
   where "next_in A u = Min (A \<inter> {u<..})"
 
 definition prev_in::"'a set \<Rightarrow> 'a \<Rightarrow> ('a::linorder)"
   where "prev_in A u = Max (A \<inter> {..<u})"
 
 context
   fixes A::"('a::linorder) set" and a b::'a
   assumes A: "finite A" "A \<subseteq> {a..b}" "a \<in> A" "b \<in> A" "a < b"
 begin
 
 text \<open>Basic properties of the next element, when one starts from an element different from top.\<close>
 
 lemma next_in_basics:
   assumes "u \<in> {a..<b}"
   shows "next_in A u \<in> A"
         "next_in A u > u"
         "A \<inter> {u<..<next_in A u} = {}"
 proof -
   have next_in_A: "next_in A u \<in> A \<inter> {u<..}"
     unfolding next_in_def apply (rule Min_in)
     using assms \<open>finite A\<close> \<open>b \<in> A\<close> by auto
   then show "next_in A u \<in> A" "next_in A u > u" by auto
   show "A \<inter> {u<..<next_in A u} = {}"
     unfolding next_in_def using A by (auto simp add: leD)
 qed
 
 lemma next_inI:
   assumes "u \<in> {a..<b}"
           "v \<in> A"
           "v > u"
           "{u<..<v} \<inter> A = {}"
   shows "next_in A u = v"
 using assms next_in_basics[OF \<open>u \<in> {a..<b}\<close>] by fastforce
 
 text \<open>Basic properties of the previous element, when one starts from an element different from
 bottom.\<close>
 
 lemma prev_in_basics:
   assumes "u \<in> {a<..b}"
   shows "prev_in A u \<in> A"
         "prev_in A u < u"
         "A \<inter> {prev_in A u<..<u} = {}"
 proof -
   have prev_in_A: "prev_in A u \<in> A \<inter> {..<u}"
     unfolding prev_in_def apply (rule Max_in)
     using assms \<open>finite A\<close> \<open>a \<in> A\<close> by auto
   then show "prev_in A u \<in> A" "prev_in A u < u" by auto
   show "A \<inter> {prev_in A u<..<u} = {}"
     unfolding prev_in_def using A by (auto simp add: leD)
 qed
 
 lemma prev_inI:
   assumes "u \<in> {a<..b}"
           "v \<in> A"
           "v < u"
           "{v<..<u} \<inter> A = {}"
   shows "prev_in A u = v"
 using assms prev_in_basics[OF \<open>u \<in> {a<..b}\<close>]
 by (meson disjoint_iff_not_equal greaterThanLessThan_iff less_linear)
 
 text \<open>The interval $[a,b]$ is covered by the intervals between the consecutive elements of $A$.\<close>
 
 lemma intervals_decomposition:
   "(\<Union> U \<in> {{u..next_in A u} | u. u \<in> A - {b}}. U) = {a..b}"
 proof
   show "(\<Union>U\<in>{{u..next_in A u} |u. u \<in> A - {b}}. U) \<subseteq> {a..b}"
     using \<open>A \<subseteq> {a..b}\<close> next_in_basics(1) apply auto apply fastforce
     by (metis \<open>A \<subseteq> {a..b}\<close> atLeastAtMost_iff eq_iff le_less_trans less_eq_real_def not_less subset_eq subset_iff_psubset_eq)
 
   have "x \<in> (\<Union>U\<in>{{u..next_in A u} |u. u \<in> A - {b}}. U)" if "x \<in> {a..b}" for x
   proof -
     consider "x = b" | "x \<in> A - {b}" | "x \<notin> A" by blast
     then show ?thesis
     proof(cases)
       case 1
       define u where "u = prev_in A b"
       have "b \<in> {a<..b}" using \<open>a < b\<close> by simp
       have "u \<in> A - {b}" unfolding u_def using prev_in_basics[OF \<open>b \<in> {a<..b}\<close>] by simp
       then have "u \<in> {a..<b}" using \<open>A \<subseteq> {a..b}\<close> \<open>a < b\<close> by fastforce
       have "next_in A u = b"
         using prev_in_basics[OF \<open>b \<in> {a<..b}\<close>] next_in_basics[OF \<open>u \<in> {a..<b}\<close>] \<open>A \<subseteq> {a..b}\<close> unfolding u_def by force
       then have "x \<in> {u..next_in A u}" unfolding 1 using prev_in_basics[OF \<open>b \<in> {a<..b}\<close>] u_def by auto
       then show ?thesis using \<open>u \<in> A - {b}\<close> by auto
     next
       case 2
       then have "x \<in> {a..<b}" using \<open>A \<subseteq> {a..b}\<close> \<open>a < b\<close> by fastforce
       have "x \<in> {x.. next_in A x}" using next_in_basics[OF \<open>x \<in> {a..<b}\<close>] by auto
       then show ?thesis using 2 by auto
     next
       case 3
       then have "x \<in> {a<..b}" using that \<open>a \<in> A\<close> leI by fastforce
       define u where "u = prev_in A x"
       have "u \<in> A - {b}" unfolding u_def using prev_in_basics[OF \<open>x \<in> {a<..b}\<close>] that by auto
       then have "u \<in> {a..<b}" using \<open>A \<subseteq> {a..b}\<close> \<open>a < b\<close> by fastforce
       have "x \<in> {u..next_in A u}"
         using prev_in_basics[OF \<open>x \<in> {a<..b}\<close>] next_in_basics[OF \<open>u \<in> {a..<b}\<close>] unfolding u_def by auto
       then show ?thesis using \<open>u \<in> A - {b}\<close> by auto
     qed
   qed
   then show "{a..b} \<subseteq> (\<Union>U\<in>{{u..next_in A u} |u. u \<in> A - {b}}. U)" by auto
 qed
 end
 
 text \<open>If one inserts an additional element, then next and previous elements are not modified,
 except at the location of the insertion.\<close>
 
 lemma next_in_insert:
   assumes A: "finite A" "A \<subseteq> {a..b}" "a \<in> A" "b \<in> A" "a < b"
       and "x \<in> {a..b} - A"
   shows "\<And>u. u \<in> A - {b, prev_in A x} \<Longrightarrow> next_in (insert x A) u = next_in A u"
         "next_in (insert x A) x = next_in A x"
         "next_in (insert x A) (prev_in A x) = x"
 proof -
   define B where "B = insert x A"
   have B: "finite B" "B \<subseteq> {a..b}" "a \<in> B" "b \<in> B" "a < b"
     using assms unfolding B_def by auto
   have x: "x \<in> {a..<b}" "x \<in> {a<..b}" using assms leI by fastforce+
   show "next_in B x = next_in A x"
     unfolding B_def by (auto simp add: next_in_def)
 
   show "next_in B (prev_in A x) = x"
     apply (rule next_inI[OF B])
     unfolding B_def using prev_in_basics[OF A \<open>x \<in> {a<..b}\<close>] \<open>A \<subseteq> {a..b}\<close> x by auto
 
   fix u assume "u \<in> A - {b, prev_in A x}"
   then have "u \<in> {a..<b}" using assms by fastforce
   have "x \<notin> {u<..<next_in A u}"
   proof (rule ccontr)
     assume "\<not>(x \<notin> {u<..<next_in A u})"
     then have *: "x \<in> {u<..<next_in A u}" by auto
     have "prev_in A x = u"
       apply (rule prev_inI[OF A \<open>x \<in> {a<..b}\<close>])
       using \<open>u \<in> A - {b, prev_in A x}\<close> * next_in_basics[OF A \<open>u \<in> {a..<b}\<close>] apply auto
       by (meson disjoint_iff_not_equal greaterThanLessThan_iff less_trans)
     then show False using \<open>u \<in> A - {b, prev_in A x}\<close> by auto
   qed
   show "next_in B u = next_in A u"
     apply (rule next_inI[OF B \<open>u \<in> {a..<b}\<close>]) unfolding B_def
     using next_in_basics[OF A \<open>u \<in> {a..<b}\<close>] \<open>x \<notin> {u<..<next_in A u}\<close> by auto
 qed
 
 text \<open>If consecutive elements are enough separated, this implies a simple bound on the
 cardinality of the set.\<close>
 
 lemma separated_in_real_card_bound2:
   fixes A::"real set"
   assumes A: "finite A" "A \<subseteq> {a..b}" "a \<in> A" "b \<in> A" "a < b"
       and B: "\<And>u. u \<in> A - {b} \<Longrightarrow> next_in A u \<ge> u + d" "d > 0"
   shows "card A \<le> nat (floor ((b-a)/d) + 1)"
 proof (rule separated_in_real_card_bound[OF \<open>A \<subseteq> {a..b}\<close> \<open>d > 0\<close>])
   fix x y assume "x \<in> A" "y \<in> A" "y > x"
   then have "x \<in> A - {b}" "x \<in> {a..<b}" using \<open>A \<subseteq> {a..b}\<close> by auto
   have "y \<ge> next_in A x"
     using next_in_basics[OF A \<open>x \<in> {a..<b}\<close>] \<open>y \<in> A\<close> \<open>y > x\<close> by auto
   then show "y \<ge> x + d" using B(1)[OF \<open>x \<in> A - {b}\<close>] by auto
 qed
 
 
 subsection \<open>Well-orders\<close>
 
 text \<open>In this subsection, we give additional lemmas on well-orders or cardinals or whatever,
 that would well belong to the library, and will be needed below.\<close>
 
 lemma (in wo_rel) max2_underS [simp]:
   assumes "x \<in> underS z" "y \<in> underS z"
   shows "max2 x y \<in> underS z"
 using assms max2_def by auto
 
 lemma (in wo_rel) max2_underS' [simp]:
   assumes "x \<in> underS y"
   shows "max2 x y = y" "max2 y x = y"
 apply (simp add: underS_E assms max2_def)
 using assms max2_def ANTISYM antisym_def underS_E by fastforce
 
 lemma (in wo_rel) max2_xx [simp]:
   "max2 x x = x"
 using max2_def by auto
 
 declare underS_notIn [simp]
 
 text \<open>The abbrevation $=o$ is used both in \verb+Set_Algebras+ and Cardinals.
 We disable the one from \verb+Set_Algebras+.\<close>
 
 no_notation elt_set_eq (infix "=o" 50)
 
 lemma regularCard_ordIso:
   assumes "Card_order r" "regularCard r" "s =o r"
   shows "regularCard s"
 unfolding regularCard_def
 proof (auto)
   fix K assume K: "K \<subseteq> Field s" "cofinal K s"
   obtain f where f: "bij_betw f (Field s) (Field r)" "embed s r f" using \<open>s =o r\<close> unfolding ordIso_def iso_def by auto
   have "f`K \<subseteq> Field r" using K(1) f(1) bij_betw_imp_surj_on by blast
   have "cofinal (f`K) r" unfolding cofinal_def
   proof
     fix a assume "a \<in> Field r"
     then obtain a' where a: "a' \<in> Field s" "f a' = a" using f
       by (metis bij_betw_imp_surj_on imageE)
     then obtain b' where b: "b' \<in> K" "a' \<noteq> b' \<and> (a', b') \<in> s"
       using \<open>cofinal K s\<close> unfolding cofinal_def by auto
     have P1: "f b' \<in> f`K" using b(1) by auto
     have "a' \<noteq> b'" "a' \<in> Field s" "b' \<in> Field s" using a(1) b K(1) by auto
     then have P2: "a \<noteq> f b'" unfolding a(2)[symmetric] using f(1) unfolding bij_betw_def inj_on_def by auto
     have "(a', b') \<in> s" using b by auto
     then have P3: "(a, f b') \<in> r" unfolding a(2)[symmetric] using f
       by (meson FieldI1 FieldI2 Card_order_ordIso[OF assms(1) assms(3)] card_order_on_def iso_defs(1) iso_iff2)
     show "\<exists>b\<in>f ` K. a \<noteq> b \<and> (a, b) \<in> r"
       using P1 P2 P3 by blast
   qed
   then have "|f`K| =o r"
     using \<open>regularCard r\<close> \<open>f`K \<subseteq> Field r\<close> unfolding regularCard_def by auto
   moreover have "|f`K| =o |K|" using f(1) K(1)
     by (meson bij_betw_subset card_of_ordIsoI ordIso_symmetric)
   ultimately show "|K| =o s"
     using \<open>s =o r\<close> by (meson ordIso_symmetric ordIso_transitive)
 qed
 
 lemma AboveS_not_empty_in_regularCard:
   assumes "|S| <o r" "S \<subseteq> Field r"
   assumes r: "Card_order r" "regularCard r" "\<not>finite (Field r)"
   shows "AboveS r S \<noteq> {}"
 proof -
   have "\<not>(cofinal S r)"
     using assms not_ordLess_ordIso unfolding regularCard_def by auto
   then obtain a where a: "a \<in> Field r" "\<forall>b\<in>S. \<not>(a \<noteq> b \<and> (a,b) \<in> r)"
     unfolding cofinal_def by auto
   have *: "a = b \<or> (b, a) \<in> r" if "b \<in> S" for b
   proof -
     have "a = b \<or> (a,b) \<notin> r" using a that by auto
     then show ?thesis
       using \<open>Card_order r\<close> \<open>a \<in> Field r\<close> \<open>b \<in> S\<close> \<open>S \<subseteq> Field r\<close> unfolding card_order_on_def well_order_on_def linear_order_on_def total_on_def
       by auto
   qed
   obtain c where "c \<in> Field r" "c \<noteq> a" "(a, c) \<in> r"
     using a(1) r infinite_Card_order_limit by fastforce
   then have "c \<in> AboveS r S"
     unfolding AboveS_def apply simp using Card_order_trans[OF r(1)] by (metis *)
   then show ?thesis by auto
 qed
 
 lemma AboveS_not_empty_in_regularCard':
   assumes "|S| <o r" "f`S \<subseteq> Field r" "T \<subseteq> S"
   assumes r: "Card_order r" "regularCard r" "\<not>finite (Field r)"
   shows "AboveS r (f`T) \<noteq> {}"
 proof -
   have "|f`T| \<le>o |T|" by simp
   moreover have "|T| \<le>o |S|" using \<open>T \<subseteq> S\<close> by simp
   ultimately have *: "|f`T| <o r" using \<open>|S| <o r\<close> by (meson ordLeq_ordLess_trans)
   show ?thesis using AboveS_not_empty_in_regularCard[OF * _ r] \<open>T \<subseteq> S\<close> \<open>f`S \<subseteq> Field r\<close> by auto
 qed
 
 lemma Well_order_extend:
 assumes WELL: "well_order_on A r" and SUB: "A \<subseteq> B"
 shows "\<exists>r'. well_order_on B r' \<and> r \<subseteq> r'"
 proof-
   have r: "Well_order r \<and> Field r = A" using WELL well_order_on_Well_order by blast
   let ?C = "B - A"
   obtain r'' where "well_order_on ?C r''" using well_order_on by blast
   then have r'': "Well_order r'' \<and> Field r'' = ?C"
     using well_order_on_Well_order by blast
   let ?r' = "r Osum r''"
   have "Field r Int Field r'' = {}" using r r'' by auto
   then have "r \<le>o ?r'" using Osum_ordLeq[of r r''] r r'' by blast
   then have "Well_order ?r'" unfolding ordLeq_def by auto
   moreover have "Field ?r' = B" using r r'' SUB by (auto simp add: Field_Osum)
   ultimately have "well_order_on B ?r'" by auto
   moreover have "r \<subseteq> ?r'" by (simp add: Osum_def subrelI)
   ultimately show ?thesis by blast
 qed
 
 text \<open>The next lemma shows that, if the range of a function is endowed with a wellorder,
 then one can pull back this wellorder by the function, and then extend it in the fibers
 of the function in order to keep the wellorder property.
 
 The proof is done by taking an arbitrary family of wellorders on each of the fibers, and using
 the lexicographic order: one has $x < y$ if $f x < f y$, or if $f x = f y$ and, in the corresponding
 fiber of $f$, one has $x < y$.
 
 To formalize it, it is however more efficient to use one single wellorder, and restrict it
 to each fiber.\<close>
 
 lemma Well_order_pullback:
   assumes "Well_order r"
   shows "\<exists>s. Well_order s \<and> Field s = UNIV \<and> (\<forall>x y. (f x, f y) \<in> (r-Id) \<longrightarrow> (x, y) \<in> s)"
 proof -
   obtain r2 where r2: "Well_order r2" "Field r2 = UNIV" "r \<subseteq> r2"
     using Well_order_extend[OF assms, of UNIV] well_order_on_Well_order by auto
   obtain s2 where s2: "Well_order s2" "Field s2 = (UNIV::'b set)"
     by (meson well_ordering)
 
   have r2s2:
     "\<And>x y z. (x, y) \<in> s2 \<Longrightarrow> (y, z) \<in> s2 \<Longrightarrow> (x, z) \<in> s2"
     "\<And>x. (x, x) \<in> s2"
     "\<And>x y. (x, y) \<in> s2 \<or> (y, x) \<in> s2"
     "\<And>x y. (x, y) \<in> s2 \<Longrightarrow> (y, x) \<in> s2 \<Longrightarrow> x = y"
     "\<And>x y z. (x, y) \<in> r2 \<Longrightarrow> (y, z) \<in> r2 \<Longrightarrow> (x, z) \<in> r2"
     "\<And>x. (x, x) \<in> r2"
     "\<And>x y. (x, y) \<in> r2 \<or> (y, x) \<in> r2"
     "\<And>x y. (x, y) \<in> r2 \<Longrightarrow> (y, x) \<in> r2 \<Longrightarrow> x = y"
     using r2 s2 unfolding well_order_on_def linear_order_on_def partial_order_on_def total_on_def preorder_on_def antisym_def refl_on_def trans_def
     by (metis UNIV_I)+
 
   define s where "s = {(x,y). (f x, f y) \<in> r2 \<and> (f x = f y \<longrightarrow> (x, y) \<in> s2)}"
   have "linear_order s"
   unfolding linear_order_on_def partial_order_on_def preorder_on_def
   proof (auto)
     show "total_on UNIV s"
       unfolding s_def apply (rule total_onI, auto) using r2s2 by metis+
     show "refl_on UNIV s"
       unfolding s_def apply (rule refl_onI, auto) using r2s2 by blast+
     show "trans s"
       unfolding s_def apply (rule transI, auto) using r2s2 by metis+
     show "antisym s"
       unfolding s_def apply (rule antisymI, auto) using r2s2 by metis+
   qed
   moreover have "wf (s - Id)"
   proof (rule wfI_min)
     fix x::'b and Q assume "x \<in> Q"
     obtain z' where z': "z' \<in> f`Q" "\<And>y. (y, z') \<in> r2 - Id \<longrightarrow> y \<notin> f`Q"
     proof (rule wfE_min[of "r2-Id" "f x" "f`Q"], auto)
       show "wf(r2-Id)" using \<open>Well_order r2\<close> unfolding well_order_on_def by auto
       show "f x \<in> f`Q" using \<open>x \<in> Q\<close> by auto
     qed
     define Q2 where "Q2 = Q \<inter> f-`{z'}"
     obtain z where z: "z \<in> Q2" "\<And>y. (y, z) \<in> s2 - Id \<longrightarrow> y \<notin> Q2"
     proof (rule wfE_min'[of "s2-Id" "Q2"], auto)
       show "wf(s2-Id)" using \<open>Well_order s2\<close> unfolding well_order_on_def by auto
       assume "Q2 = {}"
       then show False unfolding Q2_def using \<open>z' \<in> f`Q\<close> by blast
     qed
     have "(y, z) \<in> (s-Id) \<Longrightarrow> y \<notin> Q" for y
       unfolding s_def using z' z Q2_def by auto
     then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> s - Id \<longrightarrow> y \<notin> Q"
       using \<open>z \<in> Q2\<close> Q2_def by auto
   qed
   ultimately have "well_order_on UNIV s" unfolding well_order_on_def by simp
   moreover have "(f x, f y) \<in> (r-Id) \<longrightarrow> (x, y) \<in> s" for x y
     unfolding s_def using \<open>r \<subseteq> r2\<close> by auto
   ultimately show ?thesis using well_order_on_Well_order by metis
 qed
 
 end (*of theory Library_Complements*)
diff --git a/thys/Smooth_Manifolds/Analysis_More.thy b/thys/Smooth_Manifolds/Analysis_More.thy
--- a/thys/Smooth_Manifolds/Analysis_More.thy
+++ b/thys/Smooth_Manifolds/Analysis_More.thy
@@ -1,1464 +1,1394 @@
 section \<open>Library Additions\<close>
 theory Analysis_More
   imports "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
     "HOL-Library.Function_Algebras"
     "HOL-Types_To_Sets.Linear_Algebra_On"
 begin
 
 
 lemma openin_open_Int'[intro]:
   "open S \<Longrightarrow> openin (top_of_set U) (S \<inter> U)"
   by (auto simp: openin_open)
 
 subsection \<open>Parametricity rules for topology\<close>
 
 text \<open>TODO: also check with theory \<open>Transfer_Euclidean_Space_Vector\<close> in AFP/ODE...\<close>
 
 context includes lifting_syntax begin
 
 lemma Sigma_transfer[transfer_rule]:
   "(rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B)) Sigma Sigma"
   unfolding Sigma_def
   by transfer_prover
 
 lemma filterlim_transfer[transfer_rule]:
   "((A ===> B) ===> rel_filter B ===> rel_filter A ===> (=)) filterlim filterlim"
   if [transfer_rule]: "bi_unique B"
   unfolding filterlim_iff
   by transfer_prover
 
 lemma nhds_transfer[transfer_rule]:
   "(A ===> rel_filter A) nhds nhds"
   if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
   unfolding nhds_def
   by transfer_prover
 
 lemma at_within_transfer[transfer_rule]:
   "(A ===> rel_set A ===> rel_filter A) at_within at_within"
   if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
   unfolding at_within_def
   by transfer_prover
 
 lemma continuous_on_transfer[transfer_rule]:
   "(rel_set A ===> (A ===> B) ===> (=)) continuous_on continuous_on"
   if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
     "bi_unique B" "bi_total B" "(rel_set B ===> (=)) open open"
   unfolding continuous_on_def
   by transfer_prover
 
 lemma continuous_on_transfer_right_total[transfer_rule]:
   "(rel_set A ===> (A ===> B) ===> (=)) (\<lambda>X::'a::t2_space set. continuous_on (X \<inter> Collect AP)) (\<lambda>Y::'b::t2_space set. continuous_on Y)"
   if DomainA: "Domainp A = AP"
     and [folded DomainA, transfer_rule]: "bi_unique A" "right_total A" "(rel_set A ===> (=)) (openin (top_of_set (Collect AP))) open"
     "bi_unique B" "bi_total B" "(rel_set B ===> (=)) open open"
   unfolding DomainA[symmetric]
 proof (intro rel_funI)
   fix X Y f g
   assume H[transfer_rule]: "rel_set A X Y" "(A ===> B) f g"
   from H(1) have XA: "x \<in> X \<Longrightarrow> Domainp A x" for x
     by (auto simp: rel_set_def)
   then have *: "X \<inter> Collect (Domainp A) = X" by auto
   have "openin (top_of_set (Collect (Domainp A))) (Collect (Domainp A))" by auto
   show " continuous_on (X \<inter> Collect (Domainp A)) f = continuous_on Y g"
     unfolding continuous_on_eq_continuous_within continuous_within_topological *
     apply transfer
     apply safe
     subgoal for x B
       apply (drule bspec, assumption, drule spec, drule mp, assumption, drule mp, assumption)
       apply clarsimp
       subgoal for AA
         apply (rule exI[where x="AA \<inter> Collect (Domainp A)"])
         by (auto intro: XA)
       done
     subgoal using XA by (force simp: openin_subtopology)
     done
 qed
 
 lemma continuous_on_transfer_right_total2[transfer_rule]:
   "(rel_set A ===> (A ===> B) ===> (=)) (\<lambda>X::'a::t2_space set. continuous_on X) (\<lambda>Y::'b::t2_space set. continuous_on Y)"
   if DomainB: "Domainp B = BP"
   and [folded DomainB, transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
     "bi_unique B" "right_total B" "(rel_set B ===> (=)) ((openin (top_of_set (Collect BP)))) open"
   unfolding DomainB[symmetric]
 proof (intro rel_funI)
   fix X Y f g
   assume H[transfer_rule]: "rel_set A X Y" "(A ===> B) f g"
   show "continuous_on X f = continuous_on Y g"
     unfolding continuous_on_eq_continuous_within continuous_within_topological
     apply transfer
     apply safe
     subgoal for x C
       apply (clarsimp simp: openin_subtopology)
       apply (drule bspec, assumption, drule spec, drule mp, assumption, drule mp, assumption)
       apply clarsimp
       by (meson Domainp_applyI H(1) H(2) rel_setD1)
     subgoal for x C
     proof -
       let ?sub = "top_of_set (Collect (Domainp B))"
       assume cont: "\<forall>x\<in>X. \<forall>Ba\<in>{A. Ball A (Domainp B)}.
           openin (top_of_set (Collect (Domainp B))) Ba \<longrightarrow> f x \<in> Ba \<longrightarrow> (\<exists>Aa.  open Aa \<and> x \<in> Aa \<and> (\<forall>y\<in>X. y \<in> Aa \<longrightarrow> f y \<in> Ba))"
         and x: "x \<in> X" "open C" "f x \<in> C"
       let ?B = "C \<inter> Collect (Domainp B)"
       have "?B \<in> {A. Ball A (Domainp B)}" by auto
       have "openin ?sub (Collect (Domainp B))" by auto
       then have "openin ?sub ?B" using \<open>open C\<close> by auto
       moreover have "f x \<in> ?B" using x
         apply transfer apply auto
         by (meson Domainp_applyI H(1) H(2) rel_setD1)
       ultimately obtain D where "open D \<and> x \<in> D \<and> (\<forall>y\<in>X. y \<in> D \<longrightarrow> f y \<in> ?B)"
         using cont x
         by blast
       then show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>X. y \<in> A \<longrightarrow> f y \<in> C)" by auto
     qed
     done
 qed
 
 
 lemma generate_topology_transfer[transfer_rule]:
   includes lifting_syntax
   assumes [transfer_rule]: "right_total A" "bi_unique A"
   shows "(rel_set (rel_set A) ===> rel_set A ===> (=)) (generate_topology o (insert (Collect (Domainp A)))) generate_topology"
 proof (intro rel_funI)
   fix B C X Y assume t[transfer_rule]: "rel_set (rel_set A) B C" "rel_set A X Y"
   then have "X \<subseteq> Collect (Domainp A)" by (auto simp: rel_set_def)
   with t have rI: "rel_set A (X \<inter> Collect (Domainp A)) Y"
     by (auto simp: inf_absorb1)
   have eq_UNIV_I: "Z = UNIV" if [transfer_rule]: "rel_set A {a. Domainp A a} Z" for Z
     using that assms
     apply (auto simp: right_total_def rel_set_def)
     using bi_uniqueDr by fastforce
   show "(generate_topology \<circ> insert (Collect (Domainp A))) B X = generate_topology C Y"
     unfolding o_def
   proof (rule iffI)
     fix x
     assume "generate_topology (insert (Collect (Domainp A)) B) X"
     then show "generate_topology C Y" unfolding o_def
       using rI
     proof (induction X arbitrary: Y)
       case [transfer_rule]: UNIV
       with eq_UNIV_I[of Y] show ?case
         by (simp add: generate_topology.UNIV)
     next
       case (Int a b)
       note [transfer_rule] = Int(5)
       obtain a' where a'[transfer_rule]: "rel_set A (a \<inter> Collect (Domainp A)) a'"
         by (metis Domainp_iff Domainp_set Int_Collect)
       obtain b' where b'[transfer_rule]: "rel_set A (b \<inter> Collect (Domainp A)) b'"
         by (metis Domainp_iff Domainp_set Int_Collect)
       from Int.IH(1)[OF a'] Int.IH(2)[OF b']
       have "generate_topology C a'" "generate_topology C b'" by auto
       from generate_topology.Int[OF this] have "generate_topology C (a' \<inter> b')" .
       also have "a' \<inter> b' = Y"
         by transfer auto
       finally show ?case
         by (simp add: generate_topology.Int)
     next
       case (UN K)
       note [transfer_rule] = UN(3)
       have "\<exists>K'. \<forall>k. rel_set A (k \<inter> Collect (Domainp A)) (K' k)"
         by (rule choice) (metis Domainp_iff Domainp_set Int_Collect)
       then obtain K' where K': "\<And>k. rel_set A (k \<inter> Collect (Domainp A)) (K' k)" by metis
       from UN.IH[OF _ this] have "generate_topology C k'" if "k' \<in> K'`K" for k' using that by auto
       from generate_topology.UN[OF this] have "generate_topology C (\<Union>(K' ` K))" .
       also
       from K' have [transfer_rule]: "(rel_set (=) ===> rel_set A) (\<lambda>x. x \<inter> Collect (Domainp A)) K'"
         by (fastforce simp: rel_fun_def rel_set_def)
       have "\<Union>(K' ` K) = Y"
         by transfer auto
       finally show ?case
         by (simp add: generate_topology.UN)
     next
       case (Basis s)
       from this(1) show ?case
       proof
         assume "s = Collect (Domainp A)" 
         with eq_UNIV_I[of Y] Basis(2)
         show ?case
           by (simp add: generate_topology.UNIV)
       next
         assume "s \<in> B"
         with Basis(2) obtain t where [transfer_rule]: "rel_set A (s \<inter> Collect (Domainp A)) t" by auto
         from Basis(1) t(1) have s: "s \<inter> Collect (Domainp A) = s"
           by (force simp: rel_set_def)
         have "t \<in> C" using \<open>s \<in> B\<close> s
           by transfer auto
         also note [transfer_rule] = Basis(2)
         have "t = Y"
           by transfer auto
         finally show ?case
           by (rule generate_topology.Basis)
       qed
     qed
   next
     assume "generate_topology C Y"
     then show "generate_topology (insert (Collect (Domainp A)) B) X"
       using \<open>rel_set A X Y\<close>
     proof (induction arbitrary: X)
       case [transfer_rule]: UNIV
       have "UNIV = (UNIV::'b set)" by auto
       then have "X = {a. Domainp A a}" by transfer
       then show ?case by (intro generate_topology.Basis) auto
     next
       case (Int a b)
       obtain a' b' where [transfer_rule]: "rel_set A a' a" "rel_set A b' b"
         by (meson assms(1) right_total_def right_total_rel_set)
       from generate_topology.Int[OF Int.IH(1)[OF this(1)] Int.IH(2)[OF this(2)]]
       have "generate_topology (insert {a. Domainp A a} B) (a' \<inter> b')" by simp
       also
       define I where "I = a \<inter> b"
       from \<open>rel_set A X (a \<inter> b)\<close> have [transfer_rule]: "rel_set A X I" by (simp add: I_def)
       from I_def
       have "a' \<inter> b' = X" by transfer simp
       finally show ?case .
     next
       case (UN K)
       have "\<exists>K'. \<forall>k. rel_set A (K' k) k"
         by (rule choice) (meson assms(1) right_total_def right_total_rel_set)
       then obtain K' where K': "\<And>k. rel_set A (K' k) k" by metis
       from UN.IH[OF _ this] have "generate_topology (insert {a. Domainp A a} B) k"
         if "k \<in> K'`K" for k using that by auto
       from generate_topology.UN[OF this]
       have "generate_topology (insert {a. Domainp A a} B) (\<Union>(K'`K))" by auto
       also
       from K' have [transfer_rule]: "(rel_set (=) ===> rel_set A) K' id"
         by (fastforce simp: rel_fun_def rel_set_def)
       define U where "U =  (\<Union>(id ` K))"
       from \<open>rel_set A X _\<close> have [transfer_rule]: "rel_set A X U" by (simp add: U_def)
       from U_def have "\<Union>(K' ` K) = X" by transfer simp
       finally show ?case .
     next
       case (Basis s)
       note [transfer_rule] = \<open>rel_set A X s\<close>
       from \<open>s \<in> C\<close> have "X \<in> B" by transfer
       then show ?case by (intro generate_topology.Basis) auto
     qed
   qed
 qed
 
 end
 
 
 subsection \<open>Miscellaneous\<close>
 
 lemmas [simp del] = mem_ball
 
 lemma in_closureI[intro, simp]: "x \<in> X \<Longrightarrow> x \<in> closure X"
   using closure_subset by auto
 
 lemmas open_continuous_vimage = continuous_on_open_vimage[THEN iffD1, rule_format]
 lemma open_continuous_vimage': "open s \<Longrightarrow> continuous_on s f \<Longrightarrow> open B \<Longrightarrow> open (s \<inter> f -` B)"
   using open_continuous_vimage[of s f B] by (auto simp: Int_commute)
 
 lemma support_on_mono: "support_on carrier f \<subseteq> support_on carrier g"
   if "\<And>x. x \<in> carrier \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> g x \<noteq> 0"
   using that
   by (auto simp: support_on_def)
 
 
 lemma image_prod: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = f ` A \<times> g ` B" by auto
 
 
 subsection \<open>Closed support\<close>
 
 definition "csupport_on X S = closure (support_on X S)"
 
 lemma closed_csupport_on[intro, simp]: "closed (csupport_on carrier \<phi>)"
   by (auto simp: csupport_on_def)
 
 lemma not_in_csupportD: "x \<notin> csupport_on carrier \<phi> \<Longrightarrow> x \<in> carrier \<Longrightarrow> \<phi> x = 0"
   by (auto simp: csupport_on_def support_on_def)
 
 lemma csupport_on_mono: "csupport_on carrier f \<subseteq> csupport_on carrier g"
   if "\<And>x. x \<in> carrier \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> g x \<noteq> 0"
   unfolding csupport_on_def
   apply (rule closure_mono)
   using that
   by (rule support_on_mono)
 
 subsection \<open>Homeomorphism\<close>
 
 lemma homeomorphism_empty[simp]:
   "homeomorphism {} t f f' \<longleftrightarrow> t = {}"
   "homeomorphism s {} f f' \<longleftrightarrow> s = {}"
   by (auto simp: homeomorphism_def)
 
 lemma homeomorphism_add:
   "homeomorphism UNIV UNIV (\<lambda>x. x + c) (\<lambda>x. x - c)"
   for c::"_::real_normed_vector"
   unfolding homeomorphism_def
   by (auto simp: algebra_simps continuous_intros intro!: image_eqI[where x="x - c" for x])
 
 lemma in_range_scaleR_iff: "x \<in> range ((*\<^sub>R) c) \<longleftrightarrow> c = 0 \<longrightarrow> x = 0"
   for x::"_::real_vector"
   by (auto simp: intro!: image_eqI[where x="x /\<^sub>R c"])
 
 lemma homeomorphism_scaleR:
   "homeomorphism UNIV UNIV (\<lambda>x. c *\<^sub>R x::_::real_normed_vector) (\<lambda>x. x /\<^sub>R c)"
   if "c \<noteq> 0"
   using that
   unfolding homeomorphism_def
   by (auto simp: in_range_scaleR_iff algebra_simps intro!: continuous_intros)
 
 
 lemma homeomorphism_prod:
   "homeomorphism (a \<times> b) (c \<times> d) (\<lambda>(x, y). (f x, g y)) (\<lambda>(x, y). (f' x, g' y))"
   if "homeomorphism a c f f'"
      "homeomorphism b d g g'"
   using that by (simp add: homeomorphism_def image_prod)
     (auto simp add: split_beta intro!: continuous_intros elim: continuous_on_compose2)
 
 
 subsection \<open>Generalizations\<close>
 
-lemma univ_second_countable:
-  obtains \<B> :: "'a::second_countable_topology set set"
-  where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
-    "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
-  by (metis ex_countable_basis topological_basis_def)
-
-proposition Lindelof:
-  fixes \<F> :: "'a::second_countable_topology set set"
-  assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
-  obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
-proof -
-  obtain \<B> :: "'a set set"
-    where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
-      and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
-    using univ_second_countable by auto
-  define \<D> where "\<D> \<equiv> {S. S \<in> \<B> \<and> (\<exists>U. U \<in> \<F> \<and> S \<subseteq> U)}"
-  have "countable \<D>"
-    apply (rule countable_subset [OF _ \<open>countable \<B>\<close>])
-    apply (force simp: \<D>_def)
-    done
-  have "\<And>S. \<exists>U. S \<in> \<D> \<longrightarrow> U \<in> \<F> \<and> S \<subseteq> U"
-    by (simp add: \<D>_def)
-  then obtain G where G: "\<And>S. S \<in> \<D> \<longrightarrow> G S \<in> \<F> \<and> S \<subseteq> G S"
-    by metis
-  have "\<Union>\<F> \<subseteq> \<Union>\<D>"
-    unfolding \<D>_def by (blast dest: \<F> \<B>)
-  moreover have "\<Union>\<D> \<subseteq> \<Union>\<F>"
-    using \<D>_def by blast
-  ultimately have eq1: "\<Union>\<F> = \<Union>\<D>" ..
-  have eq2: "\<Union>\<D> = \<Union> (G ` \<D>)"
-    using G eq1 by auto
-  show ?thesis
-    apply (rule_tac \<F>' = "G ` \<D>" in that)
-    using G \<open>countable \<D>\<close>  apply (auto simp: eq1 eq2)
-    done
-qed
-
-
 lemma openin_subtopology_eq_generate_topology:
   "openin (top_of_set S) x = generate_topology (insert S ((\<lambda>B. B \<inter> S) ` BB)) x"
   if open_gen: "open = generate_topology BB" and subset: "x \<subseteq> S"
 proof -
   have "generate_topology (insert S ((\<lambda>B. B \<inter> S) ` BB)) (T \<inter> S)"
     if "generate_topology BB T"
     for T
     using that
   proof (induction)
     case UNIV
     then show ?case by (auto intro!: generate_topology.Basis)
   next
     case (Int a b)
     have "generate_topology (insert S ((\<lambda>B. B \<inter> S) ` BB)) (a \<inter> S \<inter> (b \<inter> S))"
       by (rule generate_topology.Int) (use Int in auto)
     then show ?case by (simp add: ac_simps)
   next
     case (UN K)
     then have "generate_topology (insert S ((\<lambda>B. B \<inter> S) ` BB)) (\<Union>k\<in>K. k \<inter> S)"
       by (intro generate_topology.UN) auto
     then show ?case by simp
   next
     case (Basis s)
     then show ?case
       by (intro generate_topology.Basis) auto
   qed
   moreover
   have "\<exists>T. generate_topology BB T \<and> x = T \<inter> S"
     if "generate_topology (insert S ((\<lambda>B. B \<inter> S) ` BB)) x" "x \<noteq> UNIV"
     using that
   proof (induction)
     case UNIV
     then show ?case by simp
   next
     case (Int a b)
     then show ?case
       using generate_topology.Int 
       by auto
   next
     case (UN K)
     from UN.IH have "\<forall>k\<in>K-{UNIV}. \<exists>T. generate_topology BB T \<and> k = T \<inter> S" by auto
     from this[THEN bchoice] obtain T where T: "\<And>k. k \<in> T ` (K - {UNIV}) \<Longrightarrow> generate_topology BB k" "\<And>k. k \<in> K - {UNIV} \<Longrightarrow> k = (T k) \<inter> S"
       by auto
     from generate_topology.UN[OF T(1)]
     have "generate_topology BB (\<Union>(T ` (K - {UNIV})))" by auto
     moreover have "\<Union>K = (\<Union>(T ` (K - {UNIV}))) \<inter> S" if "UNIV \<notin> K" using T(2) UN that by auto
     ultimately show ?case
       apply (cases "UNIV \<in> K") subgoal using UN by auto
       subgoal by auto
       done
   next
     case (Basis s)
-    from this(1) show ?case
-      apply rule
-      subgoal
-        apply (rule exI[where x=UNIV])
-        by (auto simp: generate_topology.UNIV)
-      subgoal
-        apply clarsimp
-        subgoal for B
-          apply (rule exI[where x="B"]) by (auto simp: generate_topology.Basis)
-        done
-      done
+    then show ?case
+      using generate_topology.UNIV generate_topology.Basis by blast
   qed
   moreover
   have "\<exists>T. generate_topology BB T \<and> UNIV = T \<inter> S" if "generate_topology (insert S ((\<lambda>B. B \<inter> S) ` BB)) x"
      "x = UNIV"
   proof -
     have "S = UNIV"
       using that \<open>x \<subseteq> S\<close>
       by auto
     then show ?thesis by (simp add: generate_topology.UNIV)
   qed
   ultimately show ?thesis
     by (metis open_gen open_openin openin_open_Int' openin_subtopology)
 qed
 
 subsection \<open>Equal topologies\<close>
 
 lemma topology_eq_iff: "t = s \<longleftrightarrow> (topspace t = topspace s \<and>
   (\<forall>x\<subseteq>topspace t. openin t x = openin s x))"
   by (metis (full_types) openin_subset topology_eq)
 
 
 subsection \<open>Finer topologies\<close>
 
 definition finer_than (infix "(finer'_than)" 50)
   where "T1 finer_than T2 \<longleftrightarrow> continuous_map T1 T2 (\<lambda>x. x)"
 
 lemma finer_than_iff_nhds:
   "T1 finer_than T2 \<longleftrightarrow> (\<forall>X. openin T2 X \<longrightarrow> openin T1 (X \<inter> topspace T1)) \<and> (topspace T1 \<subseteq> topspace T2)"
   by (auto simp: finer_than_def continuous_map_alt)
 
 lemma continuous_on_finer_topo:
   "continuous_map s t f"
   if "continuous_map s' t f" "s finer_than s'"
   using that
   by (auto simp: finer_than_def o_def dest: continuous_map_compose)
 
 lemma continuous_on_finer_topo2:
   "continuous_map s t f"
   if "continuous_map s t' f" "t' finer_than t"
   using that
   by (auto simp: finer_than_def o_def dest: continuous_map_compose)
 
 lemma antisym_finer_than: "S = T" if "S finer_than T" "T finer_than S"
   using that
   apply (auto simp: finer_than_def topology_eq_iff continuous_map_alt)
   apply (metis inf.orderE)+
   done
 
 lemma subtopology_finer_than[simp]: "top_of_set X finer_than euclidean"
   by (auto simp: finer_than_iff_nhds openin_subtopology)
 
 subsection \<open>Support\<close>
 
 lemma support_on_nonneg_sum:
   "support_on X (\<lambda>x. \<Sum>i\<in>S. f i x) = (\<Union>i\<in>S. support_on X (f i))"
   if "finite S" "\<And>x i . x \<in> X \<Longrightarrow> i \<in> S \<Longrightarrow> f i x \<ge> 0"
   for f::"_\<Rightarrow>_\<Rightarrow>_::ordered_comm_monoid_add"
   using that by (auto simp: support_on_def sum_nonneg_eq_0_iff)
 
 lemma support_on_nonneg_sum_subset:
   "support_on X (\<lambda>x. \<Sum>i\<in>S. f i x) \<subseteq> (\<Union>i\<in>S. support_on X (f i))"
   for f::"_\<Rightarrow>_\<Rightarrow>_::ordered_comm_monoid_add"
   by (cases "finite S") (auto simp: support_on_def dest!: sum_not_0)
 
 lemma support_on_nonneg_sum_subset':
   "support_on X (\<lambda>x. \<Sum>i\<in>S x. f i x) \<subseteq> (\<Union>x\<in>X. (\<Union>i\<in>S x. support_on X (f i)))"
   for f::"_\<Rightarrow>_\<Rightarrow>_::ordered_comm_monoid_add"
   by (auto simp: support_on_def dest!: sum_not_0)
 
 subsection \<open>Final topology (Bourbaki, General Topology I, 4.)\<close>
 
 definition "final_topology X Y f =
   topology (\<lambda>U. U \<subseteq> X \<and>
     (\<forall>i. openin (Y i) (f i -` U \<inter> topspace (Y i))))"
 
 lemma openin_final_topology:
   "openin (final_topology X Y f) =
     (\<lambda>U. U \<subseteq> X \<and> (\<forall>i. openin (Y i) (f i -` U \<inter> topspace (Y i))))"
   unfolding final_topology_def
   apply (rule topology_inverse')
   unfolding istopology_def
 proof safe
   fix S T i
   assume "\<forall>i. openin (Y i) (f i -` S \<inter> topspace (Y i))"
     "\<forall>i. openin (Y i) (f i -` T \<inter> topspace (Y i))"
   then have "openin (Y i) (f i -` S \<inter> topspace (Y i) \<inter> (f i -` T \<inter> topspace (Y i)))"
     (is "openin _ ?I")
     by auto
   also have "?I = f i -` (S \<inter> T) \<inter> topspace (Y i)"
     (is "_ = ?R")
     by auto
   finally show "openin (Y i) ?R" .
 next
   fix K i
   assume "\<forall>U\<in>K. U \<subseteq> X \<and> (\<forall>i. openin (Y i) (f i -` U \<inter> topspace (Y i)))"
   then have "openin (Y i) (\<Union>X\<in>K. f i -` X \<inter> topspace (Y i))"
     by (intro openin_Union) auto
   then show "openin (Y i) (f i -` \<Union>K \<inter> topspace (Y i))"
     by (auto simp: vimage_Union)
 qed force+
 
 lemma topspace_final_topology:
   "topspace (final_topology X Y f) = X"
   if "\<And>i. f i \<in> topspace (Y i) \<rightarrow> X"
 proof -
   have *: "f i -` X \<inter> topspace (Y i) = topspace (Y i)" for i
     using that
     by auto
   show ?thesis
     unfolding topspace_def
     unfolding openin_final_topology
     apply (rule antisym)
      apply force
     apply (rule subsetI)
     apply (rule UnionI[where X=X])
     using that
     by (auto simp: *)
 qed
 
 lemma continuous_on_final_topologyI2:
   "continuous_map (Y i) (final_topology X Y f) (f i)"
   if "\<And>i. f i \<in> topspace (Y i) \<rightarrow> X"
   using that
   by (auto simp: openin_final_topology continuous_map_alt topspace_final_topology)
 
 lemma continuous_on_final_topologyI1:
   "continuous_map (final_topology X Y f) Z g"
   if hyp: "\<And>i. continuous_map (Y i) Z (g o f i)"
     and that: "\<And>i. f i \<in> topspace (Y i) \<rightarrow> X" "g \<in> X \<rightarrow> topspace Z"
   unfolding continuous_map_alt
 proof safe
   fix V assume V: "openin Z V"
   have oV: "openin (Y i) (f i -` g -` V \<inter> topspace (Y i))"
     for i
     using hyp[rule_format, of i] V
     by (auto simp: continuous_map_alt vimage_comp dest!: spec[where x=V])
   have *: "f i -` g -` V \<inter> f i -` X \<inter> topspace (Y i) =
       f i -` g -` V \<inter> topspace (Y i)"
     (is "_ = ?rhs i")
     for i using that
     by auto
   show "openin (final_topology X Y f) (g -` V \<inter> topspace (final_topology X Y f))"
     by (auto simp: openin_final_topology oV topspace_final_topology that *)
 qed (use that in \<open>auto simp: topspace_final_topology\<close>)
 
 
 lemma continuous_on_final_topology_iff:
   "continuous_map (final_topology X Y f) Z g \<longleftrightarrow> (\<forall>i. continuous_map (Y i) Z (g o f i))"
   if "\<And>i. f i \<in> topspace (Y i) \<rightarrow> X" "g \<in> X \<rightarrow> topspace Z"
   using that
   by (auto intro!: continuous_on_final_topologyI1[OF _ that]
       intro: continuous_map_compose[OF continuous_on_final_topologyI2[OF that(1)]])
 
 
 subsection \<open>Quotient topology\<close>
 
 definition map_topology :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a topology \<Rightarrow> 'b topology" where
   "map_topology p X = final_topology (p ` topspace X) (\<lambda>_. X) (\<lambda>(_::unit). p)"
 
 lemma openin_map_topology:
   "openin (map_topology p X) = (\<lambda>U. U \<subseteq> p ` topspace X \<and> openin X (p -` U \<inter> topspace X))"
   by (auto simp: map_topology_def openin_final_topology)
 
 lemma topspace_map_topology[simp]: "topspace (map_topology f T) = f ` topspace T"
   unfolding map_topology_def
   by (subst topspace_final_topology) auto
 
 lemma continuous_on_map_topology:
   "continuous_map T (map_topology f T) f"
   unfolding continuous_map_alt openin_map_topology
   by auto
 
 lemma continuous_map_composeD:
   "continuous_map T X (g \<circ> f) \<Longrightarrow> g \<in> f ` topspace T \<rightarrow> topspace X"
   by (auto simp: continuous_map_def)
 
 lemma continuous_on_map_topology2:
   "continuous_map T X (g \<circ> f) \<longleftrightarrow> continuous_map (map_topology f T) X g"
   unfolding map_topology_def
   apply safe
   subgoal
     apply (rule continuous_on_final_topologyI1)
     subgoal by assumption
     subgoal by force
     subgoal by (rule continuous_map_composeD)
     done
   subgoal
     apply (erule continuous_map_compose[rotated])
     apply (rule continuous_on_final_topologyI2)
     by force
   done
 
 lemma map_sub_finer_than_commute:
   "map_topology f (subtopology T (f -` X)) finer_than subtopology (map_topology f T) X"
   by (auto simp: finer_than_def continuous_map_def openin_subtopology openin_map_topology
       topspace_subtopology)
 
 lemma sub_map_finer_than_commute:
   "subtopology (map_topology f T) X finer_than map_topology f (subtopology T (f -` X))"
   if "openin T (f -` X)"\<comment> \<open>this is more or less the condition from
     \<^url>\<open>https://math.stackexchange.com/questions/705840/quotient-topology-vs-subspace-topology\<close>\<close>
   unfolding finer_than_def continuous_map_alt
 proof (rule conjI, clarsimp)
   fix U
   assume "openin (map_topology f (subtopology T (f -` X))) U"
   then obtain W where W: "U \<subseteq> f ` (topspace T \<inter> f -` X)" "openin T W" "f -` U \<inter> (topspace T \<inter> f -` X) = W \<inter> f -` X"
     by (auto simp: topspace_subtopology openin_subtopology openin_map_topology)
   have "(f -` f ` W \<inter> f -` X) \<inter> topspace T = W \<inter> topspace T \<inter> f -` X"
     apply auto
     by (metis Int_iff W(3) vimage_eq)
   also have "openin T \<dots>"
     by (auto intro!: W that)
   finally show "openin (subtopology (map_topology f T) X) (U \<inter> (f ` topspace T \<inter> X))"
     using W
     unfolding topspace_subtopology topspace_map_topology openin_subtopology openin_map_topology
     by (intro exI[where x="(f ` W \<inter> X)"]) auto
 qed auto
 
 lemma subtopology_map_topology:
   "subtopology (map_topology f T) X = map_topology f (subtopology T (f -` X))"
   if "openin T (f -` X)"
   apply (rule antisym_finer_than)
   using sub_map_finer_than_commute[OF that] map_sub_finer_than_commute[of f T X]
   by auto
 
 lemma quotient_map_map_topology:
   "quotient_map X (map_topology f X) f"
   by (auto simp: quotient_map_def openin_map_topology ac_simps)
     (simp_all add: vimage_def Int_def)
 
 lemma topological_space_quotient: "class.topological_space (openin (map_topology f euclidean))"
   if "surj f"
   apply standard
     apply (auto simp: )
   using that
   by (auto simp: openin_map_topology)
 
 lemma t2_space_quotient: "class.t2_space (open::'b set \<Rightarrow> bool)"
   if open_def: "open = (openin (map_topology (p::'a::t2_space\<Rightarrow>'b::topological_space) euclidean))"
     "surj p" and open_p: "\<And>X. open X \<Longrightarrow> open (p ` X)" and "closed {(x, y). p x = p y}" (is "closed ?R")
   apply (rule class.t2_space.intro)
   subgoal by (unfold open_def, rule topological_space_quotient; fact)
 proof standard
   fix a b::'b
   obtain x y where a_def: "a = p x" and b_def: "b = p y" using \<open>surj p\<close> by fastforce
   assume "a \<noteq> b"
   with \<open>closed ?R\<close> have "open (-?R)" "(x, y) \<in> -?R" by (auto simp add: a_def b_def)
   from open_prod_elim[OF this]
   obtain N\<^sub>x N\<^sub>y where "open N\<^sub>x" "open N\<^sub>y" "(x, y) \<in> N\<^sub>x \<times> N\<^sub>y" "N\<^sub>x \<times> N\<^sub>y \<subseteq> -?R" .
   then have "p ` N\<^sub>x \<inter> p ` N\<^sub>y = {}" by auto
   moreover
   from \<open>open N\<^sub>x\<close> \<open>open N\<^sub>y\<close> have "open (p ` N\<^sub>x)" "open (p ` N\<^sub>y)"
     using open_p by blast+
   moreover have "a \<in> p ` N\<^sub>x" "b \<in> p ` N\<^sub>y" using \<open>(x, y) \<in> _ \<times> _\<close> by (auto simp: a_def b_def)
   ultimately show "\<exists>U V. open U \<and> open V \<and> a \<in> U \<and> b \<in> V \<and> U \<inter> V = {}" by blast
 qed
 
 lemma second_countable_topology_quotient: "class.second_countable_topology (open::'b set \<Rightarrow> bool)"
   if open_def: "open = (openin (map_topology (p::'a::second_countable_topology\<Rightarrow>'b::topological_space) euclidean))"
     "surj p" and open_p: "\<And>X. open X \<Longrightarrow> open (p ` X)"
   apply (rule class.second_countable_topology.intro)
   subgoal by (unfold open_def, rule topological_space_quotient; fact)
 proof standard
   have euclidean_def: "euclidean = map_topology p euclidean"
     by (simp add: openin_inverse open_def)
   have continuous_on: "continuous_on UNIV p"
     using continuous_map_iff_continuous2 continuous_on_map_topology euclidean_def by fastforce
   from ex_countable_basis[where 'a='a] obtain A::"'a set set" where "countable A" "topological_basis A"
     by auto
   define B where "B = (\<lambda>X. p ` X) ` A"
   have "countable (B::'b set set)"
     by (auto simp: B_def intro!: \<open>countable A\<close>)
   moreover have "topological_basis B"
   proof (rule topological_basisI)
     fix B' assume "B' \<in> B" then show "open B'" using \<open>topological_basis A\<close>
       by (auto simp: B_def topological_basis_open intro!: open_p)
   next
     fix x::'b and O' assume "open O'" "x \<in> O'"
     have "open (p -` O')"
       using \<open>open O'\<close>
       by (rule open_vimage) (auto simp: continuous_on)
     obtain y where y: "y \<in> p -` {x}"
       using \<open>x \<in> O'\<close>
       by auto (metis UNIV_I open_def(2) rangeE)
     then have "y \<in> p -` O'" using \<open>x \<in> O'\<close> by auto
     from topological_basisE[OF \<open>topological_basis A\<close> \<open>open (p -` O')\<close> this]
     obtain C where "C \<in> A" "y \<in> C" "C \<subseteq> p -` O'" .
     let ?B' = "p ` C"
     have "?B' \<in> B"
       using \<open>C \<in> A\<close> by (auto simp: B_def)
     moreover
     have "x \<in> ?B'" using y \<open>y \<in> C\<close> \<open>x \<in> O'\<close>
       by auto
     moreover
     have "?B' \<subseteq> O'"
       using \<open>C \<subseteq> _\<close> by auto
     ultimately show "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" by metis
   qed
   ultimately show "\<exists>B::'b set set. countable B \<and> open = generate_topology B"
     by (auto simp: topological_basis_imp_subbasis)
 qed
 
 
 subsection \<open>Closure\<close>
 
 lemma closure_Union: "closure (\<Union>X) = (\<Union>x\<in>X. closure x)" if "finite X"
   using that
   by (induction X) auto
 
 subsection \<open>Compactness\<close>
 
 lemma compact_if_closed_subset_of_compact:
   "compact S" if "closed S" "compact T" "S \<subseteq> T"
 proof (rule compactI)
   fix UU assume UU: "\<forall>t\<in>UU. open t" "S \<subseteq> \<Union>UU"
   have "T \<subseteq> \<Union>(insert (- S) (UU))" "\<And>B. B \<in> insert (- S) UU \<Longrightarrow> open B"
     using UU \<open>S \<subseteq> T\<close>
     by (auto simp: open_Compl \<open>closed S\<close>)
   from compactE[OF \<open>compact T\<close> this]
   obtain \<T>' where \<T>: "\<T>' \<subseteq> insert (- S) UU" "finite \<T>'" "T \<subseteq> \<Union>\<T>'"
     by metis
   show "\<exists>C'\<subseteq>UU. finite C' \<and> S \<subseteq> \<Union>C'"
     apply (rule exI[where x="\<T>' - {-S}"])
     using \<T> UU
     apply auto
   proof -
     fix x assume "x \<in> S"
     with \<T> \<open>S \<subseteq> T\<close> obtain U where "x \<in> U" "U \<in> \<T>'" using \<T>
       by auto
     then show "\<exists>X\<in>\<T>' - {- S}. x \<in> X"
       using \<T> UU \<open>x \<in> S\<close>
       apply -
       apply (rule bexI[where x=U])
       by auto
   qed
 qed
 
 subsection \<open>Locally finite\<close>
 
 definition "locally_finite_on X I U \<longleftrightarrow> (\<forall>p\<in>X. \<exists>N. p\<in>N \<and> open N \<and> finite {i\<in>I. U i \<inter> N \<noteq> {}})"
 
 lemmas locally_finite_onI = locally_finite_on_def[THEN iffD2, rule_format]
 
 lemma locally_finite_onE:
   assumes "locally_finite_on X I U"
   assumes "p \<in> X"
   obtains N where "p \<in> N" "open N" "finite {i\<in>I. U i \<inter> N \<noteq> {}}"
   using assms
   by (auto simp: locally_finite_on_def)
 
 lemma locally_finite_onD:
   assumes "locally_finite_on X I U"
   assumes "p \<in> X"
   shows "finite {i\<in>I. p \<in> U i}"
   apply (rule locally_finite_onE[OF assms])
   apply (rule finite_subset)
   by auto
 
 lemma locally_finite_on_open_coverI: "locally_finite_on X I U"
   if fin: "\<And>j. j \<in> I \<Longrightarrow> finite {i\<in>I. U i \<inter> U j \<noteq> {}}"
     and open_cover: "X \<subseteq> (\<Union>i\<in>I. U i)" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
 proof (rule locally_finite_onI)
   fix p assume "p \<in> X"
   then obtain i where i: "i \<in> I" "p \<in> U i" "open (U i)"
     using open_cover
     by blast
   show "\<exists>N. p \<in> N \<and> open N \<and> finite {i \<in> I. U i \<inter> N \<noteq> {}}"
     by (intro exI[where x="U i"] conjI i fin)
 qed
 
 lemma locally_finite_compactD:
   "finite {i\<in>I. U i \<inter> V \<noteq> {}}"
   if lf: "locally_finite_on X I U"
     and compact: "compact V"
     and subset: "V \<subseteq> X"
 proof -
   have "\<exists>N. \<forall>p \<in> X. p \<in> N p \<and> open (N p) \<and> finite {i\<in>I. U i \<inter> N p \<noteq> {}}"
     by (rule bchoice) (auto elim!: locally_finite_onE[OF lf, rule_format])
   then obtain N where N: "\<And>p. p \<in> X \<Longrightarrow> p \<in> N p"
     "\<And>p. p \<in> X \<Longrightarrow> open (N p)"
     "\<And>p. p \<in> X \<Longrightarrow> finite {i\<in>I. U i \<inter> N p \<noteq> {}}"
     by blast
   have "V \<subseteq> (\<Union>p\<in>X. N p)" "\<And>B. B \<in> N ` X \<Longrightarrow> open B"
     using N subset by force+
   from compactE[OF compact this]
   obtain C where C: "C \<subseteq> X" "finite C" "V \<subseteq> \<Union>(N ` C)"
     by (metis finite_subset_image)
   then have "{i\<in>I. U i \<inter> V \<noteq> {}} \<subseteq> {i\<in>I. U i \<inter> \<Union>(N ` C) \<noteq> {}}"
     by force
   also have "\<dots> \<subseteq> (\<Union>c\<in>C. {i\<in>I. U i \<inter> N c \<noteq> {}})"
     by force
   also have "finite \<dots>"
     apply (rule finite_Union)
     using C by (auto intro!: C N)
   finally (finite_subset) show ?thesis .
 qed
 
 lemma closure_Int_open_eq_empty: "open S \<Longrightarrow> (closure T \<inter> S) = {} \<longleftrightarrow> T \<inter> S = {}"
   by (auto simp: open_Int_closure_eq_empty ac_simps)
 
 lemma locally_finite_on_subset:
   assumes "locally_finite_on X J U"
   assumes "\<And>i. i \<in> I \<Longrightarrow> V i \<subseteq> U i" "I \<subseteq> J"
   shows "locally_finite_on X I V"
 proof (rule locally_finite_onI)
   fix p assume "p \<in> X"
   from locally_finite_onE[OF assms(1) this]
   obtain N where "p \<in> N" "open N" "finite {i \<in> J. U i \<inter> N \<noteq> {}}" .
   then show "\<exists>N. p \<in> N \<and> open N \<and> finite {i \<in> I. V i \<inter> N \<noteq> {}}"
     apply (intro exI[where x=N])
     using assms
     by (auto elim!: finite_subset[rotated])
 qed
 
 lemma locally_finite_on_closure:
   "locally_finite_on X I (\<lambda>x. closure (U x))"
   if "locally_finite_on X I U"
 proof (rule locally_finite_onI)
   fix p assume "p \<in> X"
   from locally_finite_onE[OF that this] obtain N
     where "p \<in> N" "open N" "finite {i \<in> I. U i \<inter> N \<noteq> {}}" .
   then show "\<exists>N. p \<in> N \<and> open N \<and> finite {i \<in> I. closure (U i) \<inter> N \<noteq> {}}"
     by (auto intro!: exI[where x=N] simp: closure_Int_open_eq_empty)
 qed
 
 
 lemma locally_finite_on_closedin_Union_closure:
   "closedin (top_of_set X) (\<Union>i\<in>I. closure (U i))"
   if "locally_finite_on X I U" "\<And>i. i \<in> I \<Longrightarrow> closure (U i) \<subseteq> X"
   unfolding closedin_def
   apply safe
   subgoal using that(2) by auto
   subgoal
     apply (subst openin_subopen)
   proof clarsimp
     fix x
     assume x: "x \<in> X" "\<forall>i\<in>I. x \<notin> closure (U i)"
     from locally_finite_onE[OF that(1) \<open>x \<in> X\<close>]
     obtain N where N: "x \<in> N" "open N" "finite {i \<in> I. U i \<inter> N \<noteq> {}}" (is "finite ?I").
     define N' where "N' = N - (\<Union>i \<in> ?I. closure (U i))"
     have "open N'"
       by (auto simp: N'_def intro!: N)
     then have "openin (top_of_set X) (X \<inter> N')"
       by (rule openin_open_Int)
     moreover
     have "x \<in> X \<inter> N'" using x
       by (auto simp: N'_def N)
     moreover
     have "X \<inter> N' \<subseteq> X - (\<Union>i\<in>I. closure (U i))"
       using x that(2)
       apply (auto simp: N'_def)
       by (meson N(2) closure_iff_nhds_not_empty dual_order.refl)
     ultimately show "\<exists>T. openin (top_of_set X) T \<and> x \<in> T \<and> T \<subseteq> X - (\<Union>i\<in>I. closure (U i))"
       by auto
   qed
   done
 
 lemma closure_subtopology_minimal:
   "S \<subseteq> T \<Longrightarrow> closedin (top_of_set X) T \<Longrightarrow> closure S \<inter> X \<subseteq> T"
   apply (auto simp: closedin_closed)
   using closure_minimal by blast
 
 lemma locally_finite_on_closure_Union:
   "(\<Union>i\<in>I. closure (U i)) = closure (\<Union>i\<in>I. (U i)) \<inter> X"
   if "locally_finite_on X I U" "\<And>i. i \<in> I \<Longrightarrow> closure (U i) \<subseteq> X"
 proof (rule antisym)
   show "(\<Union>i\<in>I. closure (U i)) \<subseteq> closure (\<Union>i\<in>I. U i) \<inter> X"
     using that
     apply auto
     by (metis (no_types, lifting) SUP_le_iff closed_closure closure_minimal closure_subset subsetCE)
   show "closure (\<Union>i\<in>I. U i) \<inter> X \<subseteq> (\<Union>i\<in>I. closure (U i))"
     apply (rule closure_subtopology_minimal)
     apply auto
     using that
     by (auto intro!: locally_finite_on_closedin_Union_closure)
 qed
 
 
 subsection \<open>Refinement of cover\<close>
 
 definition refines :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> bool" (infix "refines" 50)
   where "A refines B \<longleftrightarrow> (\<forall>s\<in>A. (\<exists>t. t \<in> B \<and> s \<subseteq> t))"
 
 lemma refines_subset: "x refines y" if "z refines y" "x \<subseteq> z"
   using that by (auto simp: refines_def)
 
 subsection \<open>Functions as vector space\<close>
 
 instantiation "fun" :: (type, scaleR) scaleR begin
 
 definition scaleR_fun :: "real \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
   "scaleR_fun r f = (\<lambda>x. r *\<^sub>R f x)"
 
 lemma scaleR_fun_beta[simp]: "(r *\<^sub>R f) x = r *\<^sub>R f x"
   by (simp add: scaleR_fun_def)
 
 instance ..
 
 end
 
 instance "fun" :: (type, real_vector) real_vector
   by standard (auto simp: scaleR_fun_def algebra_simps)
 
 
 subsection \<open>Additional lemmas\<close>
 
 lemmas [simp del] = vimage_Un vimage_Int
 
 lemma finite_Collect_imageI: "finite {U \<in> f ` X. P U}" if "finite {x\<in>X. P (f x)}"
 proof -
   have "{d \<in> f ` X. P d} \<subseteq> f ` {c \<in> X. P (f c)}"
     by blast
   then show ?thesis
     using finite_surj that by blast
 qed
 
 lemma plus_compose: "(x + y) \<circ> f = (x \<circ> f) + (y \<circ> f)"
   by auto
 
 lemma mult_compose: "(x * y) \<circ> f = (x \<circ> f) * (y \<circ> f)"
   by auto
 
 lemma scaleR_compose: "(c *\<^sub>R x) \<circ> f = c *\<^sub>R (x \<circ> f)"
   by (auto simp:)
 
 lemma image_scaleR_ball:
   fixes a :: "'a::real_normed_vector"
   shows "c \<noteq> 0 \<Longrightarrow> (*\<^sub>R) c ` ball a r = ball (c *\<^sub>R a) (abs c *\<^sub>R r)"
 proof (auto simp: mem_ball dist_norm, goal_cases)
   case (1 b)
   have "norm (c *\<^sub>R a - c *\<^sub>R b)  = abs c * norm (a - b)"
     by (auto simp: norm_scaleR[symmetric] algebra_simps simp del: norm_scaleR)
   also have "\<dots> < abs c * r"
     apply (rule mult_strict_left_mono)
     using 1 by auto
   finally show ?case .
 next
   case (2 x)
   have "norm (a - x /\<^sub>R c) < r"
   proof -
     have "norm (a - x /\<^sub>R c) = abs c *\<^sub>R norm (a - x /\<^sub>R c) /\<^sub>R abs c"
       using 2 by auto
     also have "abs c *\<^sub>R norm (a - x /\<^sub>R c) = norm (c *\<^sub>R a - x)"
       using 2
       by (auto simp: norm_scaleR[symmetric] algebra_simps simp del: norm_scaleR)
     also have "\<dots> < \<bar>c\<bar> * r"
       by fact
     also have "\<bar>c\<bar> * r /\<^sub>R \<bar>c\<bar> = r" using 2 by auto
     finally show ?thesis using 2 by auto
   qed
   then have xdc: "x /\<^sub>R c \<in> ball a r"
     by (auto simp: mem_ball dist_norm)
   show ?case
     apply (rule image_eqI[OF _ xdc])
     using 2 by simp
 qed
 
 
 subsection \<open>Continuity\<close>
 
 lemma continuous_within_topologicalE:
   assumes "continuous (at x within s) f"
     "open B" "f x \<in> B"
   obtains A where "open A" "x \<in> A" "\<And>y. y \<in> s \<Longrightarrow> y \<in> A \<Longrightarrow> f y \<in> B"
   using assms continuous_within_topological by metis
 
 lemma continuous_within_topologicalE':
   assumes "continuous (at x) f"
     "open B" "f x \<in> B"
   obtains A where "open A" "x \<in> A" "f ` A \<subseteq> B"
   using assms continuous_within_topologicalE[OF assms]
   by (metis UNIV_I image_subsetI)
 
 lemma continuous_on_inverse: "continuous_on S f \<Longrightarrow> 0 \<notin> f ` S \<Longrightarrow> continuous_on S (\<lambda>x. inverse (f x))"
   for f::"_\<Rightarrow>_::real_normed_div_algebra"
   by (auto simp: continuous_on_def intro!: tendsto_inverse)
 
 
 subsection \<open>@{term "(has_derivative)"}\<close>
 
 lemma has_derivative_plus_fun[derivative_intros]:
   "(x + y has_derivative x' + y') (at a within A)"
   if [derivative_intros]:
     "(x has_derivative x') (at a within A)"
     "(y has_derivative y') (at a within A)"
   by (auto simp: plus_fun_def intro!: derivative_eq_intros)
 
 lemma has_derivative_scaleR_fun[derivative_intros]:
   "(x *\<^sub>R y has_derivative x *\<^sub>R y') (at a within A)"
   if [derivative_intros]:
     "(y has_derivative y') (at a within A)"
   by (auto simp: scaleR_fun_def intro!: derivative_eq_intros)
 
 lemma has_derivative_times_fun[derivative_intros]:
   "(x * y has_derivative (\<lambda>h. x a * y' h + x' h * y a)) (at a within A)"
   if [derivative_intros]:
     "(x has_derivative x') (at a within A)"
     "(y has_derivative y') (at a within A)"
   for x y::"_\<Rightarrow>'a::real_normed_algebra"
   by (auto simp: times_fun_def intro!: derivative_eq_intros)
 
 lemma real_sqrt_has_derivative_generic:
   "x \<noteq> 0 \<Longrightarrow> (sqrt has_derivative (*) ((if x > 0 then 1 else -1) * inverse (sqrt x) / 2)) (at x within S)"
   apply (rule has_derivative_at_withinI)
   using DERIV_real_sqrt_generic[of x "(if x > 0 then 1 else -1) * inverse (sqrt x) / 2"] at_within_open[of x "UNIV - {0}"]
   by (auto simp: has_field_derivative_def open_delete ac_simps split: if_splits)
 
 lemma sqrt_has_derivative:
   "((\<lambda>x. sqrt (f x)) has_derivative (\<lambda>xa. (if 0 < f x then 1 else - 1) / (2 * sqrt (f x)) * f' xa)) (at x within S)"
   if "(f has_derivative f') (at x within S)" "f x \<noteq> 0"
   by (rule has_derivative_eq_rhs[OF has_derivative_compose[OF that(1) real_sqrt_has_derivative_generic, OF that(2)]])
     (auto simp: divide_simps)
 
 lemmas has_derivative_norm_compose[derivative_intros] = has_derivative_compose[OF _ has_derivative_norm]
 
 subsection \<open>Differentiable\<close>
 
 lemmas differentiable_on_empty[simp]
 
 lemma differentiable_transform_eventually: "f differentiable (at x within X)"
   if "g differentiable (at x within X)"
     "f x = g x"
     "\<forall>\<^sub>F x in (at x within X). f x = g x"
   using that
   apply (auto simp: differentiable_def)
   subgoal for D
     apply (rule exI[where x=D])
     apply (auto simp: has_derivative_within)
     by (simp add: eventually_mono Lim_transform_eventually)
   done
 
 lemma differentiable_within_eqI: "f differentiable at x within X"
   if "g differentiable at x within X" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"
     "x \<in> X" "open X"
   apply (rule differentiable_transform_eventually)
     apply (rule that)
    apply (auto simp: that)
 proof -
   have "\<forall>\<^sub>F x in at x within X. x \<in> X"
     using \<open>open X\<close>
     using eventually_at_topological by blast
   then show " \<forall>\<^sub>F x in at x within X. f x = g x"
     by eventually_elim (auto simp: that)
 qed
 
 lemma differentiable_eqI: "f differentiable at x"
   if "g differentiable at x" "\<And>x. x \<in> X \<Longrightarrow> f x = g x" "x \<in> X" "open X"
   using that
   unfolding at_within_open[OF that(3,4), symmetric]
   by (rule differentiable_within_eqI)
 
 lemma differentiable_on_eqI:
   "f differentiable_on S"
   if "g differentiable_on S" "\<And>x. x \<in> S \<Longrightarrow> f x = g x" "open S"
   using that differentiable_eqI[of g _ S f]
   by (auto simp: differentiable_on_eq_differentiable_at)
 
 lemma differentiable_on_comp: "(f o g) differentiable_on S"
   if "g differentiable_on S" "f differentiable_on (g ` S)"
   using that
   by (auto simp: differentiable_on_def intro: differentiable_chain_within)
 
 lemma differentiable_on_comp2: "(f o g) differentiable_on S"
   if  "f differentiable_on T" "g differentiable_on S" "g ` S \<subseteq> T"
   apply (rule differentiable_on_comp)
    apply (rule that)
   apply (rule differentiable_on_subset)
   apply (rule that)
   apply (rule that)
   done
 
 lemmas differentiable_on_compose2 = differentiable_on_comp2[unfolded o_def]
 
 lemma differentiable_on_openD: "f differentiable at x"
   if "f differentiable_on X" "open X" "x \<in> X"
   using differentiable_on_eq_differentiable_at that by blast
 
 lemma differentiable_on_add_fun[intro, simp]:
   "x differentiable_on UNIV \<Longrightarrow> y differentiable_on UNIV \<Longrightarrow> x + y differentiable_on UNIV"
   by (auto simp: plus_fun_def)
 
 lemma differentiable_on_mult_fun[intro, simp]:
   "x differentiable_on UNIV \<Longrightarrow> y differentiable_on UNIV \<Longrightarrow> x * y differentiable_on UNIV"
   for x y::"_\<Rightarrow>'a::real_normed_algebra"
   by (auto simp: times_fun_def)
 
 lemma differentiable_on_scaleR_fun[intro, simp]:
   "y differentiable_on UNIV \<Longrightarrow> x *\<^sub>R y differentiable_on UNIV"
   by (auto simp: scaleR_fun_def)
 
 lemma sqrt_differentiable:
   "(\<lambda>x. sqrt (f x)) differentiable (at x within S)"
   if "f differentiable (at x within S)" "f x \<noteq> 0"
   using that
   using sqrt_has_derivative[of f _ x S]
   by (auto simp: differentiable_def)
 
 lemma sqrt_differentiable_on: "(\<lambda>x. sqrt (f x)) differentiable_on S"
   if "f differentiable_on S" "0 \<notin> f ` S"
   using sqrt_differentiable[of f _ S] that
   by (force simp: differentiable_on_def)
 
 lemma differentiable_on_inverse: "f differentiable_on S \<Longrightarrow> 0 \<notin> f ` S \<Longrightarrow> (\<lambda>x. inverse (f x)) differentiable_on S"
   for f::"_\<Rightarrow>_::real_normed_field"
   by (auto simp: differentiable_on_def intro!: differentiable_inverse)
 
 lemma differentiable_on_openI:
   "f differentiable_on S"
   if "open S" "\<And>x. x \<in> S \<Longrightarrow> \<exists>f'. (f has_derivative f') (at x)"
   using that
   by (auto simp: differentiable_on_def at_within_open[where S=S] differentiable_def)
 
 lemmas differentiable_norm_compose_at = differentiable_compose[OF differentiable_norm_at]
 
 lemma differentiable_on_Pair:
   "f differentiable_on S \<Longrightarrow> g differentiable_on S \<Longrightarrow> (\<lambda>x. (f x, g x)) differentiable_on S"
   unfolding differentiable_on_def
   using differentiable_Pair[of f _ S g] by auto
 
 lemma differentiable_at_fst:
   "(\<lambda>x. fst (f x)) differentiable at x within X" if "f differentiable at x within X"
   using that
   by (auto simp: differentiable_def dest!: has_derivative_fst)
 
 lemma differentiable_at_snd:
   "(\<lambda>x. snd (f x)) differentiable at x within X" if "f differentiable at x within X"
   using that
   by (auto simp: differentiable_def dest!: has_derivative_snd)
 
 lemmas frechet_derivative_worksI = frechet_derivative_works[THEN iffD1]
 
 lemma sin_differentiable_at: "(\<lambda>x. sin (f x::real)) differentiable at x within X"
   if "f differentiable at x within X"
-  by (auto intro!: differentiableI derivative_eq_intros frechet_derivative_worksI[OF that])
+  using differentiable_def has_derivative_sin that by blast
 
 lemma cos_differentiable_at: "(\<lambda>x. cos (f x::real)) differentiable at x within X"
   if "f differentiable at x within X"
-  by (auto intro!: differentiableI derivative_eq_intros frechet_derivative_worksI[OF that])
+  using differentiable_def has_derivative_cos that by blast
 
 
 subsection \<open>Frechet derivative\<close>
 
-lemma frechet_derivative_transform_within_open:
-  "frechet_derivative f (at x) = frechet_derivative g (at x)"
-  if "open X" "x \<in> X" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"
-    "f differentiable at x"
-  apply (rule frechet_derivative_at)
-  apply (rule has_derivative_transform_within_open[OF _ that(1-3)])
-  unfolding frechet_derivative_works[symmetric]
-  by fact
-
 lemmas frechet_derivative_transform_within_open_ext =
   fun_cong[OF frechet_derivative_transform_within_open]
 
 lemmas frechet_derivative_at' = frechet_derivative_at[symmetric]
 
-lemma frechet_derivative_const: "frechet_derivative (\<lambda>x. c) (at a) = (\<lambda>x. 0)"
-  by (rule frechet_derivative_at')
-    (auto intro!: derivative_eq_intros frechet_derivative_worksI)
-
-lemma frechet_derivative_id: "frechet_derivative (\<lambda>x. x) (at a) = (\<lambda>x. x)"
-  by (rule frechet_derivative_at')
-    (auto intro!: derivative_eq_intros frechet_derivative_worksI)
-
 lemma frechet_derivative_plus_fun:
   "x differentiable at a \<Longrightarrow> y differentiable at a \<Longrightarrow>
   frechet_derivative (x + y) (at a) =
     frechet_derivative x (at a) + frechet_derivative y (at a)"
   by (rule frechet_derivative_at')
     (auto intro!: derivative_eq_intros frechet_derivative_worksI)
 
 lemmas frechet_derivative_plus = frechet_derivative_plus_fun[unfolded plus_fun_def]
 
 lemma frechet_derivative_zero_fun: "frechet_derivative 0 (at a) = 0"
   by (auto simp: frechet_derivative_const zero_fun_def)
 
 lemma frechet_derivative_sin:
   "frechet_derivative (\<lambda>x. sin (f x)) (at x) = (\<lambda>xa. frechet_derivative f (at x) xa * cos (f x))"
   if "f differentiable (at x)"
   for f::"_\<Rightarrow>real"
   by (rule frechet_derivative_at'[OF has_derivative_sin[OF frechet_derivative_worksI[OF that]]])
 
 lemma frechet_derivative_cos:
   "frechet_derivative (\<lambda>x. cos (f x)) (at x) = (\<lambda>xa. frechet_derivative f (at x) xa * - sin (f x))"
   if "f differentiable (at x)"
   for f::"_\<Rightarrow>real"
   by (rule frechet_derivative_at'[OF has_derivative_cos[OF frechet_derivative_worksI[OF that]]])
 
 lemma differentiable_sum_fun:
   "(\<And>i. i \<in> I \<Longrightarrow> (f i differentiable at a)) \<Longrightarrow> sum f I differentiable at a"
   by (induction I rule: infinite_finite_induct) (auto simp: zero_fun_def plus_fun_def)
 
 lemma frechet_derivative_sum_fun:
   "(\<And>i. i \<in> I \<Longrightarrow> (f i differentiable at a)) \<Longrightarrow>
   frechet_derivative (\<Sum>i\<in>I. f i) (at a) = (\<Sum>i\<in>I. frechet_derivative (f i) (at a))"
   by (induction I rule: infinite_finite_induct)
     (auto simp: frechet_derivative_zero_fun frechet_derivative_plus_fun differentiable_sum_fun)
 
 lemma sum_fun_def: "(\<Sum>i\<in>I. f i) = (\<lambda>x. \<Sum>i\<in>I. f i x)"
   by (induction I rule: infinite_finite_induct) auto
 
 lemmas frechet_derivative_sum = frechet_derivative_sum_fun[unfolded sum_fun_def]
 
 
 lemma frechet_derivative_times_fun:
   "f differentiable at a \<Longrightarrow> g differentiable at a \<Longrightarrow>
   frechet_derivative (f * g) (at a) =
   (\<lambda>x. f a * frechet_derivative g (at a) x + frechet_derivative f (at a) x * g a)"
   for f g::"_\<Rightarrow>'a::real_normed_algebra"
   by (rule frechet_derivative_at') (auto intro!: derivative_eq_intros frechet_derivative_worksI)
 
 lemmas frechet_derivative_times = frechet_derivative_times_fun[unfolded times_fun_def]
 
 lemma frechet_derivative_scaleR_fun:
   "y differentiable at a \<Longrightarrow>
   frechet_derivative (x *\<^sub>R y) (at a) =
     x *\<^sub>R frechet_derivative y (at a)"
   by (rule frechet_derivative_at')
     (auto intro!: derivative_eq_intros frechet_derivative_worksI)
 
 lemmas frechet_derivative_scaleR = frechet_derivative_scaleR_fun[unfolded scaleR_fun_def]
 
 lemma frechet_derivative_compose:
   "frechet_derivative (f o g) (at x) = frechet_derivative (f) (at (g x)) o frechet_derivative g (at x)"
   if "g differentiable at x" "f differentiable at (g x)"
-  apply (rule frechet_derivative_at')
-  apply (rule diff_chain_at)
-   apply (rule frechet_derivative_worksI)
-  apply (rule that)
-  apply (rule frechet_derivative_worksI)
-  apply (rule that)
-  done
+  by (meson diff_chain_at frechet_derivative_at' frechet_derivative_works that)
 
 lemma frechet_derivative_compose_eucl:
   "frechet_derivative (f o g) (at x) =
     (\<lambda>v. \<Sum>i\<in>Basis. ((frechet_derivative g (at x) v) \<bullet> i) *\<^sub>R frechet_derivative f (at (g x)) i)"
   (is "?l = ?r")
   if "g differentiable at x" "f differentiable at (g x)"
 proof (rule ext)
   fix v
   interpret g: linear "frechet_derivative g (at x)"
     using that(1)
     by (rule linear_frechet_derivative)
   interpret f: linear "frechet_derivative f (at (g x))"
     using that(2)
     by (rule linear_frechet_derivative)
   have "frechet_derivative (f o g) (at x) v =
     frechet_derivative f (at (g x)) (\<Sum>i\<in>Basis. (frechet_derivative g (at x) v \<bullet> i) *\<^sub>R i)"
     unfolding frechet_derivative_compose[OF that] o_apply
     by (simp add: euclidean_representation)
   also have "\<dots> = ?r v"
     by (auto simp: g.sum g.scaleR f.sum f.scaleR)
   finally show "?l v = ?r v" .
 qed
 
 
 lemma frechet_derivative_works_on_open:
   "f differentiable_on X \<Longrightarrow> open X \<Longrightarrow> x \<in> X \<Longrightarrow>
     (f has_derivative frechet_derivative f (at x)) (at x)"
   and frechet_derivative_works_on:
   "f differentiable_on X \<Longrightarrow> x \<in> X \<Longrightarrow>
     (f has_derivative frechet_derivative f (at x within X)) (at x within X)"
   by (auto simp: differentiable_onD differentiable_on_openD frechet_derivative_worksI)
 
 lemma frechet_derivative_inverse: "frechet_derivative (\<lambda>x. inverse (f x)) (at x) =
     (\<lambda>h. - 1 / (f x)\<^sup>2 * frechet_derivative f (at x) h)"
   if "f differentiable at x" "f x \<noteq> 0" for f::"_\<Rightarrow>_::real_normed_field"
   apply (rule frechet_derivative_at')
   using that
   by (auto intro!: derivative_eq_intros frechet_derivative_worksI
       simp: divide_simps algebra_simps power2_eq_square)
 
 lemma frechet_derivative_sqrt: "frechet_derivative (\<lambda>x. sqrt (f x)) (at x) =
   (\<lambda>v. (if f x > 0 then 1 else -1) / (2 * sqrt (f x)) * frechet_derivative f (at x) v)"
   if "f differentiable at x" "f x \<noteq> 0" 
   apply (rule frechet_derivative_at')
   apply (rule sqrt_has_derivative[THEN has_derivative_eq_rhs])
   by (auto intro!: frechet_derivative_worksI that simp: divide_simps)
 
 lemma frechet_derivative_norm: "frechet_derivative (\<lambda>x. norm (f x)) (at x) =
     (\<lambda>v. frechet_derivative f (at x) v \<bullet> sgn (f x))"
   if "f differentiable at x" "f x \<noteq> 0" 
   for f::"_\<Rightarrow>_::real_inner"
   apply (rule frechet_derivative_at')
   by (auto intro!: derivative_eq_intros frechet_derivative_worksI that simp: divide_simps)
 
 lemma (in bounded_linear) frechet_derivative:
   "frechet_derivative f (at x) = f"
   apply (rule frechet_derivative_at')
   apply (rule has_derivative_eq_rhs)
    apply (rule has_derivative)
   by (auto intro!: derivative_eq_intros)
 
 bundle no_matrix_mult begin
 no_notation matrix_matrix_mult (infixl "**" 70)
 end
 
 lemma (in bounded_bilinear) frechet_derivative:
   includes no_matrix_mult
   shows
     "x differentiable at a \<Longrightarrow> y differentiable at a \<Longrightarrow>
       frechet_derivative (\<lambda>a. x a ** y a) (at a) =
         (\<lambda>h. x a ** frechet_derivative y (at a) h + frechet_derivative x (at a) h ** y a)"
   by (rule frechet_derivative_at') (auto intro!: FDERIV frechet_derivative_worksI)
 
 lemma frechet_derivative_divide: "frechet_derivative (\<lambda>x. f x / g x) (at x) =
     (\<lambda>h. frechet_derivative f (at x) h / (g x) -frechet_derivative g (at x) h * f x / (g x)\<^sup>2)"
   if "f differentiable at x" "g differentiable at x" "g x \<noteq> 0" for f::"_\<Rightarrow>_::real_normed_field"
   using that
   by (auto simp: divide_inverse_commute bounded_bilinear.frechet_derivative[OF bounded_bilinear_mult]
       frechet_derivative_inverse)
 
 lemma frechet_derivative_pair:
   "frechet_derivative (\<lambda>x. (f x, g x)) (at x) = (\<lambda>v. (frechet_derivative f (at x) v, frechet_derivative g (at x) v))"
   if "f differentiable (at x)" "g differentiable (at x)"
   apply (rule frechet_derivative_at')
   apply (rule derivative_eq_intros)
     apply (rule frechet_derivative_worksI) apply fact    
     apply (rule frechet_derivative_worksI) apply fact
   ..
 
 lemma frechet_derivative_fst:
   "frechet_derivative (\<lambda>x. fst (f x)) (at x) = (\<lambda>xa. fst (frechet_derivative f (at x) xa))"
   if "(f differentiable at x)"
   for f::"_\<Rightarrow>(_::real_normed_vector \<times> _::real_normed_vector)"
   apply (rule frechet_derivative_at')
   using that
   by (auto intro!: derivative_eq_intros frechet_derivative_worksI)
 
 lemma frechet_derivative_snd:
   "frechet_derivative (\<lambda>x. snd (f x)) (at x) = (\<lambda>xa. snd (frechet_derivative f (at x) xa))"
   if "(f differentiable at x)"
   for f::"_\<Rightarrow>(_::real_normed_vector \<times> _::real_normed_vector)"
   apply (rule frechet_derivative_at')
   using that
   by (auto intro!: derivative_eq_intros frechet_derivative_worksI)
 
 lemma frechet_derivative_eq_vector_derivative_1:
   assumes "f differentiable at t"
   shows "frechet_derivative f (at t) 1 = vector_derivative f (at t)"
   apply (subst frechet_derivative_eq_vector_derivative)
    apply (rule assms) by auto
 
 
 subsection \<open>Linear algebra\<close>
 
 lemma (in vector_space) dim_pos_finite_dimensional_vector_spaceE:
   assumes "dim (UNIV::'b set) > 0"
   obtains basis where "finite_dimensional_vector_space scale basis"
 proof -
   from assms obtain b where b: "local.span b = local.span UNIV" "local.independent b"
     by (auto simp: dim_def split: if_splits)
   then have "dim UNIV = card b"
     by (rule dim_eq_card)
   with assms have "finite b" by (auto simp: card_ge_0_finite)
   then have "finite_dimensional_vector_space scale b"
     by unfold_locales (auto simp: b)
   then show ?thesis ..
 qed
 
 context vector_space_on begin
 
 context includes lifting_syntax assumes "\<exists>(Rep::'s \<Rightarrow> 'b) (Abs::'b \<Rightarrow> 's). type_definition Rep Abs S" begin
 
 interpretation local_typedef_vector_space_on S scale "TYPE('s)" by unfold_locales fact
 
 lemmas_with [var_simplified explicit_ab_group_add,
     unoverload_type 'd,
     OF type.ab_group_add_axioms type_vector_space_on_with,
     folded dim_S_def,
     untransferred,
     var_simplified implicit_ab_group_add]:
     lt_dim_pos_finite_dimensional_vector_spaceE = vector_space.dim_pos_finite_dimensional_vector_spaceE
 
 end
 
 lemmas_with [cancel_type_definition,
     OF S_ne,
     folded subset_iff',
     simplified pred_fun_def, folded finite_dimensional_vector_space_on_with,
     simplified\<comment>\<open>too much?\<close>]:
     dim_pos_finite_dimensional_vector_spaceE = lt_dim_pos_finite_dimensional_vector_spaceE
 
 end
 
 
 subsection \<open>Extensional function space\<close>
 
 text \<open>f is zero outside A. We use such functions to canonically represent
   functions whose domain is A\<close>
 definition extensional0 :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::zero) \<Rightarrow> bool"
   where "extensional0 A f = (\<forall>x. x \<notin> A \<longrightarrow> f x = 0)"
 
 lemma extensional0_0[intro, simp]: "extensional0 X 0"
   by (auto simp: extensional0_def)
 
 lemma extensional0_UNIV[intro, simp]: "extensional0 UNIV f"
   by (auto simp: extensional0_def)
 
 lemma ext_extensional0:
   "f = g" if "extensional0 S f" "extensional0 S g" "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
   using that by (force simp: extensional0_def fun_eq_iff)
 
 lemma extensional0_add[intro, simp]:
   "extensional0 S f \<Longrightarrow> extensional0 S g \<Longrightarrow> extensional0 S (f + g::_\<Rightarrow>'a::comm_monoid_add)"
   by (auto simp: extensional0_def)
 
 lemma extensinoal0_mult[intro, simp]:
   "extensional0 S x \<Longrightarrow> extensional0 S y \<Longrightarrow> extensional0 S (x * y)"
   for x y::"_\<Rightarrow>'a::mult_zero"
   by (auto simp: extensional0_def)
 
 lemma extensional0_scaleR[intro, simp]: "extensional0 S f \<Longrightarrow> extensional0 S (c *\<^sub>R f::_\<Rightarrow>'a::real_vector)"
   by (auto simp: extensional0_def)
 
 lemma extensional0_outside: "x \<notin> S \<Longrightarrow> extensional0 S f \<Longrightarrow> f x = 0"
   by (auto simp: extensional0_def)
 
 lemma subspace_extensional0: "subspace (Collect (extensional0 X))"
   by (auto simp: subspace_def)
 
 text \<open>Send the function f to its canonical representative as a function with domain A\<close>
 definition restrict0 :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::zero) \<Rightarrow> 'a \<Rightarrow> 'b"
   where "restrict0 A f x = (if x \<in> A then f x else 0)"
 
 lemma restrict0_UNIV[simp]: "restrict0 UNIV = (\<lambda>x. x)"
   by (intro ext) (auto simp: restrict0_def)
 
 lemma extensional0_restrict0[intro, simp]: "extensional0 A (restrict0 A f)"
   by (auto simp: extensional0_def restrict0_def)
 
 lemma restrict0_times: "restrict0 A (x * y) = restrict0 A x * restrict0 A y"
   for x::"'a\<Rightarrow>'b::mult_zero"
   by (auto simp: restrict0_def[abs_def])
 
 lemma restrict0_apply_in[simp]: "x \<in> A \<Longrightarrow> restrict0 A f x = f x"
   by (auto simp: restrict0_def)
 
 lemma restrict0_apply_out[simp]: "x \<notin> A \<Longrightarrow> restrict0 A f x = 0"
   by (auto simp: restrict0_def)
 
 lemma restrict0_scaleR: "restrict0 A (c *\<^sub>R f::_\<Rightarrow>'a::real_vector) = c *\<^sub>R restrict0 A f"
   by (auto simp: restrict0_def[abs_def])
 
 lemma restrict0_add: "restrict0 A (f + g::_\<Rightarrow>'a::real_vector) = restrict0 A f + restrict0 A g"
   by (auto simp: restrict0_def[abs_def])
 
 lemma restrict0_restrict0: "restrict0 X (restrict0 Y f) = restrict0 (X \<inter> Y) f"
   by (auto simp: restrict0_def)
 
 end