# HG changeset patch
# User wenzelm
# Date 1675194275 -3600
# Node ID 1250a1f2bc1e13d8c84c588987bbc7b678ba7350
# Parent  1310df9229bd8af77f0f7db30d2d5e7b19090d6b# Parent  913c781ff6baff93825642f8f7fa49d07e5c401e
merged

diff -r 913c781ff6ba -r 1250a1f2bc1e src/Doc/Prog_Prove/document/intro-isabelle.tex
--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex	Tue Jan 31 20:44:35 2023 +0100
@@ -55,7 +55,6 @@
 \subsection*{Getting Started with Isabelle}
 
 If you have not done so already, download and install Isabelle
-(this book is compatible with Isabelle2020)
 from \url{https://isabelle.in.tum.de}. You can start it by clicking
 on the application icon. This will launch Isabelle's
 user interface based on the text editor \concept{jEdit}. Below you see
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -805,17 +805,15 @@
     using h unfolding ring_iso_def bij_betw_def inj_on_def by auto
 
   have h_inv_bij: "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)"
-      using bij_betw_inv_into h ring_iso_def by fastforce
+    by (simp add: bij_betw_inv_into h ring_iso_memE(5))
 
-  show "inv_into (carrier R) h \<in> ring_iso S R"
-    apply (rule ring_iso_memI)
-    apply (simp add: h_surj inv_into_into)
-       apply (auto simp add: h_inv_bij)
-    using ring_iso_memE [OF h] bij_betwE [OF h_inv_bij] 
-    apply (simp_all add: \<open>ring R\<close> bij_betw_def bij_betw_inv_into_right inv_into_f_eq ring.ring_simprules(5))
-    using ring_iso_memE [OF h] bij_betw_inv_into_right [of h "carrier R" "carrier S"]
-    apply (simp add: \<open>ring R\<close> inv_into_f_eq ring.ring_simprules(1))
-    by (simp add: \<open>ring R\<close> inv_into_f_eq ring.ring_simprules(6))
+  have "inv_into (carrier R) h \<in> ring_hom S R"
+    using ring_iso_memE [OF h] bij_betwE [OF h_inv_bij] \<open>ring R\<close>
+    by (simp add: bij_betw_imp_inj_on bij_betw_inv_into_right inv_into_f_eq ring.ring_simprules ring_hom_memI)
+  moreover have "bij_betw (inv_into (carrier R) h) (carrier S) (carrier R)"
+    using h_inv_bij by force
+    ultimately show "inv_into (carrier R) h \<in> ring_iso S R"
+      by (simp add: ring_iso_def)
 qed
 
 corollary ring_iso_sym:
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -318,12 +318,26 @@
 unfolding constant_on_def
 by (metis equals0I inj_on_contraD islimpt_UNIV islimpt_def)
 
+lemma constant_on_compose:
+  assumes "f constant_on A"
+  shows   "g \<circ> f constant_on A"
+  using assms by (auto simp: constant_on_def)
+
+lemma not_constant_onI:
+  "f x \<noteq> f y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> \<not>f constant_on A"
+  unfolding constant_on_def by metis
+
+lemma constant_onE:
+  assumes "f constant_on S" and "\<And>x. x\<in>S \<Longrightarrow> f x = g x"
+  shows "g constant_on S"
+  using assms unfolding constant_on_def by simp
+
 lemma constant_on_closureI:
   fixes f :: "_ \<Rightarrow> 'b::t1_space"
   assumes cof: "f constant_on S" and contf: "continuous_on (closure S) f"
-    shows "f constant_on (closure S)"
-using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
-by metis
+  shows "f constant_on (closure S)"
+  using continuous_constant_on_closure [OF contf] cof unfolding constant_on_def
+  by metis
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Continuity relative to a union.\<close>
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -2193,6 +2193,12 @@
     by (auto simp: Re_exp Im_exp)
 qed
 
+lemma Arg_1 [simp]: "Arg 1 = 0"
+  by (rule Arg_unique[of 1]) auto
+
+lemma Arg_numeral [simp]: "Arg (numeral n) = 0"
+  by (rule Arg_unique[of "numeral n"]) auto
+  
 lemma Arg_times_of_real [simp]:
   assumes "0 < r" shows "Arg (of_real r * z) = Arg z"
   using Arg_def Ln_times_of_real assms by auto
@@ -2207,6 +2213,10 @@
   using Im_Ln_le_pi Im_Ln_pos_le
   by (simp add: Arg_def)
 
+text \<open>converse fails because the argument can equal $\pi$.\<close> 
+lemma Arg_uminus: "Arg z < 0 \<Longrightarrow> Arg (-z) > 0"
+  by (smt (verit) Arg_bounded Arg_minus Complex.Arg_def)
+
 lemma Arg_eq_pi: "Arg z = pi \<longleftrightarrow> Re z < 0 \<and> Im z = 0"
   by (auto simp: Arg_def Im_Ln_eq_pi)
 
@@ -2261,7 +2271,13 @@
   by (metis Arg_cnj_eq_inverse Arg_inverse Reals_0 complex_cnj_zero)
 
 lemma Arg_exp: "-pi < Im z \<Longrightarrow> Im z \<le> pi \<Longrightarrow> Arg(exp z) = Im z"
-  by (rule Arg_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
+  by (simp add: Arg_eq_Im_Ln)
+
+lemma Arg_cis: "x \<in> {-pi<..pi} \<Longrightarrow> Arg (cis x) = x"
+  unfolding cis_conv_exp by (subst Arg_exp) auto
+
+lemma Arg_rcis: "x \<in> {-pi<..pi} \<Longrightarrow> r > 0 \<Longrightarrow> Arg (rcis r x) = x"
+  unfolding rcis_def by (subst Arg_times_of_real) (auto simp: Arg_cis)
 
 lemma Ln_Arg: "z\<noteq>0 \<Longrightarrow> Ln(z) = ln(norm z) + \<i> * Arg(z)"
   by (metis Arg_def Re_Ln complex_eq)
@@ -3093,6 +3109,33 @@
     by simp
 qed
 
+lemma csqrt_mult:
+  assumes "Arg z + Arg w \<in> {-pi<..pi}"
+  shows   "csqrt (z * w) = csqrt z * csqrt w"
+proof (cases "z = 0 \<or> w = 0")
+  case False
+  have "csqrt (z * w) = exp ((ln (z * w)) / 2)"
+    using False by (intro csqrt_exp_Ln) auto
+  also have "\<dots> = exp ((Ln z + Ln w) / 2)"
+    using False assms by (subst Ln_times_simple) (auto simp: Arg_eq_Im_Ln)
+  also have "(Ln z + Ln w) / 2 = Ln z / 2 + Ln w / 2"
+    by (simp add: add_divide_distrib)
+  also have "exp \<dots> = csqrt z * csqrt w"
+    using False by (simp add: exp_add csqrt_exp_Ln)
+  finally show ?thesis .
+qed auto
+
+lemma Arg_csqrt [simp]: "Arg (csqrt z) = Arg z / 2"
+proof (cases "z = 0")
+  case False
+  have "Im (Ln z) \<in> {-pi<..pi}"
+    by (simp add: False Im_Ln_le_pi mpi_less_Im_Ln)
+  also have "\<dots> \<subseteq> {-2*pi<..2*pi}"
+    by auto
+  finally show ?thesis
+    using False by (auto simp: csqrt_exp_Ln Arg_exp Arg_eq_Im_Ln)
+qed (auto simp: Arg_zero)
+
 lemma csqrt_inverse:
   "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt (inverse z) = inverse (csqrt z)"
   by (metis Ln_inverse csqrt_eq_0 csqrt_exp_Ln divide_minus_left exp_minus 
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -313,9 +313,13 @@
 lemma diff_chain_at[derivative_intros]:
   "(f has_derivative f') (at x) \<Longrightarrow>
     (g has_derivative g') (at (f x)) \<Longrightarrow> ((g \<circ> f) has_derivative (g' \<circ> f')) (at x)"
-  using has_derivative_compose[of f f' x UNIV g g']
-  by (simp add: comp_def)
-
+  by (meson diff_chain_within has_derivative_at_withinI)
+
+lemma has_vector_derivative_shift: "(f has_vector_derivative D x) (at x)
+           \<Longrightarrow> ((+) d \<circ> f has_vector_derivative D x) (at x)"
+  using diff_chain_at [OF _ shift_has_derivative_id]
+  by (simp add: has_derivative_iff_Ex has_vector_derivative_def) 
+  
 lemma has_vector_derivative_within_open:
   "a \<in> S \<Longrightarrow> open S \<Longrightarrow>
     (f has_vector_derivative f') (at a within S) \<longleftrightarrow> (f has_vector_derivative f') (at a)"
@@ -3311,7 +3315,16 @@
 
 lemma C1_differentiable_on_of_real [derivative_intros]: "of_real C1_differentiable_on S"
   unfolding C1_differentiable_on_def
-  by (smt (verit, del_insts) DERIV_ident UNIV_I continuous_on_const has_vector_derivative_of_real has_vector_derivative_transform)
+  using vector_derivative_works by fastforce
+
+lemma C1_differentiable_on_translation:
+  "f C1_differentiable_on U - S \<Longrightarrow> (+) d \<circ> f C1_differentiable_on U - S"
+  by (metis C1_differentiable_on_def has_vector_derivative_shift)
+
+lemma C1_differentiable_on_translation_eq: 
+  fixes d :: "'a::real_normed_vector"
+  shows "(+) d \<circ> f C1_differentiable_on i - S \<longleftrightarrow> f C1_differentiable_on i - S"
+  by (force simp: o_def intro: C1_differentiable_on_translation dest: C1_differentiable_on_translation [of concl: "-d"])
 
 
 definition\<^marker>\<open>tag important\<close> piecewise_C1_differentiable_on
@@ -3330,6 +3343,11 @@
            C1_differentiable_on_def differentiable_def has_vector_derivative_def
            intro: has_derivative_at_withinI)
 
+lemma piecewise_C1_differentiable_on_translation_eq:
+  "((+) d \<circ> f piecewise_C1_differentiable_on i) \<longleftrightarrow> (f piecewise_C1_differentiable_on i)"
+  unfolding piecewise_C1_differentiable_on_def continuous_on_translation_eq
+  by (metis C1_differentiable_on_translation_eq)
+
 lemma piecewise_C1_differentiable_compose [derivative_intros]:
   assumes fg: "f piecewise_C1_differentiable_on S" "g piecewise_C1_differentiable_on (f ` S)" and fin: "\<And>x. finite (S \<inter> f-`{x})"
   shows "(g \<circ> f) piecewise_C1_differentiable_on S"
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -370,6 +370,20 @@
     by (metis islimpt_approachable closed_limpt [where 'a='a])
 qed
 
+lemma discrete_imp_not_islimpt:
+  assumes e: "0 < e"
+    and d: "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> dist y x < e \<Longrightarrow> y = x"
+  shows "\<not> x islimpt S"
+proof
+  assume "x islimpt S"
+  hence "x islimpt S - {x}"
+    by (meson islimpt_punctured)
+  moreover from assms have "closed (S - {x})"
+    by (intro discrete_imp_closed) auto
+  ultimately show False
+    unfolding closed_limpt by blast
+qed
+  
 
 subsection \<open>Interior\<close>
 
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -13,7 +13,6 @@
   Product_Vector
 begin
 
-
 section \<open>Elementary Topology\<close>
 
 
@@ -845,6 +844,22 @@
   apply (auto simp: open_Int)
   done
 
+lemma open_imp_islimpt:
+  fixes x::"'a:: perfect_space"
+  assumes "open S" "x\<in>S"
+  shows "x islimpt S"
+  using assms interior_eq interior_limit_point by auto
+
+lemma islimpt_Int_eventually:
+  assumes "x islimpt A" "eventually (\<lambda>y. y \<in> B) (at x)"
+  shows   "x islimpt A \<inter> B"
+  using assms unfolding islimpt_def eventually_at_filter eventually_nhds
+  by (metis Int_iff UNIV_I open_Int)
+
+lemma islimpt_conv_frequently_at:
+  "x islimpt A \<longleftrightarrow> frequently (\<lambda>y. y \<in> A) (at x)"
+  unfolding islimpt_def eventually_at_filter frequently_def eventually_nhds by blast
+
 lemma interior_closed_Un_empty_interior:
   assumes cS: "closed S"
     and iT: "interior T = {}"
@@ -2435,6 +2450,16 @@
 lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f"
   by (force simp: homeomorphism_def)
 
+lemma continuous_on_translation_eq:
+  fixes g :: "'a :: real_normed_vector \<Rightarrow> 'b :: real_normed_vector"
+  shows "continuous_on A ((+) a \<circ> g) = continuous_on A g"
+proof -
+  have g: "g = (\<lambda>x. -a + x) \<circ> ((\<lambda>x. a + x) \<circ> g)"
+    by (rule ext) simp
+  show ?thesis
+    by (metis (no_types, opaque_lifting) g continuous_on_compose homeomorphism_def homeomorphism_translation)
+qed
+
 definition\<^marker>\<open>tag important\<close> homeomorphic :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
     (infixr "homeomorphic" 60)
   where "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Analysis/Line_Segment.thy
--- a/src/HOL/Analysis/Line_Segment.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Analysis/Line_Segment.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -914,15 +914,21 @@
   qed
 qed
 
+lemma closed_segment_same_fst:
+  "fst a = fst b \<Longrightarrow> closed_segment a b = {fst a} \<times> closed_segment (snd a) (snd b)"
+  by (auto simp: closed_segment_def scaleR_prod_def)
+
+lemma closed_segment_same_snd:
+  "snd a = snd b \<Longrightarrow> closed_segment a b = closed_segment (fst a) (fst b) \<times> {snd a}"
+  by (auto simp: closed_segment_def scaleR_prod_def)
+
 lemma subset_oc_segment:
   fixes a :: "'a::euclidean_space"
   shows "open_segment a b \<subseteq> closed_segment c d \<longleftrightarrow>
          a = b \<or> a \<in> closed_segment c d \<and> b \<in> closed_segment c d"
-apply (simp add: subset_open_segment [symmetric])
-apply (rule iffI)
- apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment subset_open_segment)
-apply (meson dual_order.trans segment_open_subset_closed)
-done
+  apply (rule iffI)
+   apply (metis closure_closed_segment closure_mono closure_open_segment subset_closed_segment)
+  by (meson dual_order.trans segment_open_subset_closed subset_open_segment)
 
 lemmas subset_segment = subset_closed_segment subset_co_segment subset_oc_segment subset_open_segment
 
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Analysis/Smooth_Paths.thy
--- a/src/HOL/Analysis/Smooth_Paths.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Analysis/Smooth_Paths.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -270,6 +270,9 @@
 lemma closed_valid_path_image: "valid_path g \<Longrightarrow> closed(path_image g)"
   by (metis closed_path_image valid_path_imp_path)
 
+lemma valid_path_translation_eq: "valid_path ((+)d \<circ> p) \<longleftrightarrow> valid_path p"
+  by (simp add: valid_path_def piecewise_C1_differentiable_on_translation_eq)
+ 
 lemma valid_path_compose:
   assumes "valid_path g"
       and der: "\<And>x. x \<in> path_image g \<Longrightarrow> f field_differentiable (at x)"
@@ -312,9 +315,8 @@
   ultimately have "f \<circ> g C1_differentiable_on {0..1} - S"
     using C1_differentiable_on_eq by blast
   moreover have "path (f \<circ> g)"
-    apply (rule path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]])
     using der
-    by (simp add: continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
+    by (simp add: path_continuous_image[OF valid_path_imp_path[OF \<open>valid_path g\<close>]] continuous_at_imp_continuous_on field_differentiable_imp_continuous_at)
   ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
     using \<open>finite S\<close> by auto
 qed
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/BNF_Cardinal_Order_Relation.thy
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -411,7 +411,7 @@
     card_of_Field_ordIso[of r] ordLeq_ordIso_trans by blast
 
 lemma card_of_Pow: "|A| <o |Pow A|"
-  using card_of_ordLess2[of "Pow A" A]  Cantors_paradox[of A]
+  using card_of_ordLess2[of "Pow A" A]  Cantors_theorem[of A]
     Pow_not_empty[of A] by auto
 
 corollary Card_order_Pow:
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Complex.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -214,8 +214,14 @@
   finally show ?thesis .
 qed
 
+lemma surj_Re: "surj Re"
+  by (metis Re_complex_of_real surj_def)
+
+lemma surj_Im: "surj Im"
+  by (metis complex.sel(2) surj_def)
+
 lemma complex_Im_fact [simp]: "Im (fact n) = 0"
-  by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat)
+  by (metis complex_Im_of_nat of_nat_fact)
 
 lemma Re_prod_Reals: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<real>) \<Longrightarrow> Re (prod f A) = prod (\<lambda>x. Re (f x)) A"
 proof (induction A rule: infinite_finite_induct)
@@ -279,6 +285,9 @@
 lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
   by (metis mult.commute power2_i power_mult)
 
+lemma i_even_power' [simp]: "even n \<Longrightarrow> \<i> ^ n = (-1) ^ (n div 2)"
+  by (metis dvd_mult_div_cancel power2_i power_mult)
+
 lemma Re_i_times [simp]: "Re (\<i> * z) = - Im z"
   by simp
 
@@ -521,6 +530,12 @@
 lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
   by (simp add: complex_eq_iff)
 
+lemma in_image_cnj_iff: "z \<in> cnj ` A \<longleftrightarrow> cnj z \<in> A"
+  by (metis complex_cnj_cnj image_iff)
+
+lemma image_cnj_conv_vimage_cnj: "cnj ` A = cnj -` A"
+  using in_image_cnj_iff by blast
+
 lemma complex_cnj_zero [simp]: "cnj 0 = 0"
   by (simp add: complex_eq_iff)
 
@@ -835,6 +850,15 @@
 lemma cis_divide: "cis a / cis b = cis (a - b)"
   by (simp add: divide_complex_def cis_mult)
 
+lemma divide_conv_cnj: "norm z = 1 \<Longrightarrow> x / z = x * cnj z"
+  by (metis complex_div_cnj div_by_1 mult_1 of_real_1 power2_eq_square)
+
+lemma i_not_in_Reals [simp, intro]: "\<i> \<notin> \<real>"
+  by (auto simp: complex_is_Real_iff)
+
+lemma powr_power_complex: "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> (z powr u :: complex) ^ n = z powr (of_nat n * u)"
+  by (induction n) (auto simp: algebra_simps powr_add)
+  
 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)"
   by (auto simp add: DeMoivre)
 
@@ -853,6 +877,11 @@
 lemma cis_multiple_2pi[simp]: "n \<in> \<int> \<Longrightarrow> cis (2 * pi * n) = 1"
   by (auto elim!: Ints_cases simp: cis.ctr one_complex.ctr)
 
+lemma minus_cis: "-cis x = cis (x + pi)"
+  by (simp flip: cis_mult)
+
+lemma minus_cis': "-cis x = cis (x - pi)"
+  by (simp flip: cis_divide)
 
 subsubsection \<open>$r(\cos \theta + i \sin \theta)$\<close>
 
@@ -1045,6 +1074,12 @@
     using pi_not_less_zero by linarith
 qed auto
 
+lemma cos_Arg: "z \<noteq> 0 \<Longrightarrow> cos (Arg z) = Re z / norm z"
+  by (metis Re_sgn cis.sel(1) cis_Arg)
+
+lemma sin_Arg: "z \<noteq> 0 \<Longrightarrow> sin (Arg z) = Im z / norm z"
+  by (metis Im_sgn cis.sel(2) cis_Arg)
+
 subsection \<open>Complex n-th roots\<close>
 
 lemma bij_betw_roots_unity:
@@ -1246,6 +1281,9 @@
         field_simps real_sqrt_mult[symmetric] real_sqrt_divide)
 qed
 
+lemma norm_csqrt [simp]: "norm (csqrt z) = sqrt (norm z)"
+  by (metis abs_of_nonneg norm_ge_zero norm_mult power2_csqrt power2_eq_square real_sqrt_abs)
+
 lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
   by auto (metis power2_csqrt power_eq_0_iff)
 
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Deriv.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -82,9 +82,12 @@
 lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
   by (simp add: has_derivative_def)
 
-lemma has_derivative_id [derivative_intros, simp]: "(id has_derivative id) (at a)"
+lemma has_derivative_id [derivative_intros, simp]: "(id has_derivative id) F"
   by (metis eq_id_iff has_derivative_ident)
 
+lemma shift_has_derivative_id: "((+) d has_derivative (\<lambda>x. x)) F"
+  using has_derivative_def by fastforce
+
 lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
   by (simp add: has_derivative_def)
 
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Filter.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -65,6 +65,9 @@
 lemma eventuallyI: "(\<And>x. P x) \<Longrightarrow> eventually P F"
   by (auto intro: always_eventually)
 
+lemma filter_eqI: "(\<And>P. eventually P F \<longleftrightarrow> eventually P G) \<Longrightarrow> F = G"
+  by (auto simp: filter_eq_iff)
+
 lemma eventually_mono:
   "\<lbrakk>eventually P F; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> eventually Q F"
   unfolding eventually_def
@@ -105,6 +108,11 @@
   shows "eventually (\<lambda>i. R i) F"
   using assms by (auto elim!: eventually_rev_mp)
 
+lemma eventually_cong:
+  assumes "eventually P F" and "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
+  shows   "eventually Q F \<longleftrightarrow> eventually R F"
+  using assms eventually_elim2 by blast
+
 lemma eventually_ball_finite_distrib:
   "finite A \<Longrightarrow> (eventually (\<lambda>x. \<forall>y\<in>A. P x y) net) \<longleftrightarrow> (\<forall>y\<in>A. eventually (\<lambda>x. P x y) net)"
   by (induction A rule: finite_induct) (auto simp: eventually_conj_iff)
@@ -209,6 +217,12 @@
   "(\<exists>\<^sub>Fx in F. P x \<longrightarrow> Q x) \<longleftrightarrow> (eventually P F \<longrightarrow> frequently Q F)"
   unfolding imp_conv_disj frequently_disj_iff not_eventually[symmetric] ..
 
+lemma frequently_eventually_conj:
+  assumes "\<exists>\<^sub>Fx in F. P x"
+  assumes "\<forall>\<^sub>Fx in F. Q x"
+  shows "\<exists>\<^sub>Fx in F. Q x \<and> P x"
+  using assms eventually_elim2 by (force simp add: frequently_def)
+
 lemma eventually_frequently_const_simps:
   "(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
   "(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
@@ -557,6 +571,13 @@
   apply (auto elim!: eventually_rev_mp)
   done
 
+lemma eventually_comp_filtermap:
+    "eventually (P \<circ> f) F \<longleftrightarrow> eventually P (filtermap f F)"
+  unfolding comp_def using eventually_filtermap by auto
+
+lemma filtermap_compose: "filtermap (f \<circ> g) F = filtermap f (filtermap g F)"
+  unfolding filter_eq_iff by (simp add: eventually_filtermap)
+
 lemma filtermap_ident: "filtermap (\<lambda>x. x) F = F"
   by (simp add: filter_eq_iff eventually_filtermap)
 
@@ -585,6 +606,16 @@
 lemma filtermap_INF: "filtermap f (\<Sqinter>b\<in>B. F b) \<le> (\<Sqinter>b\<in>B. filtermap f (F b))"
   by (rule INF_greatest, rule filtermap_mono, erule INF_lower)
 
+lemma frequently_cong:
+  assumes ev: "eventually P F" and QR: "\<And>x. P x \<Longrightarrow> Q x \<longleftrightarrow> R x"
+  shows   "frequently Q F \<longleftrightarrow> frequently R F"
+  unfolding frequently_def 
+  using QR by (auto intro!: eventually_cong [OF ev])
+
+lemma frequently_filtermap:
+  "frequently P (filtermap f F) = frequently (\<lambda>x. P (f x)) F"
+  by (simp add: frequently_def eventually_filtermap)
+
 
 subsubsection \<open>Contravariant map function for filters\<close>
 
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Fun.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -353,6 +353,17 @@
 lemma inj_on_imp_bij_betw: "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
   unfolding bij_betw_def by simp
 
+lemma bij_betw_DiffI:
+  assumes "bij_betw f A B" "bij_betw f C D" "C \<subseteq> A" "D \<subseteq> B"
+  shows   "bij_betw f (A - C) (B - D)"
+  using assms unfolding bij_betw_def inj_on_def by auto
+
+lemma bij_betw_singleton_iff [simp]: "bij_betw f {x} {y} \<longleftrightarrow> f x = y"
+  by (auto simp: bij_betw_def)
+
+lemma bij_betw_singletonI [intro]: "f x = y \<Longrightarrow> bij_betw f {x} {y}"
+  by auto
+
 lemma bij_betw_apply: "\<lbrakk>bij_betw f A B; a \<in> A\<rbrakk> \<Longrightarrow> f a \<in> B"
   unfolding bij_betw_def by auto
 
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -72,7 +72,7 @@
 lemma countable_infiniteE':
   assumes "countable A" "infinite A"
   obtains g where "bij_betw g (UNIV :: nat set) A"
-  using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast
+  by (meson assms bij_betw_inv countableE_infinite)
 
 lemma countable_enum_cases:
   assumes "countable S"
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Library/Equipollence.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -186,7 +186,7 @@
 
 lemma lesspoll_Pow_self: "A \<prec> Pow A"
   unfolding lesspoll_def bij_betw_def eqpoll_def
-  by (meson lepoll_Pow_self Cantors_paradox)
+  by (meson lepoll_Pow_self Cantors_theorem)
 
 lemma finite_lesspoll_infinite:
   assumes "infinite A" "finite B" shows "B \<prec> A"
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Library/Product_Order.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -35,6 +35,9 @@
 lemma Pair_le [simp]: "(a, b) \<le> (c, d) \<longleftrightarrow> a \<le> c \<and> b \<le> d"
   unfolding less_eq_prod_def by simp
 
+lemma atLeastAtMost_prod_eq: "{a..b} = {fst a..fst b} \<times> {snd a..snd b}"
+  by (auto simp: less_eq_prod_def)
+
 instance prod :: (preorder, preorder) preorder
 proof
   fix x y z :: "'a \<times> 'b"
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Power.thy
--- a/src/HOL/Power.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Power.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -89,6 +89,9 @@
 lemma power4_eq_xxxx: "x^4 = x * x * x * x"
   by (simp add: mult.assoc power_numeral_even)
 
+lemma power_numeral_reduce: "x ^ numeral n = x * x ^ pred_numeral n"
+  by (simp add: numeral_eq_Suc)
+
 lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)"
 proof (induct "f x" arbitrary: f)
   case 0
@@ -654,9 +657,18 @@
 lemma of_nat_power_less_of_nat_cancel_iff[simp]: "of_nat x < (of_nat b) ^ w \<longleftrightarrow> x < b ^ w"
   by (metis of_nat_less_iff of_nat_power)
 
+lemma power2_nonneg_ge_1_iff: 
+  assumes "x \<ge> 0"
+  shows   "x ^ 2 \<ge> 1 \<longleftrightarrow> x \<ge> 1"
+  using assms by (auto intro: power2_le_imp_le)
+
+lemma power2_nonneg_gt_1_iff: 
+  assumes "x \<ge> 0"
+  shows   "x ^ 2 > 1 \<longleftrightarrow> x > 1"
+  using assms  by (auto intro: power_less_imp_less_base)
+
 end
 
-
 text \<open>Some @{typ nat}-specific lemmas:\<close>
 
 lemma mono_ge2_power_minus_self:
@@ -822,12 +834,14 @@
 
 end
 
-
 subsection \<open>Miscellaneous rules\<close>
 
 lemma (in linordered_semidom) self_le_power: "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
   using power_increasing [of 1 n a] power_one_right [of a] by auto
 
+lemma power2_ge_1_iff: "x ^ 2 \<ge> 1 \<longleftrightarrow> x \<ge> 1 \<or> x \<le> (-1 :: 'a :: linordered_idom)"
+  using abs_le_square_iff[of 1 x] by (auto simp: abs_if split: if_splits)
+
 lemma (in power) power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
   unfolding One_nat_def by (cases m) simp_all
 
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -159,6 +159,11 @@
     by simp
 qed
 
+lemma shift_zero_ident [simp]:
+  fixes f :: "'a \<Rightarrow> 'b::real_vector"
+  shows "(+)0 \<circ> f = f"
+  by force
+  
 lemma linear_scale_real:
   fixes r::real shows "linear f \<Longrightarrow> f (r * b) = r * f b"
   using linear_scale by fastforce
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Set.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -952,7 +952,7 @@
 lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
   by auto
 
-theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
+theorem Cantors_theorem: "\<nexists>f. f ` A = Pow A"
 proof
   assume "\<exists>f. f ` A = Pow A"
   then obtain f where f: "f ` A = Pow A" ..
@@ -1363,7 +1363,7 @@
 lemma Diff_Int2: "A \<inter> C - B \<inter> C = A \<inter> C - B"
   by blast
 
-lemma subset_UnE: 
+lemma subset_UnE:
   assumes "C \<subseteq> A \<union> B"
   obtains A' B' where "A' \<subseteq> A" "B' \<subseteq> B" "C = A' \<union> B'"
 proof
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -535,6 +535,16 @@
   "eventually P (at a within s) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> x \<in> s \<longrightarrow> P x))"
   by (simp add: eventually_nhds eventually_at_filter)
 
+lemma eventually_at_in_open:
+  assumes "open A" "x \<in> A"
+  shows   "eventually (\<lambda>y. y \<in> A - {x}) (at x)"
+  using assms eventually_at_topological by blast
+
+lemma eventually_at_in_open':
+  assumes "open A" "x \<in> A"
+  shows   "eventually (\<lambda>y. y \<in> A) (at x)"
+  using assms eventually_at_topological by blast
+
 lemma (in topological_space) at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
   unfolding filter_eq_iff eventually_at_topological by (metis open_Int Int_iff UNIV_I)
 
@@ -569,6 +579,10 @@
   unfolding trivial_limit_def eventually_at_topological
   by (metis UNIV_I empty_iff is_singletonE is_singletonI' singleton_iff)
 
+lemma (in t1_space) eventually_neq_at_within:
+  "eventually (\<lambda>w. w \<noteq> x) (at z within A)"
+  by (smt (verit, ccfv_threshold) eventually_True eventually_at_topological separation_t1)
+
 lemma (in perfect_space) at_neq_bot [simp]: "at a \<noteq> bot"
   by (simp add: at_eq_bot_iff not_open_singleton)
 
@@ -706,6 +720,24 @@
   using linordered_field_no_lb[rule_format, of x]
   by (auto simp: eventually_at_left)
 
+lemma filtermap_nhds_eq_imp_filtermap_at_eq: 
+  assumes "filtermap f (nhds z) = nhds (f z)"
+  assumes "eventually (\<lambda>x. f x = f z \<longrightarrow> x = z) (at z)"
+  shows   "filtermap f (at z) = at (f z)"
+proof (rule filter_eqI)
+  fix P :: "'a \<Rightarrow> bool"
+  have "eventually P (filtermap f (at z)) \<longleftrightarrow> (\<forall>\<^sub>F x in nhds z. x \<noteq> z \<longrightarrow> P (f x))"
+    by (simp add: eventually_filtermap eventually_at_filter)
+  also have "\<dots> \<longleftrightarrow> (\<forall>\<^sub>F x in nhds z. f x \<noteq> f z \<longrightarrow> P (f x))"
+    by (rule eventually_cong [OF assms(2)[unfolded eventually_at_filter]]) auto
+  also have "\<dots> \<longleftrightarrow> (\<forall>\<^sub>F x in filtermap f (nhds z). x \<noteq> f z \<longrightarrow> P x)"
+    by (simp add: eventually_filtermap)
+  also have "filtermap f (nhds z) = nhds (f z)"
+    by (rule assms)
+  also have "(\<forall>\<^sub>F x in nhds (f z). x \<noteq> f z \<longrightarrow> P x) \<longleftrightarrow> (\<forall>\<^sub>F x in at (f z). P x)"
+    by (simp add: eventually_at_filter)
+  finally show "eventually P (filtermap f (at z)) = eventually P (at (f z))" .
+qed
 
 subsubsection \<open>Tendsto\<close>
 
@@ -1789,6 +1821,29 @@
     by (metis (no_types) f filterlim_compose filterlim_filtermap g tendsto_at_iff_tendsto_nhds tendsto_compose_filtermap)
 qed
 
+lemma tendsto_nhds_iff: "(f \<longlongrightarrow> (c :: 'a :: t1_space)) (nhds x) \<longleftrightarrow> f \<midarrow>x\<rightarrow> c \<and> f x = c"
+proof safe
+  assume lim: "(f \<longlongrightarrow> c) (nhds x)"
+  show "f x = c"
+  proof (rule ccontr)
+    assume "f x \<noteq> c"
+    hence "c \<noteq> f x"
+      by auto
+    then obtain A where A: "open A" "c \<in> A" "f x \<notin> A"
+      by (subst (asm) separation_t1) auto
+    with lim obtain B where "open B" "x \<in> B" "\<And>x. x \<in> B \<Longrightarrow> f x \<in> A"
+      unfolding tendsto_def eventually_nhds by metis 
+    with \<open>f x \<notin> A\<close> show False
+      by blast
+  qed
+  show "(f \<longlongrightarrow> c) (at x)"
+    using lim by (rule filterlim_mono) (auto simp: at_within_def)
+next
+  assume "f \<midarrow>x\<rightarrow> f x" "c = f x"
+  thus "(f \<longlongrightarrow> f x) (nhds x)"
+    unfolding tendsto_def eventually_at_filter by (fast elim: eventually_mono)
+qed
+
 
 subsubsection \<open>Relation of \<open>LIM\<close> and \<open>LIMSEQ\<close>\<close>
 
@@ -2275,20 +2330,35 @@
   "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
   using continuous_at_imp_continuous_at_within continuous_within_compose2 by blast
 
-lemma filtermap_nhds_open_map:
+lemma filtermap_nhds_open_map':
   assumes cont: "isCont f a"
-    and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
+    and "open A" "a \<in> A"
+    and open_map: "\<And>S. open S \<Longrightarrow> S \<subseteq> A \<Longrightarrow> open (f ` S)"
   shows "filtermap f (nhds a) = nhds (f a)"
   unfolding filter_eq_iff
 proof safe
   fix P
   assume "eventually P (filtermap f (nhds a))"
-  then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. P (f x)"
+  then obtain S where S: "open S" "a \<in> S" "\<forall>x\<in>S. P (f x)"
     by (auto simp: eventually_filtermap eventually_nhds)
-  then show "eventually P (nhds (f a))"
-    unfolding eventually_nhds by (intro exI[of _ "f`S"]) (auto intro!: open_map)
+  show "eventually P (nhds (f a))"
+    unfolding eventually_nhds 
+  proof (rule exI [of _ "f ` (A \<inter> S)"], safe)
+    show "open (f ` (A \<inter> S))"
+      using S by (intro open_Int assms) auto
+    show "f a \<in> f ` (A \<inter> S)"
+      using assms S by auto
+    show "P (f x)" if "x \<in> A" "x \<in> S" for x
+      using S that by auto
+  qed
 qed (metis filterlim_iff tendsto_at_iff_tendsto_nhds isCont_def eventually_filtermap cont)
 
+lemma filtermap_nhds_open_map:
+  assumes cont: "isCont f a"
+    and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"
+  shows "filtermap f (nhds a) = nhds (f a)"
+  using cont filtermap_nhds_open_map' open_map by blast
+
 lemma continuous_at_split:
   "continuous (at x) f \<longleftrightarrow> continuous (at_left x) f \<and> continuous (at_right x) f"
   for x :: "'a::linorder_topology"
diff -r 913c781ff6ba -r 1250a1f2bc1e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jan 31 20:37:46 2023 +0100
+++ b/src/HOL/Transcendental.thy	Tue Jan 31 20:44:35 2023 +0100
@@ -1531,6 +1531,28 @@
   qed
 qed simp
 
+lemma exp_power_int:
+  fixes  x :: "'a::{real_normed_field,banach}"
+  shows "exp x powi n = exp (of_int n * x)"
+proof (cases "n \<ge> 0")
+  case True
+  have "exp x powi n = exp x ^ nat n"
+    using True by (simp add: power_int_def)
+  thus ?thesis
+    using True by (subst (asm) exp_of_nat_mult [symmetric]) auto
+next
+  case False
+  have "exp x powi n = inverse (exp x ^ nat (-n))"
+    using False by (simp add: power_int_def field_simps)
+  also have "exp x ^ nat (-n) = exp (of_nat (nat (-n)) * x)"
+    using False by (subst exp_of_nat_mult) auto
+  also have "inverse \<dots> = exp (-(of_nat (nat (-n)) * x))"
+    by (subst exp_minus) (auto simp: field_simps)
+  also have "-(of_nat (nat (-n)) * x) = of_int n * x"
+    using False by simp
+  finally show ?thesis .
+qed
+
 
 subsubsection \<open>Properties of the Exponential Function on Reals\<close>
 
@@ -1928,9 +1950,9 @@
 proof -
   have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n + 2))) \<le> x\<^sup>2"
   proof -
-    have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
+    have "(\<lambda>n. x\<^sup>2 / 2 * (1/2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1/2)))"
       by (intro sums_mult geometric_sums) simp
-    then have sumsx: "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums x\<^sup>2"
+    then have sumsx: "(\<lambda>n. x\<^sup>2 / 2 * (1/2) ^ n) sums x\<^sup>2"
       by simp
     have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n + 2))) \<le> suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
     proof (intro suminf_le allI)
@@ -1953,7 +1975,7 @@
       qed
       show "summable (\<lambda>n. inverse (fact (n + 2)) * x ^ (n + 2))"
         by (rule summable_exp [THEN summable_ignore_initial_segment])
-      show "summable (\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n)"
+      show "summable (\<lambda>n. x\<^sup>2 / 2 * (1/2) ^ n)"
         by (rule sums_summable [OF sumsx])
     qed
     also have "\<dots> = x\<^sup>2"
@@ -2066,7 +2088,7 @@
 
 lemma ln_one_minus_pos_lower_bound:
   fixes x :: real
-  assumes a: "0 \<le> x" and b: "x \<le> 1 / 2"
+  assumes a: "0 \<le> x" and b: "x \<le> 1/2"
   shows "- x - 2 * x\<^sup>2 \<le> ln (1 - x)"
 proof -
   from b have c: "x < 1" by auto
@@ -2120,7 +2142,7 @@
 
 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
   fixes x :: real
-  assumes a: "-(1 / 2) \<le> x" and b: "x \<le> 0"
+  assumes a: "-(1/2) \<le> x" and b: "x \<le> 0"
   shows "\<bar>ln (1 + x) - x\<bar> \<le> 2 * x\<^sup>2"
 proof -
   have *: "- (-x) - 2 * (-x)\<^sup>2 \<le> ln (1 - (- x))"
@@ -2134,7 +2156,7 @@
 
 lemma abs_ln_one_plus_x_minus_x_bound:
   fixes x :: real
-  assumes "\<bar>x\<bar> \<le> 1 / 2"
+  assumes "\<bar>x\<bar> \<le> 1/2"
   shows "\<bar>ln (1 + x) - x\<bar> \<le> 2 * x\<^sup>2"
 proof (cases "0 \<le> x")
   case True
@@ -2493,6 +2515,9 @@
 lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
   by (induction n) (simp_all add: ac_simps powr_add)
 
+lemma powr_realpow': "(z :: real) \<ge> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> z powr of_nat n = z ^ n"
+  by (cases "z = 0") (auto simp: powr_realpow)
+
 lemma powr_real_of_int':
   assumes "x \<ge> 0" "x \<noteq> 0 \<or> n > 0"
   shows   "x powr real_of_int n = power_int x n"
@@ -3532,9 +3557,10 @@
 
 lemma cos_minus [simp]: "cos (-x) = cos x"
   for x :: "'a::{real_normed_algebra_1,banach}"
-  using cos_minus_converges [of x]
-  by (simp add: cos_def summable_norm_cos [THEN summable_norm_cancel]
-      suminf_minus sums_iff equation_minus_iff)
+  using cos_minus_converges [of x] by (metis cos_def sums_unique)
+
+lemma cos_abs_real [simp]: "cos \<bar>x :: real\<bar> = cos x"
+  by (simp add: abs_if)
 
 lemma sin_cos_squared_add [simp]: "(sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
   for x :: "'a::{real_normed_field,banach}"
@@ -4009,12 +4035,12 @@
 
 lemma sin_pi_divide_n_ge_0 [simp]:
   assumes "n \<noteq> 0"
-  shows "0 \<le> sin (pi / real n)"
+  shows "0 \<le> sin (pi/real n)"
   by (rule sin_ge_zero) (use assms in \<open>simp_all add: field_split_simps\<close>)
 
 lemma sin_pi_divide_n_gt_0:
   assumes "2 \<le> n"
-  shows "0 < sin (pi / real n)"
+  shows "0 < sin (pi/real n)"
   by (rule sin_gt_zero) (use assms in \<open>simp_all add: field_split_simps\<close>)
 
 text\<open>Proof resembles that of \<open>cos_is_zero\<close> but with \<^term>\<open>pi\<close> for the upper bound\<close>
@@ -4101,7 +4127,7 @@
 proof -
   obtain n where "odd n" and n: "x + pi/2 = of_nat n * (pi/2)" "n > 0"
     using cos_zero_lemma [of "x + pi/2"] assms by (auto simp add: cos_add)
-  then have "x = real (n - 1) * (pi / 2)"
+  then have "x = real (n - 1) * (pi/2)"
     by (simp add: algebra_simps of_nat_diff)
   then show ?thesis
     by (simp add: \<open>odd n\<close>)
@@ -4182,9 +4208,9 @@
 
 lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>i::int. x = of_int i * pi)"
 proof -
-  have "sin x = 0 \<longleftrightarrow> (\<exists>i. even i \<and> x = real_of_int i * (pi / 2))"
+  have "sin x = 0 \<longleftrightarrow> (\<exists>i. even i \<and> x = real_of_int i * (pi/2))"
     by (auto simp: sin_zero_iff_int)
-  also have "... = (\<exists>j. x = real_of_int (2*j) * (pi / 2))"
+  also have "... = (\<exists>j. x = real_of_int (2*j) * (pi/2))"
     using dvd_triv_left by blast
   also have "... = (\<exists>i::int. x = of_int i * pi)"
     by auto
@@ -4421,15 +4447,15 @@
   finally show ?thesis .
 qed
 
-lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
-proof -
-  let ?c = "cos (pi / 4)"
-  let ?s = "sin (pi / 4)"
+lemma cos_45: "cos (pi/4) = sqrt 2 / 2"
+proof -
+  let ?c = "cos (pi/4)"
+  let ?s = "sin (pi/4)"
   have nonneg: "0 \<le> ?c"
     by (simp add: cos_ge_zero)
-  have "0 = cos (pi / 4 + pi / 4)"
+  have "0 = cos (pi/4 + pi/4)"
     by simp
-  also have "cos (pi / 4 + pi / 4) = ?c\<^sup>2 - ?s\<^sup>2"
+  also have "cos (pi/4 + pi/4) = ?c\<^sup>2 - ?s\<^sup>2"
     by (simp only: cos_add power2_eq_square)
   also have "\<dots> = 2 * ?c\<^sup>2 - 1"
     by (simp add: sin_squared_eq)
@@ -4439,13 +4465,13 @@
     using nonneg by (rule power2_eq_imp_eq) simp
 qed
 
-lemma cos_30: "cos (pi / 6) = sqrt 3/2"
-proof -
-  let ?c = "cos (pi / 6)"
-  let ?s = "sin (pi / 6)"
+lemma cos_30: "cos (pi/6) = sqrt 3/2"
+proof -
+  let ?c = "cos (pi/6)"
+  let ?s = "sin (pi/6)"
   have pos_c: "0 < ?c"
     by (rule cos_gt_zero) simp_all
-  have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
+  have "0 = cos (pi/6 + pi/6 + pi/6)"
     by simp
   also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
     by (simp only: cos_add sin_add)
@@ -4458,23 +4484,34 @@
     by (rule power2_eq_imp_eq) simp
 qed
 
-lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
+lemma sin_45: "sin (pi/4) = sqrt 2 / 2"
   by (simp add: sin_cos_eq cos_45)
 
-lemma sin_60: "sin (pi / 3) = sqrt 3/2"
+lemma sin_60: "sin (pi/3) = sqrt 3/2"
   by (simp add: sin_cos_eq cos_30)
 
-lemma cos_60: "cos (pi / 3) = 1 / 2"
-proof -
-  have "0 \<le> cos (pi / 3)"
+lemma cos_60: "cos (pi/3) = 1/2"
+proof -
+  have "0 \<le> cos (pi/3)"
     by (rule cos_ge_zero) (use pi_half_ge_zero in \<open>linarith+\<close>)
   then show ?thesis
     by (simp add: cos_squared_eq sin_60 power_divide power2_eq_imp_eq)
 qed
 
-lemma sin_30: "sin (pi / 6) = 1 / 2"
+lemma sin_30: "sin (pi/6) = 1/2"
   by (simp add: sin_cos_eq cos_60)
 
+lemma cos_120: "cos (2 * pi/3) = -1/2"
+  and sin_120: "sin (2 * pi/3) = sqrt 3 / 2"
+  using sin_double[of "pi/3"] cos_double[of "pi/3"]
+  by (simp_all add: power2_eq_square sin_60 cos_60)
+
+lemma cos_120': "cos (pi * 2 / 3) = -1/2"
+  using cos_120 by (subst mult.commute)
+
+lemma sin_120': "sin (pi * 2 / 3) = sqrt 3 / 2"
+  using sin_120 by (subst mult.commute)
+
 lemma cos_integer_2pi: "n \<in> \<int> \<Longrightarrow> cos(2 * pi * n) = 1"
   by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute)
 
@@ -4563,13 +4600,13 @@
   unfolding tan_def sin_double cos_double sin_squared_eq
   by (simp add: power2_eq_square)
 
-lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
+lemma tan_30: "tan (pi/6) = 1 / sqrt 3"
   unfolding tan_def by (simp add: sin_30 cos_30)
 
-lemma tan_45: "tan (pi / 4) = 1"
+lemma tan_45: "tan (pi/4) = 1"
   unfolding tan_def by (simp add: sin_45 cos_45)
 
-lemma tan_60: "tan (pi / 3) = sqrt 3"
+lemma tan_60: "tan (pi/3) = sqrt 3"
   unfolding tan_def by (simp add: sin_60 cos_60)
 
 lemma DERIV_tan [simp]: "cos x \<noteq> 0 \<Longrightarrow> DERIV tan x :> inverse ((cos x)\<^sup>2)"
@@ -4667,7 +4704,7 @@
     by (meson less_le_trans minus_pi_half_less_zero tan_total_pos)
 next
   case ge
-  with tan_total_pos [of "-y"] obtain x where "0 \<le> x" "x < pi / 2" "tan x = - y"
+  with tan_total_pos [of "-y"] obtain x where "0 \<le> x" "x < pi/2" "tan x = - y"
     by force
   then show ?thesis
     by (rule_tac x="-x" in exI) auto
@@ -4675,7 +4712,7 @@
 
 proposition tan_total: "\<exists>! x. -(pi/2) < x \<and> x < (pi/2) \<and> tan x = y"
 proof -
-  have "u = v" if u: "- (pi / 2) < u" "u < pi / 2" and v: "- (pi / 2) < v" "v < pi / 2"
+  have "u = v" if u: "- (pi/2) < u" "u < pi/2" and v: "- (pi/2) < v" "v < pi/2"
     and eq: "tan u = tan v" for u v
   proof (cases u v rule: linorder_cases)
     case less
@@ -4706,8 +4743,8 @@
     ultimately show ?thesis
       using DERIV_unique [OF _ DERIV_tan] by fastforce
   qed auto
-  then have "\<exists>!x. - (pi / 2) < x \<and> x < pi / 2 \<and> tan x = y" 
-    if x: "- (pi / 2) < x" "x < pi / 2" "tan x = y" for x
+  then have "\<exists>!x. - (pi/2) < x \<and> x < pi/2 \<and> tan x = y" 
+    if x: "- (pi/2) < x" "x < pi/2" "tan x = y" for x
     using that by auto
   then show ?thesis
     using lemma_tan_total1 [where y = y]
@@ -4984,6 +5021,10 @@
   unfolding arcsin_def
   using the1_equality [OF sin_total]  by simp
 
+lemma arcsin_unique:
+  assumes "-pi/2 \<le> x" and "x \<le> pi/2" and "sin x = y" shows "arcsin y = x"
+  using arcsin_sin[of x] assms by force
+
 lemma arcsin_0 [simp]: "arcsin 0 = 0"
   using arcsin_sin [of 0] by simp
 
@@ -4996,6 +5037,13 @@
 lemma arcsin_minus: "- 1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin (- x) = - arcsin x"
   by (metis (no_types, opaque_lifting) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus)
 
+lemma arcsin_one_half [simp]: "arcsin (1/2) = pi / 6"
+  and arcsin_minus_one_half [simp]: "arcsin (-(1/2)) = -pi / 6"
+  by (intro arcsin_unique; simp add: sin_30 field_simps)+
+  
+lemma arcsin_one_over_sqrt_2: "arcsin (1 / sqrt 2) = pi / 4"
+  by (rule arcsin_unique) (auto simp: sin_45 field_simps)
+
 lemma arcsin_eq_iff: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arcsin x = arcsin y \<longleftrightarrow> x = y"
   by (metis abs_le_iff arcsin minus_le_iff)
 
@@ -5036,6 +5084,10 @@
 lemma arccos_cos2: "x \<le> 0 \<Longrightarrow> - pi \<le> x \<Longrightarrow> arccos (cos x) = -x"
   by (auto simp: arccos_def intro!: the1_equality cos_total)
 
+lemma arccos_unique:
+  assumes "0 \<le> x" and "x \<le> pi" and "cos x = y" shows "arccos y = x"
+  using arccos_cos assms by blast
+
 lemma cos_arcsin:
   assumes "- 1 \<le> x" "x \<le> 1"
   shows "cos (arcsin x) = sqrt (1 - x\<^sup>2)"
@@ -5061,8 +5113,7 @@
 qed
 
 lemma arccos_0 [simp]: "arccos 0 = pi/2"
-  by (metis arccos_cos cos_gt_zero cos_pi cos_pi_half pi_gt_zero
-      pi_half_ge_zero not_le not_zero_less_neg_numeral numeral_One)
+  using arccos_cos pi_half_ge_zero by fastforce
 
 lemma arccos_1 [simp]: "arccos 1 = 0"
   using arccos_cos by force
@@ -5071,8 +5122,14 @@
   by (metis arccos_cos cos_pi order_refl pi_ge_zero)
 
 lemma arccos_minus: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos (- x) = pi - arccos x"
-  by (metis arccos_cos arccos_cos2 cos_minus_pi cos_total diff_le_0_iff_le le_add_same_cancel1
-      minus_diff_eq uminus_add_conv_diff)
+  by (smt (verit, ccfv_threshold) arccos arccos_cos cos_minus cos_minus_pi)
+
+lemma arccos_one_half [simp]: "arccos (1/2) = pi / 3"
+  and arccos_minus_one_half [simp]: "arccos (-(1/2)) = 2 * pi / 3"
+  by (intro arccos_unique; simp add: cos_60 cos_120)+
+
+lemma arccos_one_over_sqrt_2: "arccos (1 / sqrt 2) = pi / 4"
+  by (rule arccos_unique) (auto simp: cos_45 field_simps)
 
 corollary arccos_minus_abs:
   assumes "\<bar>x\<bar> \<le> 1"
@@ -5211,9 +5268,9 @@
 
 lemma isCont_arctan: "isCont arctan x"
 proof -
-  obtain u where u: "- (pi / 2) < u" "u < arctan x"
+  obtain u where u: "- (pi/2) < u" "u < arctan x"
     by (meson arctan arctan_less_iff linordered_field_no_lb)
-  obtain v where v: "arctan x < v" "v < pi / 2"
+  obtain v where v: "arctan x < v" "v < pi/2"
     by (meson arctan_less_iff arctan_ubound linordered_field_no_ub)
   have "isCont arctan (tan (arctan x))"
   proof (rule isCont_inverse_function2 [of u "arctan x" v])
@@ -5442,6 +5499,9 @@
 lemma arcsin_le_arcsin: "- 1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y"
   using arcsin_le_mono by auto
 
+lemma arcsin_nonneg: "x \<in> {0..1} \<Longrightarrow> arcsin x \<ge> 0"
+  using arcsin_le_arcsin[of 0 x] by simp
+  
 lemma arccos_less_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arccos x < arccos y \<longleftrightarrow> y < x"
   by (rule trans [OF cos_mono_less_eq [symmetric]]) (use arccos_ubound arccos_lbound in auto)
 
@@ -5490,15 +5550,15 @@
 proof -
   have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0"
   proof (rule sin_eq_0_pi)
-    show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)"
+    show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi/2 - arccos x)"
       using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
       by (simp add: algebra_simps)
   next
-    show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi"
+    show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi/2 - arccos x) < pi"
       using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
       by (simp add: algebra_simps)
   next
-    show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0"
+    show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi/2 - arccos x)) = 0"
       using assms
       by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
                     power2_eq_square square_eq_1_iff)
@@ -5574,14 +5634,14 @@
 
 subsection \<open>Machin's formula\<close>
 
-lemma arctan_one: "arctan 1 = pi / 4"
+lemma arctan_one: "arctan 1 = pi/4"
   by (rule arctan_unique) (simp_all add: tan_45 m2pi_less_pi)
 
 lemma tan_total_pi4:
   assumes "\<bar>x\<bar> < 1"
-  shows "\<exists>z. - (pi / 4) < z \<and> z < pi / 4 \<and> tan z = x"
+  shows "\<exists>z. - (pi/4) < z \<and> z < pi/4 \<and> tan z = x"
 proof
-  show "- (pi / 4) < arctan x \<and> arctan x < pi / 4 \<and> tan (arctan x) = x"
+  show "- (pi/4) < arctan x \<and> arctan x < pi/4 \<and> tan (arctan x) = x"
     unfolding arctan_one [symmetric] arctan_minus [symmetric]
     unfolding arctan_less_iff
     using assms by (auto simp: arctan)
@@ -5591,13 +5651,13 @@
   assumes "\<bar>x\<bar> \<le> 1" "\<bar>y\<bar> < 1"
   shows "arctan x + arctan y = arctan ((x + y) / (1 - x * y))"
 proof (rule arctan_unique [symmetric])
-  have "- (pi / 4) \<le> arctan x" "- (pi / 4) < arctan y"
+  have "- (pi/4) \<le> arctan x" "- (pi/4) < arctan y"
     unfolding arctan_one [symmetric] arctan_minus [symmetric]
     unfolding arctan_le_iff arctan_less_iff
     using assms by auto
   from add_le_less_mono [OF this] show 1: "- (pi/2) < arctan x + arctan y"
     by simp
-  have "arctan x \<le> pi / 4" "arctan y < pi / 4"
+  have "arctan x \<le> pi/4" "arctan y < pi/4"
     unfolding arctan_one [symmetric]
     unfolding arctan_le_iff arctan_less_iff
     using assms by auto
@@ -5610,7 +5670,7 @@
 lemma arctan_double: "\<bar>x\<bar> < 1 \<Longrightarrow> 2 * arctan x = arctan ((2 * x) / (1 - x\<^sup>2))"
   by (metis arctan_add linear mult_2 not_less power2_eq_square)
 
-theorem machin: "pi / 4 = 4 * arctan (1 / 5) - arctan (1 / 239)"
+theorem machin: "pi/4 = 4 * arctan (1 / 5) - arctan (1/239)"
 proof -
   have "\<bar>1 / 5\<bar> < (1 :: real)"
     by auto
@@ -5622,17 +5682,17 @@
   from arctan_add[OF less_imp_le[OF this] this] have "2 * arctan (5 / 12) = arctan (120 / 119)"
     by auto
   moreover
-  have "\<bar>1\<bar> \<le> (1::real)" and "\<bar>1 / 239\<bar> < (1::real)"
+  have "\<bar>1\<bar> \<le> (1::real)" and "\<bar>1/239\<bar> < (1::real)"
     by auto
-  from arctan_add[OF this] have "arctan 1 + arctan (1 / 239) = arctan (120 / 119)"
+  from arctan_add[OF this] have "arctan 1 + arctan (1/239) = arctan (120 / 119)"
     by auto
-  ultimately have "arctan 1 + arctan (1 / 239) = 4 * arctan (1 / 5)"
+  ultimately have "arctan 1 + arctan (1/239) = 4 * arctan (1 / 5)"
     by auto
   then show ?thesis
     unfolding arctan_one by algebra
 qed
 
-lemma machin_Euler: "5 * arctan (1 / 7) + 2 * arctan (3 / 79) = pi / 4"
+lemma machin_Euler: "5 * arctan (1 / 7) + 2 * arctan (3 / 79) = pi/4"
 proof -
   have 17: "\<bar>1 / 7\<bar> < (1 :: real)" by auto
   with arctan_double have "2 * arctan (1 / 7) = arctan (7 / 24)"
@@ -6007,11 +6067,11 @@
 
       have c_minus_minus: "?c (- 1) i = - ?c 1 i" for i by auto
 
-      have "arctan (- 1) = arctan (tan (-(pi / 4)))"
+      have "arctan (- 1) = arctan (tan (-(pi/4)))"
         unfolding tan_45 tan_minus ..
-      also have "\<dots> = - (pi / 4)"
+      also have "\<dots> = - (pi/4)"
         by (rule arctan_tan) (auto simp: order_less_trans[OF \<open>- (pi/2) < 0\<close> pi_gt_zero])
-      also have "\<dots> = - (arctan (tan (pi / 4)))"
+      also have "\<dots> = - (arctan (tan (pi/4)))"
         unfolding neg_equal_iff_equal
         by (rule arctan_tan[symmetric]) (auto simp: order_less_trans[OF \<open>- (2 * pi) < 0\<close> pi_gt_zero])
       also have "\<dots> = - (arctan 1)"
@@ -6089,10 +6149,10 @@
     by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
 qed
 
-theorem pi_series: "pi / 4 = (\<Sum>k. (-1)^k * 1 / real (k * 2 + 1))"
+theorem pi_series: "pi/4 = (\<Sum>k. (-1)^k * 1 / real (k * 2 + 1))"
   (is "_ = ?SUM")
 proof -
-  have "pi / 4 = arctan 1"
+  have "pi/4 = arctan 1"
     using arctan_one by auto
   also have "\<dots> = ?SUM"
     using arctan_series[of 1] by auto
@@ -6597,7 +6657,7 @@
 
 lemma sinh_plus_cosh: "sinh x + cosh x = exp x"
 proof -
-  have "sinh x + cosh x = (1 / 2) *\<^sub>R (exp x + exp x)"
+  have "sinh x + cosh x = (1/2) *\<^sub>R (exp x + exp x)"
     by (simp add: sinh_def cosh_def algebra_simps)
   also have "\<dots> = exp x" by (rule scaleR_half_double)
   finally show ?thesis .
@@ -6608,7 +6668,7 @@
 
 lemma cosh_minus_sinh: "cosh x - sinh x = exp (-x)"
 proof -
-  have "cosh x - sinh x = (1 / 2) *\<^sub>R (exp (-x) + exp (-x))"
+  have "cosh x - sinh x = (1/2) *\<^sub>R (exp (-x) + exp (-x))"
     by (simp add: sinh_def cosh_def algebra_simps)
   also have "\<dots> = exp (-x)" by (rule scaleR_half_double)
   finally show ?thesis .
@@ -6895,10 +6955,10 @@
 proof -
   have *: "((\<lambda>x. - exp (- x)) \<longlongrightarrow> (-0::real)) at_top"
     by (intro tendsto_minus filterlim_compose[OF exp_at_bot] filterlim_uminus_at_bot_at_top)
-  have "filterlim (\<lambda>x. (1 / 2) * (-exp (-x) + exp x) :: real) at_top at_top"
+  have "filterlim (\<lambda>x. (1/2) * (-exp (-x) + exp x) :: real) at_top at_top"
     by (rule filterlim_tendsto_pos_mult_at_top[OF _ _
                filterlim_tendsto_add_at_top[OF *]] tendsto_const)+ (auto simp: exp_at_top)
-  also have "(\<lambda>x. (1 / 2) * (-exp (-x) + exp x) :: real) = sinh"
+  also have "(\<lambda>x. (1/2) * (-exp (-x) + exp x) :: real) = sinh"
     by (simp add: fun_eq_iff sinh_def)
   finally show ?thesis .
 qed
@@ -6915,10 +6975,10 @@
 proof -
   have *: "((\<lambda>x. exp (- x)) \<longlongrightarrow> (0::real)) at_top"
     by (intro filterlim_compose[OF exp_at_bot] filterlim_uminus_at_bot_at_top)
-  have "filterlim (\<lambda>x. (1 / 2) * (exp (-x) + exp x) :: real) at_top at_top"
+  have "filterlim (\<lambda>x. (1/2) * (exp (-x) + exp x) :: real) at_top at_top"
     by (rule filterlim_tendsto_pos_mult_at_top[OF _ _
                filterlim_tendsto_add_at_top[OF *]] tendsto_const)+ (auto simp: exp_at_top)
-  also have "(\<lambda>x. (1 / 2) * (exp (-x) + exp x) :: real) = cosh"
+  also have "(\<lambda>x. (1/2) * (exp (-x) + exp x) :: real) = cosh"
     by (simp add: fun_eq_iff cosh_def)
   finally show ?thesis .
 qed