# HG changeset patch
# User paulson
# Date 1672352065 0
# Node ID 8a17349143df036db561f28b5333ea46ce6f5c17
# Parent  947510ce4e36fce5d5f74cc8e2dd473661f672cc# Parent  25c0d4c0e1105cfeb42bc47b7c819ecde5fc4fc3
merged

diff -r 947510ce4e36 -r 8a17349143df src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Dec 29 16:44:45 2022 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Dec 29 22:14:25 2022 +0000
@@ -660,15 +660,10 @@
 
 lemma norm_sin_squared:
   "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
-proof (cases z)
-  case (Complex x1 x2)
-  then show ?thesis
-    apply (simp only: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq)
-    apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
-    apply (simp only: left_diff_distrib [symmetric] power_mult_distrib cos_squared_eq)
-    apply (simp add: power2_eq_square field_split_simps)
-    done
-qed
+  using cos_double_sin [of "Re z"]
+  apply (simp add: sin_cos_eq norm_cos_squared exp_minus mult.commute [of _ 2] exp_double)
+  apply (simp add: algebra_simps power2_eq_square)
+  done
 
 lemma exp_uminus_Im: "exp (- Im z) \<le> exp (cmod z)"
   using abs_Im_le_cmod linear order_trans by fastforce
@@ -1002,17 +997,14 @@
 
 lemma Arg2pi_times_of_real [simp]:
   assumes "0 < r" shows "Arg2pi (of_real r * z) = Arg2pi z"
-proof (cases "z=0")
-  case False
-  show ?thesis
-    by (rule Arg2pi_unique [of "r * norm z"]) (use Arg2pi False assms is_Arg_def in auto)
-qed auto
+  by (metis (no_types, lifting) Arg2pi Arg2pi_eq Arg2pi_unique assms mult.assoc 
+      mult_eq_0_iff mult_pos_pos of_real_mult zero_less_norm_iff)
 
 lemma Arg2pi_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg2pi (z * of_real r) = Arg2pi z"
   by (metis Arg2pi_times_of_real mult.commute)
 
 lemma Arg2pi_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg2pi (z / of_real r) = Arg2pi z"
-  by (metis Arg2pi_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
+  by (metis Arg2pi_times_of_real2 less_irrefl nonzero_eq_divide_eq of_real_eq_0_iff)
 
 lemma Arg2pi_le_pi: "Arg2pi z \<le> pi \<longleftrightarrow> 0 \<le> Im z"
 proof (cases "z=0")
@@ -1095,12 +1087,14 @@
 
 lemma Arg2pi_eq_iff:
   assumes "w \<noteq> 0" "z \<noteq> 0"
-     shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)"
-  using assms Arg2pi_eq [of z] Arg2pi_eq [of w]
-  apply auto
-  apply (rule_tac x="norm w / norm z" in exI)
-  apply (simp add: field_split_simps)
-  by (metis mult.commute mult.left_commute)
+  shows "Arg2pi w = Arg2pi z \<longleftrightarrow> (\<exists>x. 0 < x & w = of_real x * z)" (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then have "(cmod w) * (z / cmod z) = w"
+    by (metis Arg2pi_eq assms(2) mult_eq_0_iff nonzero_mult_div_cancel_left)
+  then show ?rhs
+    by (metis assms divide_pos_pos of_real_divide times_divide_eq_left times_divide_eq_right zero_less_norm_iff)
+qed auto
 
 lemma Arg2pi_inverse_eq_0: "Arg2pi(inverse z) = 0 \<longleftrightarrow> Arg2pi z = 0"
   by (metis Arg2pi_eq_0 Arg2pi_inverse inverse_inverse_eq)
@@ -1142,19 +1136,20 @@
   using Arg2pi_add [OF assms]
   by auto
 
-lemma Arg2pi_cnj_eq_inverse: "z\<noteq>0 \<Longrightarrow> Arg2pi (cnj z) = Arg2pi (inverse z)"
-  apply (simp add: Arg2pi_eq_iff field_split_simps complex_norm_square [symmetric])
-  by (metis of_real_power zero_less_norm_iff zero_less_power)
+lemma Arg2pi_cnj_eq_inverse:
+  assumes "z \<noteq> 0" shows "Arg2pi (cnj z) = Arg2pi (inverse z)"
+proof -
+  have "\<exists>r>0. of_real r / z = cnj z"
+    by (metis assms complex_norm_square nonzero_mult_div_cancel_left zero_less_norm_iff zero_less_power)
+  then show ?thesis
+    by (metis Arg2pi_times_of_real2 divide_inverse_commute)
+qed
 
 lemma Arg2pi_cnj: "Arg2pi(cnj z) = (if z \<in> \<real> then Arg2pi z else 2*pi - Arg2pi z)"
-proof (cases "z=0")
-  case False
-  then show ?thesis
-    by (simp add: Arg2pi_cnj_eq_inverse Arg2pi_inverse)
-qed auto
+  by (metis Arg2pi_cnj_eq_inverse Arg2pi_inverse Reals_cnj_iff complex_cnj_zero)
 
 lemma Arg2pi_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg2pi(exp z) = Im z"
-  by (rule Arg2pi_unique [of "exp(Re z)"]) (auto simp: exp_eq_polar)
+  by (simp add: Arg2pi_unique exp_eq_polar)
 
 lemma complex_split_polar:
   obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
@@ -2215,21 +2210,13 @@
 
 lemma Arg_times_of_real [simp]:
   assumes "0 < r" shows "Arg (of_real r * z) = Arg z"
-proof (cases "z=0")
-  case True
-  then show ?thesis
-    by (simp add: Arg_def)
-next
-  case False
-  with Arg_eq assms show ?thesis
-  by (auto simp: mpi_less_Arg Arg_le_pi intro!:  Arg_unique [of "r * norm z"])
-qed
+  using Arg_def Ln_times_of_real assms by auto
 
 lemma Arg_times_of_real2 [simp]: "0 < r \<Longrightarrow> Arg (z * of_real r) = Arg z"
   by (metis Arg_times_of_real mult.commute)
 
 lemma Arg_divide_of_real [simp]: "0 < r \<Longrightarrow> Arg (z / of_real r) = Arg z"
-  by (metis Arg_times_of_real2 less_numeral_extra(3) nonzero_eq_divide_eq of_real_eq_0_iff)
+  by (metis Arg_times_of_real2 less_irrefl nonzero_eq_divide_eq of_real_eq_0_iff)
 
 lemma Arg_less_0: "0 \<le> Arg z \<longleftrightarrow> 0 \<le> Im z"
   using Im_Ln_le_pi Im_Ln_pos_le
@@ -2243,18 +2230,13 @@
   by (auto simp: order.order_iff_strict Arg_def)
 
 lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
-  using complex_is_Real_iff
-  by (simp add: Arg_def Im_Ln_eq_0) (metis less_eq_real_def of_real_Re of_real_def scale_zero_left)
+  using Arg_def Im_Ln_eq_0 complex_eq_iff complex_is_Real_iff by auto
 
 corollary\<^marker>\<open>tag unimportant\<close> Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
   using assms by (auto simp: nonneg_Reals_def Arg_eq_0)
 
 lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
-proof (cases "z=0")
-  case False
-  then show ?thesis
-    using Arg_eq_0 [of "-z"] Arg_eq_pi complex_is_Real_iff by blast
-qed (simp add: Arg_def)
+  using Arg_eq_pi complex_is_Real_iff by blast
 
 lemma Arg_eq_0_pi: "Arg z = 0 \<or> Arg z = pi \<longleftrightarrow> z \<in> \<real>"
   using Arg_eq_pi_iff Arg_eq_0 by force
@@ -2266,15 +2248,11 @@
 proof (cases "z \<in> \<real>")
   case True
   then show ?thesis
-    by simp (metis Arg2pi_inverse Arg2pi_real Arg_real Reals_inverse)
+    by (metis Arg2pi_inverse Arg2pi_real Arg_real Reals_inverse)
 next
   case False
-  then have z: "Arg z < pi" "z \<noteq> 0"
-    using Arg_eq_0_pi Arg_le_pi by (auto simp: less_eq_real_def)
-  show ?thesis
-    apply (rule Arg_unique [of "inverse (norm z)"])
-    using False z mpi_less_Arg [of z] Arg_eq [of z]
-    by (auto simp: exp_minus field_simps)
+  then show ?thesis
+    by (simp add: Arg_def Ln_inverse complex_is_Real_iff complex_nonpos_Reals_iff)
 qed
 
 lemma Arg_eq_iff:
@@ -2282,7 +2260,7 @@
   shows "Arg w = Arg z \<longleftrightarrow> (\<exists>x. 0 < x \<and> w = of_real x * z)" (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  then have "w = complex_of_real (cmod w / cmod z) * z"
+  then have "w = (cmod w / cmod z) * z"
     by (metis Arg_eq assms divide_divide_eq_right eq_divide_eq exp_not_eq_zero of_real_divide)
   then show ?rhs
     using assms divide_pos_pos zero_less_norm_iff by blast
@@ -2307,14 +2285,11 @@
   assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
     shows "continuous (at z) Arg"
 proof -
-  have [simp]: "(\<lambda>z. Im (Ln z)) \<midarrow>z\<rightarrow> Arg z"
+  have "(\<lambda>z. Im (Ln z)) \<midarrow>z\<rightarrow> Arg z"
     using Arg_def assms continuous_at by fastforce
-  show ?thesis
+  then show ?thesis
     unfolding continuous_at
-  proof (rule Lim_transform_within_open)
-    show "\<And>w. \<lbrakk>w \<in> - \<real>\<^sub>\<le>\<^sub>0; w \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln w) = Arg w"
-      by (metis Arg_def Compl_iff nonpos_Reals_zero_I)
-  qed (use assms in auto)
+    by (smt (verit, del_insts) Arg_eq_Im_Ln Lim_transform_away_at assms nonpos_Reals_zero_I)
 qed
 
 lemma continuous_within_Arg: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Arg"
@@ -2388,44 +2363,17 @@
   qed
 next
   show "arctan (Im z / Re z) > -pi"
-    by (rule le_less_trans[OF _ arctan_lbound]) auto
+    by (smt (verit, ccfv_SIG) arctan field_sum_of_halves)
 next
-  have "arctan (Im z / Re z) < pi / 2"
-    by (rule arctan_ubound)
-  also have "\<dots> \<le> pi" by simp
-  finally show "arctan (Im z / Re z) \<le> pi"
-    by simp
+ show "arctan (Im z / Re z) \<le> pi"
+   by (smt (verit, best) arctan field_sum_of_halves)
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
 
-lemma Arg2pi_Ln:
-  assumes "0 < Arg2pi z" shows "Arg2pi z = Im(Ln(-z)) + pi"
-proof (cases "z = 0")
-  case True
-  with assms show ?thesis
-    by simp
-next
-  case False
-  then have "z / of_real(norm z) = exp(\<i> * of_real(Arg2pi z))"
-    using Arg2pi [of z]
-    by (metis is_Arg_def abs_norm_cancel nonzero_mult_div_cancel_left norm_of_real zero_less_norm_iff)
-  then have "- z / of_real(norm z) = exp (\<i> * (of_real (Arg2pi z) - pi))"
-    using cis_conv_exp cis_pi
-    by (auto simp: exp_diff algebra_simps)
-  then have "ln (- z / of_real(norm z)) = ln (exp (\<i> * (of_real (Arg2pi z) - pi)))"
-    by simp
-  also have "\<dots> = \<i> * (of_real(Arg2pi z) - pi)"
-    using Arg2pi [of z] assms pi_not_less_zero
-    by auto
-  finally have "Arg2pi z =  Im (Ln (- z / of_real (cmod z))) + pi"
-    by simp
-  also have "\<dots> = Im (Ln (-z) - ln (cmod z)) + pi"
-    by (metis diff_0_right minus_diff_eq zero_less_norm_iff Ln_divide_of_real False)
-  also have "\<dots> = Im (Ln (-z)) + pi"
-    by simp
-  finally show ?thesis .
-qed
+lemma Arg2pi_Ln: "0 < Arg2pi z \<Longrightarrow> Arg2pi z = Im(Ln(-z)) + pi"
+  by (smt (verit, best) Arg2pi_0 Arg2pi_exp Arg2pi_minus Arg_exp Arg_minus Im_Ln_le_pi 
+      exp_Ln mpi_less_Im_Ln neg_equal_0_iff_equal)
 
 lemma continuous_at_Arg2pi:
   assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
@@ -2433,18 +2381,14 @@
 proof -
   have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
     by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
-  have [simp]: "Im x \<noteq> 0 \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x" for x
-    using Arg2pi_Ln  by (simp add: Arg2pi_gt_0 complex_nonneg_Reals_iff)
   consider "Re z < 0" | "Im z \<noteq> 0" using assms
     using complex_nonneg_Reals_iff not_le by blast
-  then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
+  then have "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg2pi z"
     using "*" by (simp add: Arg2pi_Ln Arg2pi_gt_0 assms continuous_within)
-  show ?thesis
+  then show ?thesis
     unfolding continuous_at
-  proof (rule Lim_transform_within_open)
-    show "\<And>x. \<lbrakk>x \<in> - \<real>\<^sub>\<ge>\<^sub>0; x \<noteq> z\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg2pi x"
-      by (auto simp add: Arg2pi_Ln [OF Arg2pi_gt_0] complex_nonneg_Reals_iff)
-  qed (use assms in auto)
+    by (metis (mono_tags, lifting) Arg2pi_Ln Arg2pi_gt_0 Compl_iff Lim_transform_within_open assms 
+        closed_nonneg_Reals_complex open_Compl)
 qed
 
 
@@ -2467,18 +2411,7 @@
 lemma Arg2pi_eq_Im_Ln:
   assumes "0 \<le> Im z" "0 < Re z"
     shows "Arg2pi z = Im (Ln z)"
-proof (cases "Im z = 0")
-  case True then show ?thesis
-    using Arg2pi_eq_0 Ln_in_Reals assms(2) complex_is_Real_iff by auto
-next
-  case False
-  then have *: "Arg2pi z > 0"
-    using Arg2pi_gt_0 complex_is_Real_iff by blast
-  then have "z \<noteq> 0"
-    by auto
-  with * assms False show ?thesis
-    by (subst Arg2pi_Ln) (auto simp: Ln_minus)
-qed
+  by (smt (verit, ccfv_SIG) Arg2pi_exp Im_Ln_pos_le assms exp_Ln pi_neq_zero zero_complex.simps(1))
 
 lemma continuous_within_upperhalf_Arg2pi:
   assumes "z \<noteq> 0"
@@ -2681,9 +2614,7 @@
     also have "\<dots> \<longleftrightarrow> ((\<lambda>z. g z ^ nat n) has_field_derivative dd') (at z within S)"
     proof (rule has_field_derivative_cong_eventually)
       show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = g x ^ nat n"
-        unfolding eventually_at
-        apply (rule exI[where x=e])
-        using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute)
+        unfolding eventually_at by (metis e_dist \<open>e>0\<close> dist_commute powr_of_int that)
     qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
     also have "\<dots>" unfolding dd'_def using gderiv that
       by (auto intro!: derivative_eq_intros)
@@ -2707,8 +2638,7 @@
     proof (rule has_field_derivative_cong_eventually)
       show "\<forall>\<^sub>F x in at z within S. g x powr of_int n = inverse (g x ^ nat (- n))"
          unfolding eventually_at
-        apply (rule exI[where x=e])
-        using powr_of_int that \<open>e>0\<close> e_dist by (simp add: dist_commute)
+         by (metis \<open>e>0\<close> e_dist dist_commute linorder_not_le powr_of_int that)
     qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
     also have "\<dots>"
     proof -
@@ -2759,8 +2689,8 @@
 using field_differentiable_def has_field_derivative_powr_right by blast
 
 lemma holomorphic_on_powr_right [holomorphic_intros]:
-  assumes "f holomorphic_on s"
-  shows "(\<lambda>z. w powr (f z)) holomorphic_on s"
+  assumes "f holomorphic_on S"
+  shows "(\<lambda>z. w powr (f z)) holomorphic_on S"
 proof (cases "w = 0")
   case False
   with assms show ?thesis
@@ -2769,21 +2699,9 @@
 qed simp
 
 lemma holomorphic_on_divide_gen [holomorphic_intros]:
-  assumes f: "f holomorphic_on s" and g: "g holomorphic_on s" and 0: "\<And>z z'. \<lbrakk>z \<in> s; z' \<in> s\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0"
-shows "(\<lambda>z. f z / g z) holomorphic_on s"
-proof (cases "\<exists>z\<in>s. g z = 0")
-  case True
-  with 0 have "g z = 0" if "z \<in> s" for z
-    using that by blast
-  then show ?thesis
-    using g holomorphic_transform by auto
-next
-  case False
-  with 0 have "g z \<noteq> 0" if "z \<in> s" for z
-    using that by blast
-  with holomorphic_on_divide show ?thesis
-    using f g by blast
-qed
+  assumes "f holomorphic_on S" "g holomorphic_on S" and "\<And>z z'. \<lbrakk>z \<in> S; z' \<in> S\<rbrakk> \<Longrightarrow> g z = 0 \<longleftrightarrow> g z' = 0"
+  shows "(\<lambda>z. f z / g z) holomorphic_on S"
+  by (metis (no_types, lifting) assms division_ring_divide_zero holomorphic_on_divide holomorphic_transform)
 
 lemma norm_powr_real_powr:
   "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
@@ -2879,6 +2797,7 @@
 lemma tendsto_neg_powr_complex_of_nat:
   assumes "filterlim f at_top F" and "Re s < 0"
   shows   "((\<lambda>x. of_nat (f x) powr s) \<longlongrightarrow> 0) F"
+  using tendsto_neg_powr_complex_of_real [of "real o f" F s]
 proof -
   have "((\<lambda>x. of_real (real (f x)) powr s) \<longlongrightarrow> 0) F" using assms(2)
     by (intro filterlim_compose[OF _ tendsto_neg_powr_complex_of_real]
@@ -3093,29 +3012,18 @@
   also have "\<dots> = exp (Ln z / 2)"
     apply (rule csqrt_square)
     using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms
-    by (fastforce simp: Re_exp Im_exp )
+    by (fastforce simp: Re_exp Im_exp)
   finally show ?thesis using assms csqrt_square
     by simp
 qed
 
 lemma csqrt_inverse:
-  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
-    shows "csqrt (inverse z) = inverse (csqrt z)"
-proof (cases "z=0")
-  case False
-  then show ?thesis
-    using assms csqrt_exp_Ln Ln_inverse exp_minus
-    by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
-qed auto
-
-lemma cnj_csqrt:
-  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
-    shows "cnj(csqrt z) = csqrt(cnj z)"
-proof (cases "z=0")
-  case False
-  then show ?thesis
-     by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj)
-qed auto
+  "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 
+      inverse_nonzero_iff_nonzero)
+
+lemma cnj_csqrt: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> cnj(csqrt z) = csqrt(cnj z)"
+  by (metis cnj_Ln complex_cnj_divide complex_cnj_numeral complex_cnj_zero_iff csqrt_eq_0 csqrt_exp_Ln exp_cnj)
 
 lemma has_field_derivative_csqrt:
   assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
@@ -3175,8 +3083,8 @@
     "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
 proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
   case True
-  have [simp]: "Im z = 0" and 0: "Re z < 0 \<or> z = 0"
-    using True cnj.code complex_cnj_zero_iff  by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce
+  then have [simp]: "Im z = 0" and 0: "Re z < 0 \<or> z = 0"
+    using complex_nonpos_Reals_iff complex_eq_iff by force+
   show ?thesis
     using 0
   proof
@@ -3296,11 +3204,7 @@
   have nzi: "((1 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0"
     using nz1 nz2 by auto
   have "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))"
-    apply (simp add: divide_complex_def)
-    apply (simp add: divide_simps split: if_split_asm)
-    using assms
-    apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
-    done
+    by (simp add: Im_complex_div_lemma Re_complex_div_lemma assms cmod_eq_Im)
   then have *: "((1 - \<i>*z) / (1 + \<i>*z)) \<notin> \<real>\<^sub>\<le>\<^sub>0"
     by (auto simp add: complex_nonpos_Reals_iff)
   show "\<bar>Re(Arctan z)\<bar> < pi/2"
@@ -3483,7 +3387,7 @@
   also have "\<dots> = x"
   proof -
     have "(complex_of_real x)\<^sup>2 \<noteq> - 1"
-      by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one)
+      by (smt (verit, best) Im_complex_of_real imaginary_unit.sel(2) of_real_minus power2_eq_iff power2_i)
     then show ?thesis
       by simp
   qed
@@ -3526,22 +3430,8 @@
 qed
 
 lemma arctan_inverse:
-  assumes "0 < x"
-    shows "arctan(inverse x) = pi/2 - arctan x"
-proof -
-  have "arctan(inverse x) = arctan(inverse(tan(arctan x)))"
-    by (simp add: arctan)
-  also have "\<dots> = arctan (tan (pi / 2 - arctan x))"
-    by (simp add: tan_cot)
-  also have "\<dots> = pi/2 - arctan x"
-  proof -
-    have "0 < pi - arctan x"
-    using arctan_ubound [of x] pi_gt_zero by linarith
-    with assms show ?thesis
-      by (simp add: Transcendental.arctan_tan)
-  qed
-  finally show ?thesis .
-qed
+  "0 < x \<Longrightarrow>arctan(inverse x) = pi/2 - arctan x"
+  by (smt (verit, del_insts) arctan arctan_unique tan_cot zero_less_arctan_iff)
 
 lemma arctan_add_small:
   assumes "\<bar>x * y\<bar> < 1"
@@ -3590,7 +3480,7 @@
     show "(\<lambda>k. 1 / real (k * 2 + 1) * x ^ (k * 2 + 1)) \<longlonglongrightarrow> 0 * 0"
       using assms
       by (intro tendsto_mult real_tendsto_divide_at_top)
-        (auto simp: filterlim_real_sequentially filterlim_sequentially_iff_filterlim_real
+        (auto simp: filterlim_sequentially_iff_filterlim_real
           intro!: real_tendsto_divide_at_top tendsto_power_zero filterlim_real_sequentially
           tendsto_eq_intros filterlim_at_top_mult_tendsto_pos filterlim_tendsto_add_at_top)
   qed simp
@@ -3705,7 +3595,7 @@
   ultimately show ?thesis
     apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps)
     apply (simp add: algebra_simps)
-    apply (simp add: power2_eq_square [symmetric] algebra_simps)
+    apply (simp add: right_diff_distrib flip: power2_eq_square)
     done
 qed
 
@@ -3748,13 +3638,13 @@
   by (metis Arcsin_sin)
 
 lemma Arcsin_0 [simp]: "Arcsin 0 = 0"
-  by (metis Arcsin_sin norm_zero pi_half_gt_zero real_norm_def sin_zero zero_complex.simps(1))
+  by (simp add: Arcsin_unique)
 
 lemma Arcsin_1 [simp]: "Arcsin 1 = pi/2"
-  by (metis Arcsin_sin Im_complex_of_real Re_complex_of_real numeral_One of_real_numeral pi_half_ge_zero real_sqrt_abs real_sqrt_pow2 real_sqrt_power sin_of_real sin_pi_half)
+  using Arcsin_unique sin_of_real_pi_half by fastforce
 
 lemma Arcsin_minus_1 [simp]: "Arcsin(-1) = - (pi/2)"
-  by (metis Arcsin_1 Arcsin_sin Im_complex_of_real Re_complex_of_real abs_of_nonneg of_real_minus pi_half_ge_zero power2_minus real_sqrt_abs sin_Arcsin sin_minus)
+  by (simp add: Arcsin_unique)
 
 lemma has_field_derivative_Arcsin:
   assumes "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
@@ -3800,8 +3690,7 @@
   using Arcsin_range_lemma [of "-z"]  by simp
 
 lemma Arccos_body_lemma: "z + \<i> * csqrt(1 - z\<^sup>2) \<noteq> 0"
-  using Arcsin_body_lemma [of z]
-  by (metis Arcsin_body_lemma complex_i_mult_minus diff_minus_eq_add power2_minus right_minus_eq)
+  by (metis Arcsin_body_lemma complex_i_mult_minus diff_0 diff_eq_eq power2_minus)
 
 lemma Re_Arccos: "Re(Arccos z) = Im (Ln (z + \<i> * csqrt(1 - z\<^sup>2)))"
   by (simp add: Arccos_def)
@@ -3811,7 +3700,7 @@
 
 text\<open>A very tricky argument to find!\<close>
 lemma isCont_Arccos_lemma:
-  assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+  assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1"
     shows False
 proof (cases "Im z = 0")
   case True
@@ -3987,8 +3876,7 @@
   have "Arccos w \<bullet> Arccos w \<le> pi\<^sup>2 + (cmod w)\<^sup>2"
     using Re by (simp add: dot_square_norm cmod_power2 [of "Arccos w"])
   then have "cmod (Arccos w) \<le> pi + cmod (cos (Arccos w))"
-    apply (simp add: norm_le_square)
-    by (metis dot_square_norm norm_ge_zero norm_le_square pi_ge_zero triangle_lemma)
+    by (smt (verit) Im_Arccos_bound Re_Arccos_bound cmod_le cos_Arccos)
   then show "cmod (Arccos w) \<le> pi + cmod w"
     by auto
 qed
@@ -3996,68 +3884,11 @@
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Interrelations between Arcsin and Arccos\<close>
 
-lemma cos_Arcsin_nonzero:
-  assumes "z\<^sup>2 \<noteq> 1" shows "cos(Arcsin z) \<noteq> 0"
-proof -
-  have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = z\<^sup>2 * (z\<^sup>2 - 1)"
-    by (simp add: algebra_simps)
-  have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> z\<^sup>2 - 1"
-  proof
-    assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = z\<^sup>2 - 1"
-    then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (z\<^sup>2 - 1)\<^sup>2"
-      by simp
-    then have "z\<^sup>2 * (z\<^sup>2 - 1) = (z\<^sup>2 - 1)*(z\<^sup>2 - 1)"
-      using eq power2_eq_square by auto
-    then show False
-      using assms by simp
-  qed
-  then have "1 + \<i> * z * (csqrt (1 - z * z)) \<noteq> z\<^sup>2"
-    by (metis add_minus_cancel power2_eq_square uminus_add_conv_diff)
-  then have "2*(1 + \<i> * z * (csqrt (1 - z * z))) \<noteq> 2*z\<^sup>2"  (*FIXME cancel_numeral_factor*)
-    by (metis mult_cancel_left zero_neq_numeral)
-  then have "(\<i> * z + csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> -1"
-    using assms
-    apply (simp add: power2_sum)
-    apply (simp add: power2_eq_square algebra_simps)
-    done
-  then show ?thesis
-    apply (simp add: cos_exp_eq Arcsin_def exp_minus)
-    apply (simp add: divide_simps Arcsin_body_lemma)
-    apply (metis add.commute minus_unique power2_eq_square)
-    done
-qed
-
-lemma sin_Arccos_nonzero:
-  assumes "z\<^sup>2 \<noteq> 1" shows "sin(Arccos z) \<noteq> 0"
-proof -
-  have eq: "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = -(z\<^sup>2) * (1 - z\<^sup>2)"
-    by (simp add: algebra_simps)
-  have "\<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1 - z\<^sup>2"
-  proof
-    assume "\<i> * z * (csqrt (1 - z\<^sup>2)) = 1 - z\<^sup>2"
-    then have "(\<i> * z * (csqrt (1 - z\<^sup>2)))\<^sup>2 = (1 - z\<^sup>2)\<^sup>2"
-      by simp
-    then have "-(z\<^sup>2) * (1 - z\<^sup>2) = (1 - z\<^sup>2)*(1 - z\<^sup>2)"
-      using eq power2_eq_square by auto
-    then have "-(z\<^sup>2) = (1 - z\<^sup>2)"
-      using assms
-      by (metis add.commute add.right_neutral diff_add_cancel mult_right_cancel)
-    then show False
-      using assms by simp
-  qed
-  then have "z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2)) \<noteq> 1"
-    by (simp add: algebra_simps)
-  then have "2*(z\<^sup>2 + \<i> * z * (csqrt (1 - z\<^sup>2))) \<noteq> 2*1"
-    by (metis mult_cancel_left2 zero_neq_numeral)  (*FIXME cancel_numeral_factor*)
-  then have "(z + \<i> * csqrt (1 - z\<^sup>2))\<^sup>2 \<noteq> 1"
-    using assms
-    by (metis Arccos_def add.commute add.left_neutral cancel_comm_monoid_add_class.diff_cancel cos_Arccos csqrt_0 mult_zero_right)
-  then show ?thesis
-    apply (simp add: sin_exp_eq Arccos_def exp_minus)
-    apply (simp add: divide_simps Arccos_body_lemma)
-    apply (simp add: power2_eq_square)
-    done
-qed
+lemma cos_Arcsin_nonzero: "z\<^sup>2 \<noteq> 1 \<Longrightarrow>cos(Arcsin z) \<noteq> 0"
+  by (metis diff_0_right power_zero_numeral sin_Arcsin sin_squared_eq)
+
+lemma sin_Arccos_nonzero: "z\<^sup>2 \<noteq> 1 \<Longrightarrow>sin(Arccos z) \<noteq> 0"
+  by (metis add.right_neutral cos_Arccos power2_eq_square power_zero_numeral sin_cos_squared_add3)
 
 lemma cos_sin_csqrt:
   assumes "0 < cos(Re z)  \<or>  cos(Re z) = 0 \<and> Im z * sin(Re z) \<le> 0"
@@ -4076,185 +3907,51 @@
 qed (use assms in \<open>auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff\<close>)
 
 lemma Arcsin_Arccos_csqrt_pos:
-    "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))"
+    "(0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z) \<Longrightarrow> Arcsin z = Arccos(csqrt(1 - z\<^sup>2))"
   by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
 
 lemma Arccos_Arcsin_csqrt_pos:
-    "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))"
+    "(0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z) \<Longrightarrow> Arccos z = Arcsin(csqrt(1 - z\<^sup>2))"
   by (simp add: Arcsin_def Arccos_def Complex.csqrt_square add.commute)
 
 lemma sin_Arccos:
-    "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)"
+    "0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z \<Longrightarrow> sin(Arccos z) = csqrt(1 - z\<^sup>2)"
   by (simp add: Arccos_Arcsin_csqrt_pos)
 
 lemma cos_Arcsin:
-    "0 < Re z | Re z = 0 & 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)"
+    "0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z \<Longrightarrow> cos(Arcsin z) = csqrt(1 - z\<^sup>2)"
   by (simp add: Arcsin_Arccos_csqrt_pos)
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relationship with Arcsin on the Real Numbers\<close>
 
-lemma Im_Arcsin_of_real:
-  assumes "\<bar>x\<bar> \<le> 1"
-    shows "Im (Arcsin (of_real x)) = 0"
-proof -
-  have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
-    by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
-  then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
-    using assms abs_square_le_1
-    by (force simp add: Complex.cmod_power2)
-  then have "cmod (\<i> * of_real x + csqrt (1 - (of_real x)\<^sup>2)) = 1"
-    by (simp add: norm_complex_def)
-  then show ?thesis
-    by (simp add: Im_Arcsin exp_minus)
-qed
+lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
+  by (smt (verit, best) Arcsin_sin Im_complex_of_real Re_complex_of_real arcsin sin_of_real)
+
+lemma Im_Arcsin_of_real: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> Im (Arcsin (of_real x)) = 0"
+  by (metis Im_complex_of_real of_real_arcsin)
 
 corollary\<^marker>\<open>tag unimportant\<close> Arcsin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arcsin z \<in> \<real>"
   by (metis Im_Arcsin_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
 
-lemma arcsin_eq_Re_Arcsin:
-  assumes "\<bar>x\<bar> \<le> 1"
-    shows "arcsin x = Re (Arcsin (of_real x))"
-unfolding arcsin_def
-proof (rule the_equality, safe)
-  show "- (pi / 2) \<le> Re (Arcsin (complex_of_real x))"
-    using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
-    by (auto simp: Complex.in_Reals_norm Re_Arcsin)
-next
-  show "Re (Arcsin (complex_of_real x)) \<le> pi / 2"
-    using Re_Ln_pos_le [OF Arcsin_body_lemma, of "of_real x"]
-    by (auto simp: Complex.in_Reals_norm Re_Arcsin)
-next
-  show "sin (Re (Arcsin (complex_of_real x))) = x"
-    using Re_sin [of "Arcsin (of_real x)"] Arcsin_body_lemma [of "of_real x"]
-    by (simp add: Im_Arcsin_of_real assms)
-next
-  fix x'
-  assume "- (pi / 2) \<le> x'" "x' \<le> pi / 2" "x = sin x'"
-  then show "x' = Re (Arcsin (complex_of_real (sin x')))"
-    unfolding sin_of_real [symmetric]
-    by (subst Arcsin_sin) auto
-qed
-
-lemma of_real_arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arcsin x) = Arcsin(of_real x)"
-  by (metis Im_Arcsin_of_real add.right_neutral arcsin_eq_Re_Arcsin complex_eq mult_zero_right of_real_0)
+lemma arcsin_eq_Re_Arcsin: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> arcsin x = Re (Arcsin (of_real x))"
+  by (metis Re_complex_of_real of_real_arcsin)
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Relationship with Arccos on the Real Numbers\<close>
 
-lemma Im_Arccos_of_real:
-  assumes "\<bar>x\<bar> \<le> 1"
-    shows "Im (Arccos (of_real x)) = 0"
-proof -
-  have "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
-    by (simp add: of_real_sqrt del: csqrt_of_real_nonneg)
-  then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2))^2 = 1"
-    using assms abs_square_le_1
-    by (force simp add: Complex.cmod_power2)
-  then have "cmod (of_real x + \<i> * csqrt (1 - (of_real x)\<^sup>2)) = 1"
-    by (simp add: norm_complex_def)
-  then show ?thesis
-    by (simp add: Im_Arccos exp_minus)
-qed
+lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
+  by (smt (verit, del_insts) Arccos_unique Im_complex_of_real Re_complex_of_real arccos_lbound 
+      arccos_ubound cos_arccos_abs cos_of_real)
+
+lemma Im_Arccos_of_real: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> Im (Arccos (of_real x)) = 0"
+  by (metis Im_complex_of_real of_real_arccos)
 
 corollary\<^marker>\<open>tag unimportant\<close> Arccos_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> \<bar>Re z\<bar> \<le> 1 \<Longrightarrow> Arccos z \<in> \<real>"
-  by (metis Im_Arccos_of_real Re_complex_of_real Reals_cases complex_is_Real_iff)
-
-lemma arccos_eq_Re_Arccos:
-  assumes "\<bar>x\<bar> \<le> 1"
-    shows "arccos x = Re (Arccos (of_real x))"
-unfolding arccos_def
-proof (rule the_equality, safe)
-  show "0 \<le> Re (Arccos (complex_of_real x))"
-    using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
-    by (auto simp: Complex.in_Reals_norm Re_Arccos)
-next
-  show "Re (Arccos (complex_of_real x)) \<le> pi"
-    using Im_Ln_pos_le [OF Arccos_body_lemma, of "of_real x"]
-    by (auto simp: Complex.in_Reals_norm Re_Arccos)
-next
-  show "cos (Re (Arccos (complex_of_real x))) = x"
-    using Re_cos [of "Arccos (of_real x)"] Arccos_body_lemma [of "of_real x"]
-    by (simp add: Im_Arccos_of_real assms)
-next
-  fix x'
-  assume "0 \<le> x'" "x' \<le> pi" "x = cos x'"
-  then show "x' = Re (Arccos (complex_of_real (cos x')))"
-    unfolding cos_of_real [symmetric]
-    by (subst Arccos_cos) auto
-qed
-
-lemma of_real_arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
-  by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
-
-subsection\<^marker>\<open>tag unimportant\<close>\<open>Some interrelationships among the real inverse trig functions\<close>
-
-lemma arccos_arctan:
-  assumes "-1 < x" "x < 1"
-    shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
-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)"
-      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"
-      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"
-      using assms
-      by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
-                    power2_eq_square square_eq_1_iff)
-  qed
-  then show ?thesis
-    by simp
-qed
-
-lemma arcsin_plus_arccos:
-  assumes "-1 \<le> x" "x \<le> 1"
-    shows "arcsin x + arccos x = pi/2"
-proof -
-  have "arcsin x = pi/2 - arccos x"
-    apply (rule sin_inj_pi)
-    using assms arcsin [OF assms] arccos [OF assms]
-    by (auto simp: algebra_simps sin_diff)
-  then show ?thesis
-    by (simp add: algebra_simps)
-qed
-
-lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
-  using arcsin_plus_arccos by force
-
-lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
-  using arcsin_plus_arccos by force
-
-lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
-  by (simp add: arccos_arctan arcsin_arccos_eq)
-
-lemma csqrt_1_diff_eq: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
-  by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
-
-lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
-  apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
-  apply (subst Arcsin_Arccos_csqrt_pos)
-  apply (auto simp: power_le_one csqrt_1_diff_eq)
-  done
-
-lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
-  using arcsin_arccos_sqrt_pos [of "-x"]
-  by (simp add: arcsin_minus)
-
-lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
-  apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
-  apply (subst Arccos_Arcsin_csqrt_pos)
-  apply (auto simp: power_le_one csqrt_1_diff_eq)
-  done
-
-lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
-  using arccos_arcsin_sqrt_pos [of "-x"]
-  by (simp add: arccos_minus)
+  by (metis Im_Arccos_of_real complex_is_Real_iff of_real_Re)
+
+lemma arccos_eq_Re_Arccos: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> arccos x = Re (Arccos (of_real x))"
+  by (metis Re_complex_of_real of_real_arccos)
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Continuity results for arcsin and arccos\<close>
 
diff -r 947510ce4e36 -r 8a17349143df src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Thu Dec 29 16:44:45 2022 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Thu Dec 29 22:14:25 2022 +0000
@@ -118,12 +118,7 @@
           have *: "f \<in> U"
             if "U \<in> \<U>" and "\<forall>V\<in>\<U>. \<forall>i. i \<in> I \<and> Y V i \<noteq> topspace (X i) \<longrightarrow> f i \<in> Y V i"
               and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
-          proof -
-            have "Pi\<^sub>E I (Y U) = U"
-              using Y \<open>U \<in> \<U>\<close> by blast
-            then show "f \<in> U"
-              using that unfolding PiE_def Pi_def by blast
-          qed
+            by (smt (verit) PiE_iff Y that)
           show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
             by (auto simp: PiE_iff *)
           show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
@@ -158,18 +153,16 @@
           using Y by force
         show "?G ` \<U> \<subseteq> {Pi\<^sub>E I Y |Y. (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}}"
           apply clarsimp
-          apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
+          apply (rule_tac x= "(\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
           apply (auto simp: *)
           done
       next
         show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
         proof
           have "(\<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
-            apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
-            using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
+            by (simp add: PiE_mono Y \<open>U \<in> \<U>\<close> openin_subset)
           then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
-            using \<open>U \<in> \<U>\<close>
-            by fastforce
+            using \<open>U \<in> \<U>\<close> by fastforce
           moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
             using PiE_mem Y by fastforce
           ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
@@ -211,24 +204,25 @@
   assumes "openin (product_topology T I) U" "x \<in> U"
   shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
 proof -
-  have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
-    using assms unfolding product_topology_def by (intro openin_topology_generated_by) auto
-  then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
+  define IT where "IT \<equiv> \<lambda>X. {i. X i \<noteq> topspace (T i)}"
+  have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite (IT X)} U"
+    using assms unfolding product_topology_def IT_def by (intro openin_topology_generated_by) auto
+  then have "\<And>x. x\<in>U \<Longrightarrow> \<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite (IT X) \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
   proof induction
     case (Int U V x)
     then obtain XU XV where H:
-      "x \<in> Pi\<^sub>E I XU" "(\<forall>i. openin (T i) (XU i))" "finite {i. XU i \<noteq> topspace (T i)}" "Pi\<^sub>E I XU \<subseteq> U"
-      "x \<in> Pi\<^sub>E I XV" "(\<forall>i. openin (T i) (XV i))" "finite {i. XV i \<noteq> topspace (T i)}" "Pi\<^sub>E I XV \<subseteq> V"
-      by auto meson
+      "x \<in> Pi\<^sub>E I XU" "\<And>i. openin (T i) (XU i)" "finite (IT XU)" "Pi\<^sub>E I XU \<subseteq> U"
+      "x \<in> Pi\<^sub>E I XV" "\<And>i. openin (T i) (XV i)" "finite (IT XV)" "Pi\<^sub>E I XV \<subseteq> V"
+      by (meson Int_iff)
     define X where "X = (\<lambda>i. XU i \<inter> XV i)"
     have "Pi\<^sub>E I X \<subseteq> Pi\<^sub>E I XU \<inter> Pi\<^sub>E I XV"
-      unfolding X_def by (auto simp add: PiE_iff)
+      by (auto simp add: PiE_iff X_def)
     then have "Pi\<^sub>E I X \<subseteq> U \<inter> V" using H by auto
     moreover have "\<forall>i. openin (T i) (X i)"
       unfolding X_def using H by auto
-    moreover have "finite {i. X i \<noteq> topspace (T i)}"
-      apply (rule rev_finite_subset[of "{i. XU i \<noteq> topspace (T i)} \<union> {i. XV i \<noteq> topspace (T i)}"])
-      unfolding X_def using H by auto
+    moreover have "finite (IT X)"
+      apply (rule rev_finite_subset[of "IT XU \<union> IT XV"])
+      using H by (auto simp: X_def IT_def)
     moreover have "x \<in> Pi\<^sub>E I X"
       unfolding X_def using H by auto
     ultimately show ?case
@@ -236,16 +230,10 @@
   next
     case (UN K x)
     then obtain k where "k \<in> K" "x \<in> k" by auto
-    with UN have "\<exists>X. x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
-      by simp
-    then obtain X where "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> k"
-      by blast
-    then have "x \<in> Pi\<^sub>E I X \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> Pi\<^sub>E I X \<subseteq> (\<Union>K)"
-      using \<open>k \<in> K\<close> by auto
-    then show ?case
-      by auto
+    with \<open>k \<in> K\<close> UN show ?case
+      by (meson Sup_upper2)
   qed auto
-  then show ?thesis using \<open>x \<in> U\<close> by auto
+  then show ?thesis using \<open>x \<in> U\<close> IT_def by blast
 qed
 
 lemma product_topology_empty_discrete:
@@ -257,9 +245,7 @@
     arbitrary union_of
           ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
            relative_to topspace (product_topology X I))"
-  apply (subst product_topology)
-  apply (simp add: topology_inverse' [OF istopology_subbase])
-  done
+  by (simp add: istopology_subbase product_topology)
 
 lemma subtopology_PiE:
   "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
@@ -349,6 +335,7 @@
   "openin (product_topology X I) S \<longleftrightarrow>
     (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
                  (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
+sledgehammer [isar_proofs, provers = "cvc4 z3 spass e vampire verit", timeout = 77]
   unfolding openin_product_topology arbitrary_union_of_alt product_topology_base_alt topspace_product_topology
   apply safe
   apply (drule bspec; blast)+
@@ -438,9 +425,7 @@
 
 corollary closedin_product_topology:
    "closedin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. closedin (X i) (S i))"
-  apply (simp add: PiE_eq PiE_eq_empty_iff closure_of_product_topology flip: closure_of_eq)
-  apply (metis closure_of_empty)
-  done
+  by (smt (verit, best) PiE_eq closedin_empty closure_of_eq closure_of_product_topology)
 
 corollary closedin_product_topology_singleton:
    "f \<in> extensional I \<Longrightarrow> closedin (product_topology X I) {f} \<longleftrightarrow> (\<forall>i \<in> I. closedin (X i) {f i})"
@@ -501,17 +486,13 @@
   also have "... = (\<Inter>i\<in>J. (\<lambda>x. f x i)-`(X i) \<inter> topspace T1) \<inter> (topspace T1)"
     using * \<open>J \<subseteq> I\<close> by auto
   also have "openin T1 (...)"
-    apply (rule openin_INT)
-    apply (simp add: \<open>finite J\<close>)
-    using H(2) assms(1) \<open>J \<subseteq> I\<close> by auto
+    using H(2) \<open>J \<subseteq> I\<close> \<open>finite J\<close> assms(1) by blast
   ultimately show "openin T1 (f-`U \<inter> topspace T1)" by simp
 next
-  show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
-    apply (subst topology_generated_by_topspace[symmetric])
-    apply (subst product_topology_def[symmetric])
-    apply (simp only: topspace_product_topology)
-    apply (auto simp add: PiE_iff)
-    using assms unfolding continuous_map_def by auto
+  have "f ` topspace T1 \<subseteq> topspace (product_topology T I)"
+    using assms continuous_map_def by fastforce
+  then show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
+    by (simp add: product_topology_def)
 qed
 
 lemma continuous_map_product_then_coordinatewise [intro]:
@@ -522,8 +503,7 @@
   fix i assume "i \<in> I"
   have "(\<lambda>x. f x i) = (\<lambda>y. y i) o f" by auto
   also have "continuous_map T1 (T i) (...)"
-    apply (rule continuous_map_compose[of _ "product_topology T I"])
-    using assms \<open>i \<in> I\<close> by auto
+    by (metis \<open>i \<in> I\<close> assms continuous_map_compose continuous_map_product_coordinates)
   ultimately show "continuous_map T1 (T i) (\<lambda>x. f x i)"
     by simp
 next
@@ -583,28 +563,14 @@
   assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> open (U i)"
   shows "open {f. \<forall>i\<in>I. f (x i) \<in> U i}"
 proof -
-  define J where "J = x`I"
-  define V where "V = (\<lambda>y. if y \<in> J then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
-  define X where "X = (\<lambda>y. if y \<in> J then V y else UNIV)"
+  define V where "V \<equiv> (\<lambda>y. if y \<in> x`I then \<Inter>{U i|i. i\<in>I \<and> x i = y} else UNIV)"
+  define X where "X \<equiv> (\<lambda>y. if y \<in> x`I then V y else UNIV)"
   have *: "open (X i)" for i
     unfolding X_def V_def using assms by auto
-  have **: "finite {i. X i \<noteq> UNIV}"
-    unfolding X_def V_def J_def using assms(1) by auto
-  have "open (Pi\<^sub>E UNIV X)"
-    by (simp add: "*" "**" open_PiE)
+  then have "open (Pi\<^sub>E UNIV X)"
+    by (simp add: X_def assms(1) open_PiE)
   moreover have "Pi\<^sub>E UNIV X = {f. \<forall>i\<in>I. f (x i) \<in> U i}"
-    apply (auto simp add: PiE_iff) unfolding X_def V_def J_def
-    proof (auto)
-      fix f :: "'a \<Rightarrow> 'b" and i :: 'i
-      assume a1: "i \<in> I"
-      assume a2: "\<forall>i. f i \<in> (if i \<in> x`I then if i \<in> x`I then \<Inter>{U ia |ia. ia \<in> I \<and> x ia = i} else UNIV else UNIV)"
-      have f3: "x i \<in> x`I"
-        using a1 by blast
-      have "U i \<in> {U ia |ia. ia \<in> I \<and> x ia = x i}"
-        using a1 by blast
-      then show "f (x i) \<in> U i"
-        using f3 a2 by (meson Inter_iff)
-    qed
+    by (fastforce simp add: PiE_iff X_def V_def split: if_split_asm)
   ultimately show ?thesis by simp
 qed
 
@@ -620,25 +586,13 @@
   fixes f :: "'a::topological_space \<Rightarrow> 'b \<Rightarrow> 'c::topological_space"
   assumes "\<And>i. continuous_on S (\<lambda>x. f x i)"
   shows "continuous_on S f"
-  using continuous_map_coordinatewise_then_product [of UNIV, where T = "\<lambda>i. euclidean"]
-  by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology)
-
-lemma continuous_on_product_then_coordinatewise_UNIV:
-  assumes "continuous_on UNIV f"
-  shows "continuous_on UNIV (\<lambda>x. f x i)"
-  unfolding continuous_map_iff_continuous2 [symmetric]
-  by (rule continuous_map_product_then_coordinatewise [where I=UNIV]) (use assms in \<open>auto simp: euclidean_product_topology\<close>)
+  by (metis UNIV_I assms continuous_map_iff_continuous euclidean_product_topology
+      continuous_map_coordinatewise_then_product)
 
 lemma continuous_on_product_then_coordinatewise:
   assumes "continuous_on S f"
   shows "continuous_on S (\<lambda>x. f x i)"
-proof -
-  have "continuous_on S ((\<lambda>q. q i) \<circ> f)"
-    by (metis assms continuous_on_compose continuous_on_id
-        continuous_on_product_then_coordinatewise_UNIV continuous_on_subset subset_UNIV)
-  then show ?thesis
-    by auto
-qed
+  by (metis UNIV_I assms continuous_map_iff_continuous continuous_map_product_then_coordinatewise(1) euclidean_product_topology)
 
 lemma continuous_on_coordinatewise_iff:
   fixes f :: "('a \<Rightarrow> real) \<Rightarrow> 'b \<Rightarrow> real"
@@ -679,16 +633,15 @@
   next
     case (Suc N)
     define f::"((nat \<Rightarrow> 'a) \<times> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)"
-      where "f = (\<lambda>(x, b). (\<lambda>i. if i = N then b else x i))"
+      where "f = (\<lambda>(x, b). x(N:=b))"
     have "{x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>Suc N. x i = a)} \<subseteq> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
     proof (auto)
       fix x assume H: "\<forall>i::nat. x i \<in> F" "\<forall>i\<ge>Suc N. x i = a"
-      define y where "y = (\<lambda>i. if i = N then a else x i)"
-      have "f (y, x N) = x"
-        unfolding f_def y_def by auto
-      moreover have "(y, x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
-        unfolding y_def using H \<open>a \<in> F\<close> by auto
-      ultimately show "x \<in> f`({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
+      have "f (x(N:=a), x N) = x"
+        unfolding f_def by auto
+      moreover have "(x(N:=a), x N) \<in> {x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F"
+        using H \<open>a \<in> F\<close> by auto
+      ultimately show "x \<in> f ` ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
         by (metis (no_types, lifting) image_eqI)
     qed
     moreover have "countable ({x. (\<forall>i. x i \<in> F) \<and> (\<forall>i\<ge>N. x i = a)} \<times> F)"
@@ -742,7 +695,7 @@
     by metis
   text \<open>\<open>B i\<close> is a countable basis of neighborhoods of \<open>x\<^sub>i\<close>.\<close>
   define B where "B = (\<lambda>i. (A (x i))`UNIV \<union> {UNIV})"
-  have "countable (B i)" for i unfolding B_def by auto
+  have countB: "countable (B i)" for i unfolding B_def by auto
   have open_B: "\<And>X i. X \<in> B i \<Longrightarrow> open X"
     by (auto simp: B_def A)
   define K where "K = {Pi\<^sub>E UNIV X | X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
@@ -750,14 +703,14 @@
     unfolding K_def B_def by auto
   then have "K \<noteq> {}" by auto
   have "countable {X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
-    apply (rule countable_product_event_const) using \<open>\<And>i. countable (B i)\<close> by auto
+    by (simp add: countB countable_product_event_const)
   moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B i) \<and> finite {i. X i \<noteq> UNIV}}"
     unfolding K_def by auto
   ultimately have "countable K" by auto
-  have "x \<in> k" if "k \<in> K" for k
+  have I: "x \<in> k" if "k \<in> K" for k
     using that unfolding K_def B_def apply auto using A(1) by auto
-  have "open k" if "k \<in> K" for k
-    using that unfolding K_def  by (blast intro: open_B open_PiE elim: )
+  have II: "open k" if "k \<in> K" for k
+    using that unfolding K_def by (blast intro: open_B open_PiE)
   have Inc: "\<exists>k\<in>K. k \<subseteq> U" if "open U \<and> x \<in> U" for U
   proof -
     have "openin (product_topology (\<lambda>i. euclidean) UNIV) U" "x \<in> U"
@@ -775,31 +728,28 @@
     have *: "\<exists>y. y \<in> B i \<and> y \<subseteq> X i" for i
       unfolding B_def using A(3)[OF H(2)] H(1) by (metis PiE_E UNIV_I UnCI image_iff)
     have **: "Y i \<in> B i \<and> Y i \<subseteq> X i" for i
-      apply (cases "i \<in> I")
-      unfolding Y_def using * that apply (auto)
-      apply (metis (no_types, lifting) someI, metis (no_types, lifting) someI_ex subset_iff)
-      unfolding B_def apply simp
-      unfolding I_def apply auto
-      done
+    proof (cases "i \<in> I")
+      case True
+      then show ?thesis  
+        by (metis (mono_tags, lifting) "*" Nitpick.Eps_psimp Y_def)
+    next
+      case False
+      then show ?thesis by (simp add: B_def I_def Y_def)
+    qed
     have "{i. Y i \<noteq> UNIV} \<subseteq> I"
       unfolding Y_def by auto
-    then have ***: "finite {i. Y i \<noteq> UNIV}"
-      unfolding I_def using H(3) rev_finite_subset by blast
-    have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
-      using ** *** by auto
+    with ** have "(\<forall>i. Y i \<in> B i) \<and> finite {i. Y i \<noteq> UNIV}"
+      using H(3) I_def finite_subset by blast
     then have "Pi\<^sub>E UNIV Y \<in> K"
       unfolding K_def by auto
-
     have "Y i \<subseteq> X i" for i
-      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
-    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
-    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
+      using "**" by auto
+    then have "Pi\<^sub>E UNIV Y \<subseteq> U"
+      by (metis H(4) PiE_mono subset_trans)
     then show ?thesis using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> by auto
   qed
-
   show "\<exists>L. (\<forall>(i::nat). x \<in> L i \<and> open (L i)) \<and> (\<forall>U. open U \<and> x \<in> U \<longrightarrow> (\<exists>i. L i \<subseteq> U))"
-    apply (rule first_countableI[of K])
-    using \<open>countable K\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> x \<in> k\<close> \<open>\<And>k. k \<in> K \<Longrightarrow> open k\<close> Inc by auto
+    using \<open>countable K\<close> I II Inc by (simp add: first_countableI) 
 qed
 
 proposition product_topology_countable_basis:
@@ -821,7 +771,7 @@
     unfolding K_def using \<open>\<And>U. U \<in> B2 \<Longrightarrow> open U\<close> by auto
 
   have "countable {X. (\<forall>(i::'a). X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
-    apply (rule countable_product_event_const) using \<open>countable B2\<close> by auto
+    using \<open>countable B2\<close>  by (intro countable_product_event_const) auto
   moreover have "K = (\<lambda>X. Pi\<^sub>E UNIV X)`{X. (\<forall>i. X i \<in> B2) \<and> finite {i. X i \<noteq> UNIV}}"
     unfolding K_def by auto
   ultimately have ii: "countable K" by auto
@@ -832,9 +782,7 @@
     then have "openin (product_topology (\<lambda>i. euclidean) UNIV) U"
       unfolding open_fun_def by auto
     with product_topology_open_contains_basis[OF this \<open>x \<in> U\<close>]
-    have "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<and> (\<forall>i. open (X i)) \<and> finite {i. X i \<noteq> UNIV} \<and> (\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
-      by simp
-    then obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
+    obtain X where H: "x \<in> (\<Pi>\<^sub>E i\<in>UNIV. X i)"
                            "\<And>i. open (X i)"
                            "finite {i. X i \<noteq> UNIV}"
                            "(\<Pi>\<^sub>E i\<in>UNIV. X i) \<subseteq> U"
@@ -845,29 +793,15 @@
     have *: "\<exists>y. y \<in> B2 \<and> y \<subseteq> X i \<and> x i \<in> y" for i
       unfolding B2_def using B \<open>open (X i)\<close> \<open>x i \<in> X i\<close> by (meson UnCI topological_basisE)
     have **: "Y i \<in> B2 \<and> Y i \<subseteq> X i \<and> x i \<in> Y i" for i
-      using someI_ex[OF *]
-      apply (cases "i \<in> I")
-      unfolding Y_def using * apply (auto)
-      unfolding B2_def I_def by auto
+      using someI_ex[OF *] by (simp add: B2_def I_def Y_def)
     have "{i. Y i \<noteq> UNIV} \<subseteq> I"
       unfolding Y_def by auto
-    then have ***: "finite {i. Y i \<noteq> UNIV}"
-      unfolding I_def using H(3) rev_finite_subset by blast
-    have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
-      using ** *** by auto
+    then have "(\<forall>i. Y i \<in> B2) \<and> finite {i. Y i \<noteq> UNIV}"
+      using "**" H(3) I_def finite_subset by blast
     then have "Pi\<^sub>E UNIV Y \<in> K"
       unfolding K_def by auto
-
-    have "Y i \<subseteq> X i" for i
-      apply (cases "i \<in> I") using ** apply simp unfolding Y_def I_def by auto
-    then have "Pi\<^sub>E UNIV Y \<subseteq> Pi\<^sub>E UNIV X" by auto
-    then have "Pi\<^sub>E UNIV Y \<subseteq> U" using H(4) by auto
-
-    have "x \<in> Pi\<^sub>E UNIV Y"
-      using ** by auto
-
-    show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
-      using \<open>Pi\<^sub>E UNIV Y \<in> K\<close> \<open>Pi\<^sub>E UNIV Y \<subseteq> U\<close> \<open>x \<in> Pi\<^sub>E UNIV Y\<close> by auto
+    then show "\<exists>V\<in>K. x \<in> V \<and> V \<subseteq> U"
+      by (meson "**" H(4) PiE_I PiE_mono UNIV_I order.trans)
   next
     fix U assume "U \<in> K"
     show "open U"
@@ -878,9 +812,11 @@
 qed
 
 instance "fun" :: (countable, second_countable_topology) second_countable_topology
-  apply standard
-  using product_topology_countable_basis topological_basis_imp_subbasis by auto
-
+proof
+  show "\<exists>B::('a \<Rightarrow> 'b) set set. countable B \<and> open = generate_topology B"
+    using product_topology_countable_basis topological_basis_imp_subbasis 
+    by auto
+qed
 
 subsection\<open>The Alexander subbase theorem\<close>
 
@@ -1106,11 +1042,7 @@
   qed
   ultimately show ?thesis
     by metis
-next
-  case False
-  then show ?thesis
-    by (auto simp: continuous_map_def PiE_def)
-qed
+qed (auto simp: continuous_map_def PiE_def)
 
 
 lemma continuous_map_componentwise_UNIV:
@@ -1147,8 +1079,7 @@
       fix x f
       assume "f \<in> V"
       let ?T = "{a \<in> topspace(Y i).
-                   (\<lambda>j. if j = i then a
-                        else if j \<in> I then f j else undefined) \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>}"
+                   (\<lambda>j\<in>I. f j)(i:=a) \<in> (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>}"
       show "\<exists>T. openin (Y i) T \<and> f i \<in> T \<and> T \<subseteq> (\<lambda>f. f i) ` V"
       proof (intro exI conjI)
         show "openin (Y i) ?T"
@@ -1164,8 +1095,8 @@
               by simp (metis IntD1 PiE_iff V \<open>f \<in> V\<close> that)
           qed
           then show "continuous_map (Y i) (product_topology Y I)
-                  (\<lambda>x j. if j = i then x else if j \<in> I then f j else undefined)"
-            by (auto simp: continuous_map_componentwise assms extensional_def)
+                  (\<lambda>x. (\<lambda>j\<in>I. f j)(i:=x))"
+            by (auto simp: continuous_map_componentwise assms extensional_def restrict_def)
         next
           have "openin (product_topology Y I) (\<Pi>\<^sub>E i\<in>I. topspace (Y i))"
             by (metis openin_topspace topspace_product_topology)
@@ -1177,18 +1108,15 @@
               show "\<And>X. X \<in> (\<inter>) (\<Pi>\<^sub>E i\<in>I. topspace (Y i)) ` \<F> \<Longrightarrow> openin (product_topology Y I) X"
                 unfolding openin_product_topology relative_to_def
                 apply (clarify intro!: arbitrary_union_of_inc)
-                apply (rename_tac F)
-                apply (rule_tac x=F in exI)
                 using subsetD [OF \<F>]
-                apply (force intro: finite_intersection_of_inc)
-                done
+                by (metis (mono_tags, lifting) finite_intersection_of_inc mem_Collect_eq topspace_product_topology)
             qed (use \<open>finite \<F>\<close> \<open>\<F> \<noteq> {}\<close> in auto)
           qed
           ultimately show "openin (product_topology Y I) ((\<Pi>\<^sub>E i\<in>I. topspace (Y i)) \<inter> \<Inter>\<F>)"
             by (auto simp only: Int_Inter_eq split: if_split)
         qed
       next
-        have eqf: "(\<lambda>j. if j = i then f i else if j \<in> I then f j else undefined) = f"
+        have eqf: "(\<lambda>j\<in>I. f j)(i:=f i) = f"
           using PiE_arb V \<open>f \<in> V\<close> by force
         show "f i \<in> ?T"
           using V assms \<open>f \<in> V\<close> by (auto simp: PiE_iff eqf)
@@ -1273,10 +1201,8 @@
   next
     assume ?rhs
     then show ?lhs
-      apply (simp only: openin_product_topology)
-      apply (rule arbitrary_union_of_inc)
-      apply (auto simp: product_topology_base_alt)
-      done
+      unfolding openin_product_topology
+      by (intro arbitrary_union_of_inc) (auto simp: product_topology_base_alt)
   qed
   ultimately show ?thesis
     by simp
@@ -1306,9 +1232,7 @@
         by (simp add: continuous_map_product_projection)
       moreover
       have "\<And>x. x \<in> topspace (X i) \<Longrightarrow> x \<in> (\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
-        using \<open>i \<in> I\<close> z
-        apply (rule_tac x="\<lambda>j. if j = i then x else if j \<in> I then z j else undefined" in image_eqI, auto)
-        done
+        using \<open>i \<in> I\<close> z by (rule_tac x="z(i:=x)" in image_eqI) auto
       then have "(\<lambda>f. f i) ` (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = topspace (X i)"
         using \<open>i \<in> I\<close> z by auto
       ultimately show "compactin (X i) (topspace (X i))"
@@ -1461,7 +1385,7 @@
             then have "(\<lambda>x. x k) ` {x. x j \<in> V} = UNIV" if "k \<noteq> j" for k
               using that
               apply (clarsimp simp add: set_eq_iff)
-              apply (rule_tac x="\<lambda>m. if m = k then x else f m" in image_eqI, auto)
+              apply (rule_tac x="f(k:=x)" in image_eqI, auto)
               done
             then have "{i. (\<lambda>x. x i) ` C \<subset> topspace (X i)} \<subseteq> {j}"
               using Ceq by auto
@@ -1493,7 +1417,7 @@
               using PiE_ext \<open>g \<in> U\<close> gin by force
           next
             case (insert i M)
-            define f where "f \<equiv> \<lambda>j. if j = i then g i else h j"
+            define f where "f \<equiv> h(i:=g i)"
             have fin: "f \<in> PiE I (topspace \<circ> X)"
               unfolding f_def using gin insert.prems(1) by auto
             have subM: "{j \<in> I. f j \<noteq> g j} \<subseteq> M"
@@ -1506,13 +1430,13 @@
               show ?thesis
               proof (cases "i \<in> I")
                 case True
-                let ?U = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> U}"
-                let ?V = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> V}"
+                let ?U = "{x \<in> topspace(X i). h(i:=x) \<in> U}"
+                let ?V = "{x \<in> topspace(X i). h(i:=x) \<in> V}"
                 have False
                 proof (rule connected_spaceD [OF cs [OF \<open>i \<in> I\<close>]])
                   have "\<And>k. k \<in> I \<Longrightarrow> continuous_map (X i) (X k) (\<lambda>x. if k = i then x else h k)"
                     using continuous_map_eq_topcontinuous_at insert.prems(1) topcontinuous_at_def by fastforce
-                  then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x j. if j = i then x else h j)"
+                  then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x. h(i:=x))"
                     using \<open>i \<in> I\<close> insert.prems(1)
                     by (auto simp: continuous_map_componentwise extensional_def)
                   show "openin (X i) ?U"
@@ -1522,45 +1446,23 @@
                   show "topspace (X i) \<subseteq> ?U \<union> ?V"
                   proof clarsimp
                     fix x
-                    assume "x \<in> topspace (X i)" and "(\<lambda>j. if j = i then x else h j) \<notin> V"
+                    assume "x \<in> topspace (X i)" and "h(i:=x) \<notin> V"
                     with True subUV \<open>h \<in> Pi\<^sub>E I (topspace \<circ> X)\<close>
-                    show "(\<lambda>j. if j = i then x else h j) \<in> U"
-                      by (drule_tac c="(\<lambda>j. if j = i then x else h j)" in subsetD) auto
+                    show "h(i:=x) \<in> U"
+                      by (force dest: subsetD [where c="h(i:=x)"])
                   qed
                   show "?U \<inter> ?V = {}"
                     using disj by blast
                   show "?U \<noteq> {}"
-                    using \<open>U \<noteq> {}\<close> f_def
-                  proof -
-                    have "(\<lambda>j. if j = i then g i else h j) \<in> U"
-                      using \<open>f \<in> U\<close> f_def by blast
-                    moreover have "f i \<in> topspace (X i)"
-                      by (metis PiE_iff True comp_apply fin)
-                    ultimately have "\<exists>b. b \<in> topspace (X i) \<and> (\<lambda>a. if a = i then b else h a) \<in> U"
-                      using f_def by auto
-                    then show ?thesis
-                      by blast
-                  qed
-                  have "(\<lambda>j. if j = i then h i else h j) = h"
-                    by force
-                  moreover have "h i \<in> topspace (X i)"
-                    using True insert.prems(1) by auto
-                  ultimately show "?V \<noteq> {}"
-                    using \<open>h \<in> V\<close>  by force
+                    using True \<open>f \<in> U\<close> f_def gin by auto
+                  show "?V \<noteq> {}"
+                    using True \<open>h \<in> V\<close> V openin_subset by fastforce
                 qed
                 then show ?thesis ..
               next
                 case False
                 show ?thesis
-                proof (cases "h = f")
-                  case True
-                  show ?thesis
-                    by (rule insert.IH [OF insert.prems(1)]) (simp add: True subM)
-                next
-                  case False
-                  then show ?thesis
-                    using gin insert.prems(1) \<open>i \<notin> I\<close> unfolding f_def by fastforce
-                qed
+                  using insert.prems(1) by (metis False gin PiE_E \<open>f \<in> U\<close> f_def fun_upd_triv)
               qed
             next
               case False
@@ -1640,14 +1542,8 @@
   assumes "i \<in> I"
   shows "quotient_map(product_topology X I) (X i) (\<lambda>x. x i) \<longleftrightarrow>
            (topspace(product_topology X I) = {} \<longrightarrow> topspace(X i) = {})"
-         (is "?lhs = ?rhs")
-proof
-  assume ?lhs with assms show ?rhs
-    by (auto simp: continuous_open_quotient_map open_map_product_projection)
-next
-  assume ?rhs with assms show ?lhs
-    by (auto simp: Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection)
-qed
+  by (metis assms image_empty quotient_imp_surjective_map retraction_imp_quotient_map 
+      retraction_map_product_projection)
 
 lemma product_topology_homeomorphic_component:
   assumes "i \<in> I" "\<And>j. \<lbrakk>j \<in> I; j \<noteq> i\<rbrakk> \<Longrightarrow> \<exists>a. topspace(X j) = {a}"
@@ -1676,9 +1572,8 @@
     from that obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" 
       by force
     have "?SX f i homeomorphic_space X i"
-      apply (simp add: subtopology_PiE )
-      using product_topology_homeomorphic_component [OF \<open>i \<in> I\<close>, of "\<lambda>j. subtopology (X j) (if j = i then topspace (X i) else {f j})"]
-      using f by fastforce
+      using f product_topology_homeomorphic_component [OF \<open>i \<in> I\<close>, of "\<lambda>j. subtopology (X j) (if j = i then topspace (X i) else {f j})"]
+      by (force simp add: subtopology_PiE)
     then show ?thesis
       using minor [OF f major \<open>i \<in> I\<close>] PQ by auto
   qed
diff -r 947510ce4e36 -r 8a17349143df src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Thu Dec 29 16:44:45 2022 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Dec 29 22:14:25 2022 +0000
@@ -26,9 +26,9 @@
   proof (rule SUP_eqI)
     fix y :: ennreal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
     from this[of "Suc i"] show "f i \<le> y" by auto
-  qed (insert assms, simp)
+  qed (use assms in simp)
   ultimately show ?thesis using assms
-    by (subst suminf_eq_SUP) (auto simp: indicator_def)
+    by (simp add: suminf_eq_SUP)
 qed
 
 lemma suminf_indicator:
@@ -71,11 +71,8 @@
         by (induct n)  (auto simp add: binaryset_def f)
     qed
   moreover
-  have "... \<longlonglongrightarrow> f A + f B" by (rule tendsto_const)
-  ultimately
-  have "(\<lambda>n. \<Sum>i< Suc (Suc n). f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
-    by metis
-  hence "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
+  have "\<dots> \<longlonglongrightarrow> f A + f B" by (rule tendsto_const)
+  ultimately have "(\<lambda>n. \<Sum>i< n+2. f (binaryset A B i)) \<longlonglongrightarrow> f A + f B"
     by simp
   thus ?thesis by (rule LIMSEQ_offset [where k=2])
 qed
@@ -83,7 +80,7 @@
 lemma binaryset_sums:
   assumes f: "f {} = 0"
   shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
-    by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f] atLeast0LessThan)
+  using LIMSEQ_binaryset f sums_def by blast
 
 lemma suminf_binaryset_eq:
   fixes f :: "'a set \<Rightarrow> 'b::{comm_monoid_add, t2_space}"
@@ -148,7 +145,7 @@
   by (auto simp add: increasing_def)
 
 lemma countably_additiveI[case_names countably]:
-  "(\<And>A. range A \<subseteq> M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> M \<Longrightarrow> (\<Sum>i. f (A i)) = f (\<Union>i. A i))
+  "(\<And>A. \<lbrakk>range A \<subseteq> M; disjoint_family A; (\<Union>i. A i) \<in> M\<rbrakk> \<Longrightarrow> (\<Sum>i. f(A i)) = f(\<Union>i. A i))
   \<Longrightarrow> countably_additive M f"
   by (simp add: countably_additive_def)
 
@@ -198,9 +195,9 @@
   assume xy: "x \<in> M" "y \<in> M" "x \<subseteq> y"
   then have "y - x \<in> M" by auto
   then have "f x + 0 \<le> f x + f (y-x)" by (intro add_left_mono zero_le)
-  also have "... = f (x \<union> (y-x))" using addf
-    by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
-  also have "... = f y"
+  also have "\<dots> = f (x \<union> (y-x))"
+    by (metis addf Diff_disjoint \<open>y - x \<in> M\<close> additiveD xy(1))
+  also have "\<dots> = f y"
     by (metis Un_Diff_cancel Un_absorb1 xy(3))
   finally show "f x \<le> f y" by simp
 qed
@@ -222,9 +219,12 @@
   also have "\<dots> = f (A x) + f ((\<Union>i\<in>F. A i) - A x)"
     using f(2) by (rule additiveD) (insert in_M, auto)
   also have "\<dots> \<le> f (A x) + f (\<Union>i\<in>F. A i)"
-    using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
-  also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
-  finally show "f (\<Union>i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
+    using additive_increasing[OF f] in_M subs 
+    by (simp add: increasingD)
+  also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" 
+    using insert by (auto intro: add_left_mono)
+  finally show "f (\<Union>i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))"
+    by (simp add: insert)
 qed
 
 lemma (in ring_of_sets) countably_additive_additive:
@@ -239,10 +239,8 @@
   hence "range (binaryset x y) \<subseteq> M \<longrightarrow>
          (\<Union>i. binaryset x y i) \<in> M \<longrightarrow>
          f (\<Union>i. binaryset x y i) = (\<Sum> n. f (binaryset x y n))"
-    using ca
-    by (simp add: countably_additive_def)
-  hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow>
-         f (x \<union> y) = (\<Sum>n. f (binaryset x y n))"
+    using ca by (simp add: countably_additive_def)
+  hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow> f (x \<union> y) = (\<Sum>n. f (binaryset x y n))"
     by (simp add: range_binaryset_eq UN_binaryset_eq)
   thus "f (x \<union> y) = f x + f y" using posf x y
     by (auto simp add: Un suminf_binaryset_eq positive_def)
@@ -259,8 +257,8 @@
   fix N
   note disj_N = disjoint_family_on_mono[OF _ disj, of "{..<N}"]
   have "(\<Sum>i<N. f (A i)) = f (\<Union>i\<in>{..<N}. A i)"
-    using A by (intro additive_sum [OF f ad _ _]) (auto simp: disj_N)
-  also have "... \<le> f \<Omega>" using space_closed A
+    using A by (intro additive_sum [OF f ad]) (auto simp: disj_N)
+  also have "\<dots> \<le> f \<Omega>" using space_closed A
     by (intro increasingD[OF inc] finite_UN) auto
   finally show "(\<Sum>i<N. f (A i)) \<le> f \<Omega>" by simp
 qed (insert f A, auto simp: positive_def)
@@ -272,16 +270,10 @@
 proof (rule countably_additiveI)
   fix F :: "nat \<Rightarrow> 'a set" assume F: "range F \<subseteq> M" "(\<Union>i. F i) \<in> M" and disj: "disjoint_family F"
 
-  have "\<forall>i\<in>{i. F i \<noteq> {}}. \<exists>x. x \<in> F i" by auto
-  from bchoice[OF this] obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by auto
-
-  have inj_f: "inj_on f {i. F i \<noteq> {}}"
-  proof (rule inj_onI, simp)
-    fix i j a b assume *: "f i = f j" "F i \<noteq> {}" "F j \<noteq> {}"
-    then have "f i \<in> F i" "f j \<in> F j" using f by force+
-    with disj * show "i = j" by (auto simp: disjoint_family_on_def)
-  qed
-  have "finite (\<Union>i. F i)"
+  have "\<forall>i. F i \<noteq> {} \<longrightarrow> (\<exists>x. x \<in> F i)" by auto
+  then obtain f where f: "\<And>i. F i \<noteq> {} \<Longrightarrow> f i \<in> F i" by metis
+
+  have finU: "finite (\<Union>i. F i)"
     by (metis F(2) assms(1) infinite_super sets_into_space)
 
   have F_subset: "{i. \<mu> (F i) \<noteq> 0} \<subseteq> {i. F i \<noteq> {}}"
@@ -290,8 +282,11 @@
   proof (rule finite_imageD)
     from f have "f`{i. F i \<noteq> {}} \<subseteq> (\<Union>i. F i)" by auto
     then show "finite (f`{i. F i \<noteq> {}})"
-      by (rule finite_subset) fact
-  qed fact
+      by (simp add: finU finite_subset)
+    show inj_f: "inj_on f {i. F i \<noteq> {}}" 
+      using f disj
+      by (simp add: inj_on_def disjoint_family_on_def disjoint_iff) metis
+  qed 
   ultimately have fin_not_0: "finite {i. \<mu> (F i) \<noteq> 0}"
     by (rule finite_subset)
 
@@ -323,8 +318,7 @@
   have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
     by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
   moreover have "(\<lambda>n. (\<Sum>i<n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
-    using f(1)[unfolded positive_def] dA
-    by (auto intro!: summable_LIMSEQ)
+    by (simp add: summable_LIMSEQ)
   from LIMSEQ_Suc[OF this]
   have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) \<longlonglongrightarrow> (\<Sum>i. f (disjointed A i))"
     unfolding lessThan_Suc_atMost .
@@ -332,23 +326,21 @@
     using disjointed_additive[OF f A(1,2)] .
   ultimately show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)" by simp
 next
-  assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
+  assume cont[rule_format]: "\<forall>A. range A \<subseteq> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
   fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> M"
   have *: "(\<Union>n. (\<Union>i<n. A i)) = (\<Union>i. A i)" by auto
-  have "(\<lambda>n. f (\<Union>i<n. A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
-  proof (unfold *[symmetric], intro cont[rule_format])
-    show "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
-      using A * by auto
-  qed (force intro!: incseq_SucI)
+  have "range (\<lambda>i. \<Union>i<i. A i) \<subseteq> M" "(\<Union>i. \<Union>i<i. A i) \<in> M"
+    using A * by auto
+  then have "(\<lambda>n. f (\<Union>i<n. A i)) \<longlonglongrightarrow> f (\<Union>i. A i)"
+    unfolding *[symmetric] by (force intro!: cont incseq_SucI)+
   moreover have "\<And>n. f (\<Union>i<n. A i) = (\<Sum>i<n. f (A i))"
     using A
-    by (intro additive_sum[OF f, of _ A, symmetric])
-       (auto intro: disjoint_family_on_mono[where B=UNIV])
+    by (intro additive_sum[OF f, symmetric]) (auto intro: disjoint_family_on_mono)
   ultimately
   have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
     unfolding sums_def by simp
-  from sums_unique[OF this]
-  show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
+  then show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)"
+    by (metis sums_unique)
 qed
 
 lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
@@ -357,13 +349,15 @@
   shows "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))
      \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0)"
 proof safe
-  assume cont: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))"
-  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
-  with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
+  assume cont[rule_format]: "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> f (\<Inter>i. A i))"
+  fix A :: "nat \<Rightarrow> 'a set" 
+  assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
+  with cont[of A] show "(\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
     using \<open>positive M f\<close>[unfolded positive_def] by auto
 next
-  assume cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
-  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>"
+  assume cont[rule_format]: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) \<longlonglongrightarrow> 0"
+  fix A :: "nat \<Rightarrow> 'a set" 
+  assume A: "range A \<subseteq> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>"
 
   have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
     using additive_increasing[OF f] unfolding increasing_def by simp
@@ -378,23 +372,19 @@
     using A by (auto intro!: f_mono)
   then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
     using A by (auto simp: top_unique)
-  { fix i
-    have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
-    then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
-      using A by (auto simp: top_unique) }
-  note f_fin = this
+  have f_fin: "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>" for i
+    using A by (metis Diff Diff_subset f_mono infinity_ennreal_def range_subsetD top_unique)
   have "(\<lambda>i. f (A i - (\<Inter>i. A i))) \<longlonglongrightarrow> 0"
-  proof (intro cont[rule_format, OF _ decseq _ f_fin])
+  proof (intro cont[ OF _ decseq _ f_fin])
     show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
       using A by auto
   qed
-  from INF_Lim[OF decseq_f this]
-  have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
+  with INF_Lim decseq_f have "(INF n. f (A n - (\<Inter>i. A i))) = 0" by metis
   moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
     by auto
   ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
     using A(4) f_fin f_Int_fin
-    by (subst INF_ennreal_add_const) (auto simp: decseq_f)
+    using INF_ennreal_add_const by presburger
   moreover {
     fix n
     have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i))"
@@ -424,7 +414,8 @@
     also have "((\<Union>i. A i) - A i) \<union> A i = (\<Union>i. A i)"
       by auto
     finally have "f ((\<Union>i. A i) - A i) = f (\<Union>i. A i) - f (A i)"
-      using f(3)[rule_format, of "A i"] A by (auto simp: ennreal_add_diff_cancel subset_eq) }
+      using assms f by fastforce
+  }
   moreover have "\<forall>\<^sub>F i in sequentially. f (A i) \<le> f (\<Union>i. A i)"
     using increasingD[OF additive_increasing[OF f(1, 2)], of "A _" "\<Union>i. A i"] A
     by (auto intro!: always_eventually simp: subset_eq)
@@ -502,17 +493,11 @@
   by (metis emeasure_mono emeasure_notin_sets sets.sets_into_space sets.top zero_le)
 
 lemma emeasure_Diff:
-  assumes finite: "emeasure M B \<noteq> \<infinity>"
-  and [measurable]: "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
+  assumes "emeasure M B \<noteq> \<infinity>"
+  and "A \<in> sets M" "B \<in> sets M" and "B \<subseteq> A"
   shows "emeasure M (A - B) = emeasure M A - emeasure M B"
-proof -
-  have "(A - B) \<union> B = A" using \<open>B \<subseteq> A\<close> by auto
-  then have "emeasure M A = emeasure M ((A - B) \<union> B)" by simp
-  also have "\<dots> = emeasure M (A - B) + emeasure M B"
-    by (subst plus_emeasure[symmetric]) auto
-  finally show "emeasure M (A - B) = emeasure M A - emeasure M B"
-    using finite by simp
-qed
+  by (smt (verit, best) add_diff_self_ennreal assms emeasure_Un emeasure_mono 
+      ennreal_add_left_cancel le_iff_sup)
 
 lemma emeasure_compl:
   "s \<in> sets M \<Longrightarrow> emeasure M s \<noteq> \<infinity> \<Longrightarrow> emeasure M (space M - s) = emeasure M (space M) - emeasure M s"
@@ -563,8 +548,7 @@
   also have "\<dots> = emeasure M (A 0) - emeasure M (\<Inter>i. A i)"
     using A finite * by (simp, subst emeasure_Diff) auto
   finally show ?thesis
-    by (rule ennreal_minus_cancel[rotated 3])
-       (insert finite A, auto intro: INF_lower emeasure_mono)
+    by (smt (verit, best) Inf_lower diff_diff_ennreal le_MI finite range_eqI)
 qed
 
 lemma INF_emeasure_decseq':
@@ -580,7 +564,7 @@
   have "(INF n. emeasure M (A n)) = (INF n. emeasure M (A (n + i)))"
   proof (rule INF_eq)
     show "\<exists>j\<in>UNIV. emeasure M (A (j + i)) \<le> emeasure M (A i')" for i'
-      by (intro bexI[of _ i'] emeasure_mono decseqD[OF \<open>decseq A\<close>] A) auto
+      by (meson A \<open>decseq A\<close> decseq_def emeasure_mono iso_tuple_UNIV_I nat_le_iff_add)
   qed auto
   also have "\<dots> = emeasure M (INF n. (A (n + i)))"
     using A \<open>decseq A\<close> fin by (intro INF_emeasure_decseq) (auto simp: decseq_def less_top)
@@ -1118,7 +1102,7 @@
 
 text \<open>The next lemma is convenient to combine with a lemma whose conclusion is of the
 form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \<open>[symmetric]\<close> variant,
-but using \<open>AE_symmetric[OF...]\<close> will replace it.\<close>
+but using \<open>AE_symmetric[OF\<dots>]\<close> will replace it.\<close>
 
 (* depricated replace by laws about eventually *)
 lemma
@@ -1645,11 +1629,9 @@
   have "emeasure M (A \<union> B) \<noteq> \<infinity>"
     using emeasure_subadditive[OF measurable] fin by (auto simp: top_unique)
   then show "(measure M (A \<union> B)) \<le> (measure M A) + (measure M B)"
-    using emeasure_subadditive[OF measurable] fin
-    apply simp
-    apply (subst (asm) (2 3 4) emeasure_eq_ennreal_measure)
-    apply (auto simp flip: ennreal_plus)
-    done
+    unfolding measure_def
+    by (metis emeasure_subadditive[OF measurable] fin   enn2real_mono enn2real_plus 
+        ennreal_add_less_top infinity_ennreal_def less_top)
 qed
 
 lemma measure_subadditive_finite:
@@ -1672,13 +1654,13 @@
   assumes A: "range A \<subseteq> sets M" and fin: "(\<Sum>i. emeasure M (A i)) \<noteq> \<infinity>"
   shows "measure M (\<Union>i. A i) \<le> (\<Sum>i. measure M (A i))"
 proof -
-  from fin have **: "\<And>i. emeasure M (A i) \<noteq> top"
-    using ennreal_suminf_lessD[of "\<lambda>i. emeasure M (A i)"] by (simp add: less_top)
-  { have "emeasure M (\<Union>i. A i) \<le> (\<Sum>i. emeasure M (A i))"
-      using emeasure_subadditive_countably[OF A] .
-    also have "\<dots> < \<infinity>"
-      using fin by (simp add: less_top)
-    finally have "emeasure M (\<Union>i. A i) \<noteq> top" by simp }
+  have **: "\<And>i. emeasure M (A i) \<noteq> top"
+    using fin ennreal_suminf_lessD[of "\<lambda>i. emeasure M (A i)"] by (simp add: less_top)
+  have ge0: "(\<Sum>i. Sigma_Algebra.measure M (A i)) \<ge> 0"
+    using fin emeasure_eq_ennreal_measure[OF **]
+    by (metis infinity_ennreal_def measure_nonneg suminf_cong suminf_nonneg summable_suminf_not_top)
+  have "emeasure M (\<Union>i. A i) \<noteq> top"
+    by (metis A emeasure_subadditive_countably fin infinity_ennreal_def neq_top_trans)
   then have "ennreal (measure M (\<Union>i. A i)) = emeasure M (\<Union>i. A i)"
     by (rule emeasure_eq_ennreal_measure[symmetric])
   also have "\<dots> \<le> (\<Sum>i. emeasure M (A i))"
@@ -1687,11 +1669,7 @@
     using fin unfolding emeasure_eq_ennreal_measure[OF **]
     by (subst suminf_ennreal) (auto simp: **)
   finally show ?thesis
-    apply (rule ennreal_le_iff[THEN iffD1, rotated])
-    apply (intro suminf_nonneg allI measure_nonneg summable_suminf_not_top)
-    using fin
-    apply (simp add: emeasure_eq_ennreal_measure[OF **])
-    done
+    using ge0 ennreal_le_iff by blast
 qed
 
 lemma measure_Un_null_set: "A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> measure M (A \<union> B) = measure M A"
@@ -2038,11 +2016,11 @@
 
     have "emeasure M (B N) \<le> (\<Sum>n\<in>{..<N}. emeasure M (A n))"
       unfolding B_def by (rule emeasure_subadditive_finite, auto)
-    also have "... = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
+    also have "\<dots> = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
       using assms(2) by (simp add: emeasure_eq_ennreal_measure less_top)
-    also have "... = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
+    also have "\<dots> = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
       by auto
-    also have "... \<le> ennreal (\<Sum>n. measure M (A n))"
+    also have "\<dots> \<le> ennreal (\<Sum>n. measure M (A n))"
       using * by (auto simp: ennreal_leI)
     finally show ?thesis by simp
   qed
@@ -2069,9 +2047,9 @@
       have I: "(\<Union>k\<in>{n..}. A k) = (\<Union>k. A (k+n))" by (auto, metis le_add_diff_inverse2, fastforce)
       have "emeasure M (limsup A) \<le> emeasure M (\<Union>k\<in>{n..}. A k)"
         by (rule emeasure_mono, auto simp add: limsup_INF_SUP)
-      also have "... = emeasure M (\<Union>k. A (k+n))"
+      also have "\<dots> = emeasure M (\<Union>k. A (k+n))"
         using I by auto
-      also have "... \<le> (\<Sum>k. measure M (A (k+n)))"
+      also have "\<dots> \<le> (\<Sum>k. measure M (A (k+n)))"
         apply (rule emeasure_union_summable)
         using assms summable_ignore_initial_segment[OF assms(3), of n] by auto
       finally show ?thesis by simp
diff -r 947510ce4e36 -r 8a17349143df src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Dec 29 16:44:45 2022 +0100
+++ b/src/HOL/Transcendental.thy	Thu Dec 29 22:14:25 2022 +0000
@@ -5477,6 +5477,64 @@
     using that by metis
 qed
 
+lemma arccos_arctan:
+  assumes "-1 < x" "x < 1"
+  shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
+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)"
+      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"
+      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"
+      using assms
+      by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
+                    power2_eq_square square_eq_1_iff)
+  qed
+  then show ?thesis
+    by simp
+qed
+
+lemma arcsin_plus_arccos:
+  assumes "-1 \<le> x" "x \<le> 1"
+    shows "arcsin x + arccos x = pi/2"
+proof -
+  have "arcsin x = pi/2 - arccos x"
+    apply (rule sin_inj_pi)
+    using assms arcsin [OF assms] arccos [OF assms]
+    by (auto simp: algebra_simps sin_diff)
+  then show ?thesis
+    by (simp add: algebra_simps)
+qed
+
+lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
+  using arcsin_plus_arccos by force
+
+lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
+  using arcsin_plus_arccos by force
+
+lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
+  by (simp add: arccos_arctan arcsin_arccos_eq)
+
+lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
+  by (smt (verit, del_insts) arccos_cos arcsin_0 arcsin_le_arcsin arcsin_pi cos_arcsin)
+
+lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
+  using arcsin_arccos_sqrt_pos [of "-x"]
+  by (simp add: arcsin_minus)
+
+lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
+  by (smt (verit, del_insts) arccos_lbound arccos_le_pi2 arcsin_sin sin_arccos)
+
+lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
+  using arccos_arcsin_sqrt_pos [of "-x"]
+  by (simp add: arccos_minus)
+
 lemma cos_limit_1:
   assumes "(\<lambda>j. cos (\<theta> j)) \<longlonglongrightarrow> 1"
   shows "\<exists>k. (\<lambda>j. \<theta> j - of_int (k j) * (2 * pi)) \<longlonglongrightarrow> 0"