# HG changeset patch
# User paulson
# Date 1663091808 -3600
# Node ID 19837257fd895a68be454b56b3041451f70cd890
# Parent  1bb677cceea44b0b09dd0f8ee20b6bab69d129d4# Parent  3190ee65139ba718a0bb09b1890a80ae079b50fb
merged

diff -r 1bb677cceea4 -r 19837257fd89 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Sep 13 11:56:38 2022 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Sep 13 18:56:48 2022 +0100
@@ -103,7 +103,7 @@
     show "(cos_coeff n + \<i> * sin_coeff n) * z^n = (\<i> * z) ^ n /\<^sub>R (fact n)"
       by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE)
   qed
-  also have "... sums (exp (\<i> * z))"
+  also have "\<dots> sums (exp (\<i> * z))"
     by (rule exp_converges)
   finally have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (exp (\<i> * z))" .
   moreover have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (cos z + \<i> * sin z)"
@@ -166,7 +166,7 @@
 proof -
   have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) = (\<lambda>n. (cnj z)^n /\<^sub>R (fact n))"
     by auto
-  also have "... sums (exp (cnj z))"
+  also have "\<dots> sums (exp (cnj z))"
     by (rule exp_converges)
   finally have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (exp (cnj z))" .
   moreover have "(\<lambda>n. cnj (z ^ n /\<^sub>R (fact n))) sums (cnj (exp z))"
@@ -234,9 +234,9 @@
 proof -
   have "exp w = exp z \<longleftrightarrow> exp (w-z) = 1"
     by (simp add: exp_diff)
-  also have "... \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
+  also have "\<dots> \<longleftrightarrow> (Re w = Re z \<and> (\<exists>n::int. Im w - Im z = of_int (2 * n) * pi))"
     by (simp add: exp_eq_1)
-  also have "... \<longleftrightarrow> ?rhs"
+  also have "\<dots> \<longleftrightarrow> ?rhs"
     by (auto simp: algebra_simps intro!: complex_eqI)
   finally show ?thesis .
 qed
@@ -250,7 +250,7 @@
 proof -
   have "exp((2 * n * pi) * \<i>) = exp 0"
     using assms unfolding Ints_def exp_eq by auto
-  also have "... = 1"
+  also have "\<dots> = 1"
     by simp
   finally show ?thesis .
 qed
@@ -266,7 +266,7 @@
     by (auto simp: Ints_def)
   have "exp(((2 * n + 1) * pi) * \<i>) = exp (pi * \<i>)"
     using assms by (subst exp_eq) (auto intro!: exI[of _ n'] simp: algebra_simps)
-  also have "... = - 1"
+  also have "\<dots> = - 1"
     by simp
   finally show ?thesis .
 qed
@@ -363,17 +363,17 @@
   qed
 qed
 
-lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * pi * n)"
-proof -
-  { assume "sin y = sin x" "cos y = cos x"
-    then have "cos (y-x) = 1"
-      using cos_add [of y "-x"] by simp
-    then have "\<exists>n::int. y-x = 2 * pi * n"
-      using cos_one_2pi_int by auto }
-  then show ?thesis
-  apply (auto simp: sin_add cos_add)
-  apply (metis add.commute diff_add_cancel)
-  done
+lemma sin_cos_eq_iff: "sin y = sin x \<and> cos y = cos x \<longleftrightarrow> (\<exists>n::int. y = x + 2 * pi * n)" (is "?L=?R")
+proof
+  assume ?L
+  then have "cos (y-x) = 1"
+    using cos_add [of y "-x"] by simp
+  then show ?R
+    by (metis cos_one_2pi_int add.commute diff_add_cancel mult.assoc mult.commute) 
+next
+  assume ?R
+  then show ?L
+    by (auto simp: sin_add cos_add)
 qed
 
 lemma exp_i_ne_1:
@@ -400,17 +400,17 @@
 
 lemma cos_eq_0:
   fixes z::complex
-  shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = of_real(n * pi) + of_real pi/2)"
+  shows "cos z = 0 \<longleftrightarrow> (\<exists>n::int. z = complex_of_real(n * pi) + of_real pi/2)"
   using sin_eq_0 [of "z - of_real pi/2"]
   by (simp add: sin_diff algebra_simps)
 
 lemma cos_eq_1:
   fixes z::complex
-  shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi))"
+  shows "cos z = 1 \<longleftrightarrow> (\<exists>n::int. z = complex_of_real(2 * n * pi))"
 proof -
   have "cos z = cos (2*(z/2))"
     by simp
-  also have "... = 1 - 2 * sin (z/2) ^ 2"
+  also have "\<dots> = 1 - 2 * sin (z/2) ^ 2"
     by (simp only: cos_double_sin)
   finally have [simp]: "cos z = 1 \<longleftrightarrow> sin (z/2) = 0"
     by simp
@@ -426,16 +426,16 @@
 
 lemma csin_eq_minus1:
   fixes z::complex
-  shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + 3/2*pi)"
+  shows "sin z = -1 \<longleftrightarrow> (\<exists>n::int. z = complex_of_real(2 * n * pi) + 3/2*pi)"
         (is "_ = ?rhs")
 proof -
   have "sin z = -1 \<longleftrightarrow> sin (-z) = 1"
     by (simp add: equation_minus_iff)
-  also have "... \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
+  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. -z = of_real(2 * n * pi) + of_real pi/2)"
     by (simp only: csin_eq_1)
-  also have "... \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
+  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. z = - of_real(2 * n * pi) - of_real pi/2)"
     by (rule iff_exI) (metis add.inverse_inverse add_uminus_conv_diff minus_add_distrib)
-  also have "... = ?rhs"
+  also have "\<dots> = ?rhs"
     apply safe
     apply (rule_tac [2] x="-(x+1)" in exI)
     apply (rule_tac x="-(x+1)" in exI)
@@ -446,7 +446,7 @@
 
 lemma ccos_eq_minus1:
   fixes z::complex
-  shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = of_real(2 * n * pi) + pi)"
+  shows "cos z = -1 \<longleftrightarrow> (\<exists>n::int. z = complex_of_real(2 * n * pi) + pi)"
   using csin_eq_1 [of "z - of_real pi/2"]
   by (simp add: sin_diff algebra_simps equation_minus_iff)
 
@@ -455,11 +455,11 @@
 proof -
   have "sin x = 1 \<longleftrightarrow> sin (complex_of_real x) = 1"
     by (metis of_real_1 one_complex.simps(1) real_sin_eq sin_of_real)
-  also have "... \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
+  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + of_real pi/2)"
     by (simp only: csin_eq_1)
-  also have "... \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
+  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + of_real pi/2)"
     by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])
-  also have "... = ?rhs"
+  also have "\<dots> = ?rhs"
     by (auto simp: algebra_simps)
   finally show ?thesis .
 qed
@@ -468,11 +468,11 @@
 proof -
   have "sin x = -1 \<longleftrightarrow> sin (complex_of_real x) = -1"
     by (metis Re_complex_of_real of_real_def scaleR_minus1_left sin_of_real)
-  also have "... \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
-    by (simp only: csin_eq_minus1)
-  also have "... \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
+  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + 3/2*pi)"
+    by (simp add: csin_eq_minus1)
+  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + 3/2*pi)"
     by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])
-  also have "... = ?rhs"
+  also have "\<dots> = ?rhs"
     by (auto simp: algebra_simps)
   finally show ?thesis .
 qed
@@ -482,11 +482,11 @@
 proof -
   have "cos x = -1 \<longleftrightarrow> cos (complex_of_real x) = -1"
     by (metis Re_complex_of_real of_real_def scaleR_minus1_left cos_of_real)
-  also have "... \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
-    by (simp only: ccos_eq_minus1)
-  also have "... \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
+  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. complex_of_real x = of_real(2 * n * pi) + pi)"
+    by (simp add: ccos_eq_minus1)
+  also have "\<dots> \<longleftrightarrow> (\<exists>n::int. x = of_real(2 * n * pi) + pi)"
     by (rule iff_exI) (auto simp: algebra_simps intro: injD [OF inj_of_real [where 'a = complex]])
-  also have "... = ?rhs"
+  also have "\<dots> = ?rhs"
     by (auto simp: algebra_simps)
   finally show ?thesis .
 qed
@@ -697,9 +697,9 @@
     by (simp add: norm_add_rule_thm)
   have "norm(1 + cos z) = cmod (1 + (exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
     by (simp add: cos_exp_eq)
-  also have "... = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
+  also have "\<dots> = cmod ((2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2)"
     by (simp add: field_simps)
-  also have "... = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
+  also have "\<dots> = cmod (2 + exp (\<i> * z) + exp (- (\<i> * z))) / 2"
     by (simp add: norm_divide)
   finally show ?thesis
     by (metis exp_eq_one_iff exp_le_cancel_iff mult_2 norm_cos_le norm_ge_zero norm_one norm_triangle_mono)
@@ -801,16 +801,16 @@
   qed
   have "cmod (sin (u *\<^sub>R z)) = cmod (exp (\<i> * (u * z)) - exp (- (\<i> * (u * z)))) / 2"
     by (auto simp: scaleR_conv_of_real norm_mult norm_power sin_exp_eq norm_divide)
-  also have "... \<le> (cmod (exp (\<i> * (u * z))) + cmod (exp (- (\<i> * (u * z)))) ) / 2"
+  also have "\<dots> \<le> (cmod (exp (\<i> * (u * z))) + cmod (exp (- (\<i> * (u * z)))) ) / 2"
     by (intro divide_right_mono norm_triangle_ineq4) simp
-  also have "... \<le> exp \<bar>Im z\<bar>"
+  also have "\<dots> \<le> exp \<bar>Im z\<bar>"
     by (rule *)
   finally show "cmod (sin (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" .
   have "cmod (cos (u *\<^sub>R z)) = cmod (exp (\<i> * (u * z)) + exp (- (\<i> * (u * z)))) / 2"
     by (auto simp: scaleR_conv_of_real norm_mult norm_power cos_exp_eq norm_divide)
-  also have "... \<le> (cmod (exp (\<i> * (u * z))) + cmod (exp (- (\<i> * (u * z)))) ) / 2"
+  also have "\<dots> \<le> (cmod (exp (\<i> * (u * z))) + cmod (exp (- (\<i> * (u * z)))) ) / 2"
     by (intro divide_right_mono norm_triangle_ineq) simp
-  also have "... \<le> exp \<bar>Im z\<bar>"
+  also have "\<dots> \<le> exp \<bar>Im z\<bar>"
     by (rule *)
   finally show "cmod (cos (u *\<^sub>R z)) \<le> exp \<bar>Im z\<bar>" .
 qed
@@ -1019,9 +1019,9 @@
   case False
   have "0 \<le> Im z \<longleftrightarrow> 0 \<le> Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
     by (metis Arg2pi_eq)
-  also have "... = (0 \<le> Im (exp (\<i> * complex_of_real (Arg2pi z))))"
+  also have "\<dots> = (0 \<le> Im (exp (\<i> * complex_of_real (Arg2pi z))))"
     using False  by (simp add: zero_le_mult_iff)
-  also have "... \<longleftrightarrow> Arg2pi z \<le> pi"
+  also have "\<dots> \<longleftrightarrow> Arg2pi z \<le> pi"
     by (simp add: Im_exp) (metis Arg2pi_ge_0 Arg2pi_lt_2pi sin_lt_zero sin_ge_zero not_le)
   finally show ?thesis
     by blast
@@ -1032,9 +1032,9 @@
   case False
   have "0 < Im z \<longleftrightarrow> 0 < Im (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
     by (metis Arg2pi_eq)
-  also have "... = (0 < Im (exp (\<i> * complex_of_real (Arg2pi z))))"
+  also have "\<dots> = (0 < Im (exp (\<i> * complex_of_real (Arg2pi z))))"
     using False by (simp add: zero_less_mult_iff)
-  also have "... \<longleftrightarrow> 0 < Arg2pi z \<and> Arg2pi z < pi" (is "_ = ?rhs")
+  also have "\<dots> \<longleftrightarrow> 0 < Arg2pi z \<and> Arg2pi z < pi" (is "_ = ?rhs")
   proof -
     have "0 < sin (Arg2pi z) \<Longrightarrow> ?rhs"
       by (meson Arg2pi_ge_0 Arg2pi_lt_2pi less_le_trans not_le sin_le_zero sin_x_le_x)
@@ -1050,9 +1050,9 @@
   case False
   have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg2pi z)))"
     by (metis Arg2pi_eq)
-  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg2pi z)))"
+  also have "\<dots> \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg2pi z)))"
     using False  by (simp add: zero_le_mult_iff)
-  also have "... \<longleftrightarrow> Arg2pi z = 0"
+  also have "\<dots> \<longleftrightarrow> Arg2pi z = 0"
   proof -
     have [simp]: "Arg2pi z = 0 \<Longrightarrow> z \<in> \<real>"
       using Arg2pi_eq [of z] by (auto simp: Reals_def)
@@ -1132,11 +1132,8 @@
 lemma Arg2pi_add:
   assumes "w \<noteq> 0" "z \<noteq> 0"
     shows "Arg2pi w + Arg2pi z = (if Arg2pi w + Arg2pi z < 2*pi then Arg2pi(w * z) else Arg2pi(w * z) + 2*pi)"
-  using assms Arg2pi_diff [of "w*z" z] Arg2pi_le_div_sum_eq [of z "w*z"]
-  apply (auto simp: Arg2pi_ge_0 Arg2pi_divide not_le)
-  apply (metis Arg2pi_lt_2pi add.commute)
-  apply (metis (no_types) Arg2pi add.commute diff_0 diff_add_cancel diff_less_eq diff_minus_eq_add not_less)
-  done
+  using assms Arg2pi_diff [of "w*z" z] Arg2pi_le_div_sum_eq [of z "w*z"] Arg2pi [of "w * z"]
+  by auto
 
 lemma Arg2pi_times:
   assumes "w \<noteq> 0" "z \<noteq> 0"
@@ -1239,7 +1236,7 @@
 proof -
   have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
     by (simp add: exp_of_real)
-  also have "... = of_real(ln z)"
+  also have "\<dots> = of_real(ln z)"
     using assms by (subst Ln_exp) auto
   finally show ?thesis
     using assms by simp
@@ -1449,7 +1446,7 @@
       by (simp_all add: field_simps norm_divide del: of_real_add)
 
     have "Re (-z) \<le> norm (-z)" by (rule complex_Re_le_cmod)
-    also from z have "... < 1" by simp
+    also from z have "\<dots> < 1" by simp
     finally have "((\<lambda>z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"
       by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
     moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
@@ -1520,11 +1517,11 @@
     apply (intro suminf_le summable_mult summable_geometric)
     apply (auto simp: norm_power field_simps simp del: of_nat_add of_nat_Suc)
     done
-  also have "... = norm z^2 * (\<Sum>i. norm z^i)" using assms
+  also have "\<dots> = norm z^2 * (\<Sum>i. norm z^i)" using assms
     by (subst suminf_mult [symmetric]) (auto intro!: summable_geometric simp: norm_mult norm_power)
   also have "(\<Sum>i. norm z^i) = inverse (1 - norm z)" using assms
     by (subst suminf_geometric) (simp_all add: divide_inverse)
-  also have "norm z^2 * ... = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)
+  also have "norm z^2 * \<dots> = norm z^2 / (1 - norm z)" by (simp add: divide_inverse)
   finally show ?thesis .
 qed
 
@@ -1620,12 +1617,10 @@
 
 text\<open>A reference to the set of positive real numbers\<close>
 lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
-by (metis Im_complex_of_real Im_exp Ln_in_Reals Re_Ln_pos_lt Re_Ln_pos_lt_imp
-          Re_complex_of_real complex_is_Real_iff exp_Ln exp_of_real pi_gt_zero)
+  using Im_Ln_pos_le Im_Ln_pos_lt Re_Ln_pos_lt by fastforce
 
 lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
-by (metis Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt add.left_neutral complex_eq less_eq_real_def
-    mult_zero_right not_less_iff_gr_or_eq pi_ge_zero pi_neq_zero rcis_zero_arg rcis_zero_mod)
+  using Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt complex.expand by fastforce
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>More Properties of Ln\<close>
@@ -1637,7 +1632,7 @@
   proof (rule exp_complex_eqI)
     have "\<bar>Im (cnj (Ln z)) - Im (Ln (cnj z))\<bar> \<le> \<bar>Im (cnj (Ln z))\<bar> + \<bar>Im (Ln (cnj z))\<bar>"
       by (rule abs_triangle_ineq4)
-    also have "... < pi + pi"
+    also have "\<dots> < pi + pi"
     proof -
       have "\<bar>Im (cnj (Ln z))\<bar> < pi"
         by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)
@@ -1661,7 +1656,7 @@
   proof (rule exp_complex_eqI)
     have "\<bar>Im (Ln (inverse z)) - Im (- Ln z)\<bar> \<le> \<bar>Im (Ln (inverse z))\<bar> + \<bar>Im (- Ln z)\<bar>"
       by (rule abs_triangle_ineq4)
-    also have "... < pi + pi"
+    also have "\<dots> < pi + pi"
     proof -
       have "\<bar>Im (Ln (inverse z))\<bar> < pi"
         by (simp add: False Im_Ln_less_pi abs_if assms minus_less_iff mpi_less_Im_Ln)
@@ -1691,8 +1686,8 @@
 lemma Ln_minus_ii [simp]: "Ln(-\<i>) = - (\<i> * pi/2)"
 proof -
   have  "Ln(-\<i>) = Ln(inverse \<i>)"    by simp
-  also have "... = - (Ln \<i>)"         using Ln_inverse by blast
-  also have "... = - (\<i> * pi/2)"     by simp
+  also have "\<dots> = - (Ln \<i>)"         using Ln_inverse by blast
+  also have "\<dots> = - (\<i> * pi/2)"     by simp
   finally show ?thesis .
 qed
 
@@ -1768,11 +1763,11 @@
     using assms complex_eq_iff complex_nonpos_Reals_iff by auto
   have "Ln(inverse z) = Ln(- (inverse (-z)))"
     by simp
-  also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
+  also have "\<dots> = Ln (inverse (-z)) + \<i> * complex_of_real pi"
     using assms z by (simp add: Ln_minus divide_less_0_iff)
-  also have "... = - Ln (- z) + \<i> * complex_of_real pi"
+  also have "\<dots> = - Ln (- z) + \<i> * complex_of_real pi"
     using z Ln_inverse by presburger
-  also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
+  also have "\<dots> = - (Ln z) + \<i> * 2 * complex_of_real pi"
     using Ln_minus assms z by auto
   finally show ?thesis by (simp add: True)
 qed
@@ -1794,9 +1789,9 @@
   shows   "Ln (of_nat m / of_nat n) = of_real (ln (of_nat m) - ln (of_nat n))"
 proof -
   have "of_nat m / of_nat n = (of_real (of_nat m / of_nat n) :: complex)" by simp
-  also from assms have "Ln ... = of_real (ln (of_nat m / of_nat n))"
+  also from assms have "Ln \<dots> = of_real (ln (of_nat m / of_nat n))"
     by (simp add: Ln_of_real[symmetric])
-  also from assms have "... = of_real (ln (of_nat m) - ln (of_nat n))"
+  also from assms have "\<dots> = of_real (ln (of_nat m) - ln (of_nat n))"
     by (simp add: ln_div)
   finally show ?thesis .
 qed
@@ -1887,13 +1882,13 @@
   proof (rule Arg2pi_unique_lemma [of "- (inverse z)"])
     have "- (inverse z) = - (inverse (of_real(norm z) * exp(\<i> * t)))"
       by (metis is_Arg_def z)
-    also have "... = (cmod (- inverse z)) * exp (\<i> * (pi - t))"
+    also have "\<dots> = (cmod (- inverse z)) * exp (\<i> * (pi - t))"
       by (auto simp: field_simps exp_diff norm_divide)
     finally show "is_Arg (- inverse z) (pi - t)"
       unfolding is_Arg_def .
     have "- (inverse z) = - (inverse (of_real(norm z) * exp(\<i> * t')))"
       by (metis is_Arg_def z')
-    also have "... = (cmod (- inverse z)) * exp (\<i> * (pi - t'))"
+    also have "\<dots> = (cmod (- inverse z)) * exp (\<i> * (pi - t'))"
       by (auto simp: field_simps exp_diff norm_divide)
     finally show "is_Arg (- inverse z) (pi - t')"
       unfolding is_Arg_def .
@@ -2125,14 +2120,14 @@
     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 "... = \<i> * (of_real(Arg2pi z) - pi)"
+  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 "... = Im (Ln (-z) - ln (cmod z)) + pi"
+  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 "... = Im (Ln (-z)) + pi"
+  also have "\<dots> = Im (Ln (-z)) + pi"
     by simp
   finally show ?thesis .
 qed
@@ -2341,7 +2336,7 @@
   hence "(-x) powr a = exp (a * ln (-of_real x))" by (simp add: powr_def)
   also from x have "ln (-of_real x) = Ln (of_real x) + of_real (sgn x) * pi * \<i>"
     by (simp add: Ln_minus Ln_of_real)
-  also from x have "exp (a * ...) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
+  also from x have "exp (a * \<dots>) = cis pi powr (of_real (sgn x) * a) * of_real x powr a"
     by (simp add: powr_def exp_add algebra_simps Ln_of_real cis_conv_exp)
   also note cis_pi
   finally show ?thesis by simp
@@ -2388,14 +2383,14 @@
     then have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within S)
                 \<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within S)"
       by simp
-    also have "... \<longleftrightarrow> ((\<lambda>z. g z ^ nat n) has_field_derivative dd') (at z within S)"
+    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)
     qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
-    also have "..." unfolding dd'_def using gderiv that
+    also have "\<dots>" unfolding dd'_def using gderiv that
       by (auto intro!: derivative_eq_intros)
     finally have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within S)" .
     then show ?thesis unfolding dd_def by simp
@@ -2413,14 +2408,14 @@
     then have "((\<lambda>z. g z powr of_int n) has_field_derivative dd) (at z within S)
                 \<longleftrightarrow> ((\<lambda>z. g z powr of_int n) has_field_derivative dd') (at z within S)"
       by simp
-    also have "... \<longleftrightarrow> ((\<lambda>z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within S)"
+    also have "\<dots> \<longleftrightarrow> ((\<lambda>z. inverse (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 = 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)
     qed (use powr_of_int \<open>g z\<noteq>0\<close> that in simp)
-    also have "..."
+    also have "\<dots>"
     proof -
       have "nat (- n) + nat (1 - n) - Suc 0 = nat (- n) + nat (- n)"
         by auto
@@ -2651,7 +2646,7 @@
       by linarith
     then have "x * 2 \<le> e * (x\<^sup>2 * (Re s)\<^sup>2)"
       using e assms x by (auto simp: power2_eq_square field_simps)
-    also have "... < e * (2 + (x * (Re s * 2) + x\<^sup>2 * (Re s)\<^sup>2))"
+    also have "\<dots> < e * (2 + (x * (Re s * 2) + x\<^sup>2 * (Re s)\<^sup>2))"
       using e assms \<open>x > 0\<close>
       by (auto simp: power2_eq_square field_simps add_pos_pos)
     finally show "0 < e * 2 + (e * Re s * 2 - 2) * x + e * (Re s)\<^sup>2 * x\<^sup>2"
@@ -2797,11 +2792,11 @@
 proof -
   have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
     by (metis exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
-  also have "... = z"
+  also have "\<dots> = z"
     using assms exp_Ln by blast
   finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)"
     by simp
-  also have "... = exp (Ln z / 2)"
+  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 )
@@ -2963,15 +2958,15 @@
       by (case_tac n rule: int_cases) (auto simp: abs_mult)
     have "exp (\<i>*z)*exp (\<i>*z) = -1 \<longleftrightarrow> exp (2*\<i>*z) = -1"
       by (metis distrib_right exp_add mult_2)
-    also have "... \<longleftrightarrow> exp (2*\<i>*z) = exp (\<i>*pi)"
+    also have "\<dots> \<longleftrightarrow> exp (2*\<i>*z) = exp (\<i>*pi)"
       using cis_conv_exp cis_pi by auto
-    also have "... \<longleftrightarrow> exp (2*\<i>*z - \<i>*pi) = 1"
+    also have "\<dots> \<longleftrightarrow> exp (2*\<i>*z - \<i>*pi) = 1"
       by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute)
-    also have "... \<longleftrightarrow> Re(\<i>*2*z - \<i>*pi) = 0 \<and> (\<exists>n::int. Im(\<i>*2*z - \<i>*pi) = of_int (2 * n) * pi)"
+    also have "\<dots> \<longleftrightarrow> Re(\<i>*2*z - \<i>*pi) = 0 \<and> (\<exists>n::int. Im(\<i>*2*z - \<i>*pi) = of_int (2 * n) * pi)"
       by (simp add: exp_eq_1)
-    also have "... \<longleftrightarrow> Im z = 0 \<and> (\<exists>n::int. 2 * Re z = of_int (2*n + 1) * pi)"
+    also have "\<dots> \<longleftrightarrow> Im z = 0 \<and> (\<exists>n::int. 2 * Re z = of_int (2*n + 1) * pi)"
       by (simp add: algebra_simps)
-    also have "... \<longleftrightarrow> False"
+    also have "\<dots> \<longleftrightarrow> False"
       using assms ge_pi2
       apply (auto simp: algebra_simps)
       by (metis abs_mult_pos not_less of_nat_less_0_iff of_nat_numeral)
@@ -3191,7 +3186,7 @@
 next
   have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))"
     by (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos field_simps power2_eq_square)
-  also have "... = x"
+  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)
@@ -3242,9 +3237,9 @@
 proof -
   have "arctan(inverse x) = arctan(inverse(tan(arctan x)))"
     by (simp add: arctan)
-  also have "... = arctan (tan (pi / 2 - arctan x))"
+  also have "\<dots> = arctan (tan (pi / 2 - arctan x))"
     by (simp add: tan_cot)
-  also have "... = pi/2 - arctan x"
+  also have "\<dots> = pi/2 - arctan x"
   proof -
     have "0 < pi - arctan x"
     using arctan_ubound [of x] pi_gt_zero by linarith
@@ -3411,7 +3406,7 @@
 proof -
   have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
     by (simp add: algebra_simps)  \<comment> \<open>Cancelling a factor of 2\<close>
-  moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
+  moreover have "\<dots> \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
     by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral)
   ultimately show ?thesis
     apply (simp add: sin_exp_eq Arcsin_def Arcsin_body_lemma exp_minus divide_simps)
@@ -3442,14 +3437,14 @@
 proof -
   have "Arcsin(sin z) = - (\<i> * Ln (csqrt (1 - (\<i> * (exp (\<i>*z) - inverse (exp (\<i>*z))))\<^sup>2 / 4) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
     by (simp add: sin_exp_eq Arcsin_def exp_minus power_divide)
-  also have "... = - (\<i> * Ln (csqrt (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2)\<^sup>2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
+  also have "\<dots> = - (\<i> * Ln (csqrt (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2)\<^sup>2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
     by (simp add: field_simps power2_eq_square)
-  also have "... = - (\<i> * Ln (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
+  also have "\<dots> = - (\<i> * Ln (((exp (\<i>*z) + inverse (exp (\<i>*z)))/2) - (inverse (exp (\<i>*z)) - exp (\<i>*z)) / 2))"
     apply (subst csqrt_square)
     using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma by auto
-  also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
+  also have "\<dots> =  - (\<i> * Ln (exp (\<i>*z)))"
     by (simp add: field_simps power2_eq_square)
-  also have "... = z"
+  also have "\<dots> = z"
     using assms by (auto simp: abs_if simp del: eq_divide_eq_numeral1 split: if_split_asm)
   finally show ?thesis .
 qed
@@ -3566,7 +3561,7 @@
 proof -
   have "z*2 + \<i> * (2 * csqrt (1 - z\<^sup>2)) = 0 \<longleftrightarrow> z*2 + \<i> * csqrt (1 - z\<^sup>2)*2 = 0"
     by (simp add: algebra_simps)  \<comment> \<open>Cancelling a factor of 2\<close>
-  moreover have "... \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0"
+  moreover have "\<dots> \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0"
     by (metis distrib_right mult_eq_0_iff zero_neq_numeral)
   ultimately show ?thesis
     by (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps flip: power2_eq_square)
@@ -3585,14 +3580,14 @@
   then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
                            \<i> * csqrt (((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2)))"
     by (simp add: cos_exp_eq Arccos_def exp_minus power_divide)
-  also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
+  also have "\<dots> = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
                               \<i> * ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))))"
     apply (subst csqrt_square)
     using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z]
     by (auto simp: * Re_sin Im_sin)
-  also have "... =  - (\<i> * Ln (exp (\<i>*z)))"
+  also have "\<dots> =  - (\<i> * Ln (exp (\<i>*z)))"
     by (simp add: field_simps power2_eq_square)
-  also have "... = z"
+  also have "\<dots> = z"
     using assms
     by (subst Complex_Transcendental.Ln_exp, auto)
   finally show ?thesis .
@@ -3676,7 +3671,7 @@
   have "(Im (Arccos w))\<^sup>2 \<le> (cmod (cos (Arccos w)))\<^sup>2 - (cos (Re (Arccos w)))\<^sup>2"
     using norm_cos_squared [of "Arccos w"] real_le_abs_sinh [of "Im (Arccos w)"]
     by (simp only: abs_le_square_iff) (simp add: field_split_simps)
-  also have "... \<le> (cmod w)\<^sup>2"
+  also have "\<dots> \<le> (cmod w)\<^sup>2"
     by (auto simp: cmod_power2)
   finally show ?thesis
     using abs_le_square_iff by force
@@ -3975,7 +3970,7 @@
   have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arcsin (Re x))) =
         continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arcsin (of_real (Re x)))))"
     by (rule continuous_on_cong [OF refl]) (simp add: arcsin_eq_Re_Arcsin)
-  also have "... = ?thesis"
+  also have "\<dots> = ?thesis"
     by (rule continuous_on_cong [OF refl]) simp
   finally show ?thesis
     using continuous_on_arcsin [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
@@ -4001,7 +3996,7 @@
   have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arccos (Re x))) =
         continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arccos (of_real (Re x)))))"
     by (rule continuous_on_cong [OF refl]) (simp add: arccos_eq_Re_Arccos)
-  also have "... = ?thesis"
+  also have "\<dots> = ?thesis"
     by (rule continuous_on_cong [OF refl]) simp
   finally show ?thesis
     using continuous_on_arccos [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
@@ -4037,15 +4032,7 @@
   fixes j::nat
   assumes "n \<noteq> 0"
     shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
-proof -
-  have *: "of_nat j * (complex_of_real pi * 2) = complex_of_real (2 * real j * pi)"
-    by (simp)
-  then show ?thesis
-    apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler)
-    apply (simp only: * cos_of_real sin_of_real)
-    apply simp
-    done
-qed
+  by (metis assms bot_nat_0.not_eq_extremum exp_divide_power_eq exp_of_nat2_mult exp_two_pi_i power_one)
 
 lemma complex_root_unity_eq:
   fixes j::nat and k::nat
@@ -4058,13 +4045,13 @@
           (\<exists>z::int. of_nat j * (\<i> * (of_real pi * 2)) =
               (of_nat k + of_nat n * of_int z) * (\<i> * (of_real pi * 2)))"
       by (simp add: algebra_simps)
-    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))"
+    also have "\<dots> \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))"
       by simp
-    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
+    also have "\<dots> \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
       by (metis (mono_tags, opaque_lifting) of_int_add of_int_eq_iff of_int_mult of_int_of_nat_eq)
-    also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
+    also have "\<dots> \<longleftrightarrow> int j mod int n = int k mod int n"
       by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps)
-    also have "... \<longleftrightarrow> j mod n = k mod n"
+    also have "\<dots> \<longleftrightarrow> j mod n = k mod n"
       by (metis of_nat_eq_iff zmod_int)
     finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
              \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow> j mod n = k mod n" .
diff -r 1bb677cceea4 -r 19837257fd89 src/HOL/Analysis/Polytope.thy
--- a/src/HOL/Analysis/Polytope.thy	Tue Sep 13 11:56:38 2022 +0200
+++ b/src/HOL/Analysis/Polytope.thy	Tue Sep 13 18:56:48 2022 +0100
@@ -82,16 +82,16 @@
     then have zne: "\<And>u. \<lbrakk>u \<in> {0<..<1}; (1 - u) *\<^sub>R y + u *\<^sub>R x \<in> T\<rbrakk> \<Longrightarrow> False"
       using \<open>x \<in> S\<close> \<open>x \<notin> T\<close> \<open>T face_of S\<close> unfolding face_of_def
       by (meson greaterThanLessThan_iff in_segment(2))
-    have in01: "min (1/2) (e / norm (x - y)) \<in> {0<..<1}"
-      using \<open>y \<noteq> x\<close> \<open>e > 0\<close> by simp
-    have \<section>: "norm (min (1/2) (e / norm (x - y)) *\<^sub>R y - min (1/2) (e / norm (x - y)) *\<^sub>R x) \<le> e"
+    define u where "u \<equiv> min (1/2) (e / norm (x - y))"
+    have in01: "u \<in> {0<..<1}"
+      using \<open>y \<noteq> x\<close> \<open>e > 0\<close> by (simp add: u_def)
+    have "norm (u *\<^sub>R y - u *\<^sub>R x) \<le> e"
       using \<open>e > 0\<close>
-        by (simp add: scaleR_diff_right [symmetric] norm_minus_commute min_mult_distrib_right)
-    show False
-      apply (rule zne [OF in01 e [THEN subsetD]])
-      using \<open>y \<in> T\<close>
-        apply (simp add: hull_inc mem_affine x)
-        by (simp add: dist_norm algebra_simps \<section>)
+      by (simp add: u_def norm_minus_commute min_mult_distrib_right flip: scaleR_diff_right)
+    then have "dist y ((1 - u) *\<^sub>R y + u *\<^sub>R x) \<le> e"
+      by (simp add: dist_norm algebra_simps)
+    then show False
+      using zne [OF in01 e [THEN subsetD]] by (simp add: \<open>y \<in> T\<close> hull_inc mem_affine x)
   qed
   show ?thesis
   proof (rule subset_antisym)
@@ -187,8 +187,8 @@
       by (simp add: divide_simps) (simp add: algebra_simps)
     have "b \<in> open_segment d c"
       apply (simp add: open_segment_image_interval)
-      apply (simp add: d_def algebra_simps image_def)
-      apply (rule_tac x="e / (e + norm (b - c))" in bexI)
+      apply (simp add: d_def algebra_simps)
+      apply (rule_tac x="e / (e + norm (b - c))" in image_eqI)
       using False nbc \<open>0 < e\<close> by (auto simp: algebra_simps)
     then have "d \<in> T \<and> c \<in> T"
       by (meson \<open>b \<in> T\<close> \<open>c \<in> u\<close> \<open>d \<in> u\<close> assms face_ofD subset_iff)
@@ -244,8 +244,9 @@
   proof (cases "T = {}")
     case True then show ?thesis
       by (metis aff_dim_empty \<open>T \<noteq> S\<close>)
-  next case False then show ?thesis
-    by (metis Set.set_insert assms convex_rel_frontier_aff_dim dual_order.irrefl face_of_imp_convex face_of_subset_rel_frontier insert_not_empty subsetI)
+  next 
+    case False then show ?thesis
+      by (smt (verit) aff_dim_empty assms convex_rel_frontier_aff_dim face_of_imp_convex face_of_subset_rel_frontier)
   qed
   ultimately show ?thesis
     by simp
@@ -262,10 +263,10 @@
 qed
 
 lemma affine_hull_face_of_disjoint_rel_interior:
-    fixes S :: "'a::euclidean_space set"
+  fixes S :: "'a::euclidean_space set"
   assumes "convex S" "F face_of S" "F \<noteq> S"
   shows "affine hull F \<inter> rel_interior S = {}"
-  by (metis assms disjnt_def face_of_imp_subset order_refl subset_antisym subset_of_face_of_affine_hull)
+  by (meson antisym assms disjnt_def equalityD2 face_of_def subset_of_face_of_affine_hull)
 
 lemma affine_diff_divide:
     assumes "affine S" "k \<noteq> 0" "k \<noteq> 1" and xy: "x \<in> S" "y /\<^sub>R (1 - k) \<in> S"
@@ -312,14 +313,12 @@
       have a0: "a i = 0" if "i \<in> (S - T)" for i
         using ci0 [OF that] u01 a [of i] b [of i] that
         by (simp add: c_def Groups.ordered_comm_monoid_add_class.add_nonneg_eq_0_iff)
-      have [simp]: "sum a T = 1"
+      have  "sum a T = 1"
         using assms by (metis sum.mono_neutral_cong_right a0 asum)
-      show ?thesis
-        apply (simp add: convex_hull_finite \<open>finite T\<close>)
-        apply (rule_tac x=a in exI)
-        using a0 assms
-        apply (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right)
-        done
+      moreover have "(\<Sum>x\<in>T. a x *\<^sub>R x) = x"
+        using a0 assms by (auto simp: cge0 a aeqx [symmetric] sum.mono_neutral_right)
+      ultimately show ?thesis
+        using a assms(2) by (auto simp add: convex_hull_finite \<open>finite T\<close> )
     next
       case False
       define k where "k = sum c (S - T)"
@@ -332,38 +331,34 @@
         case True
         then have "sum c T = 0"
           by (simp add: S k_def sum_diff sumc1)
-        then have [simp]: "sum c (S - T) = 1"
+        then have "sum c (S - T) = 1"
           by (simp add: S sum_diff sumc1)
-        have ci0: "\<And>i. i \<in> T \<Longrightarrow> c i = 0"
+        moreover have ci0: "\<And>i. i \<in> T \<Longrightarrow> c i = 0"
           by (meson \<open>finite T\<close> \<open>sum c T = 0\<close> \<open>T \<subseteq> S\<close> cge0 sum_nonneg_eq_0_iff subsetCE)
-        then have [simp]: "(\<Sum>i\<in>S-T. c i *\<^sub>R i) = w"
+        then have "(\<Sum>i\<in>S-T. c i *\<^sub>R i) = w"
           by (simp add: weq_sumsum)
-        have "w \<in> convex hull (S - T)"
-          apply (simp add: convex_hull_finite fin)
-          apply (rule_tac x=c in exI)
-          apply (auto simp: cge0 weq True k_def)
-          done
+        ultimately have "w \<in> convex hull (S - T)"
+          using cge0 by (auto simp add: convex_hull_finite fin)
         then show ?thesis
           using disj waff by blast
       next
         case False
         then have sumcf: "sum c T = 1 - k"
           by (simp add: S k_def sum_diff sumc1)
-        have ge0: "\<And>x. x \<in> T \<Longrightarrow> 0 \<le> inverse (1 - k) * c x"
+        have "\<And>x. x \<in> T \<Longrightarrow> 0 \<le> inverse (1 - k) * c x"
           by (metis \<open>T \<subseteq> S\<close> cge0 inverse_nonnegative_iff_nonnegative mult_nonneg_nonneg subsetD sum_nonneg sumcf)
-        have eq1: "(\<Sum>x\<in>T. inverse (1 - k) * c x) = 1"
+        moreover have "(\<Sum>x\<in>T. inverse (1 - k) * c x) = 1"
           by (metis False eq_iff_diff_eq_0 mult.commute right_inverse sum_distrib_left sumcf)
-        have "(\<Sum>i\<in>T. c i *\<^sub>R i) /\<^sub>R (1 - k) \<in> convex hull T"
+        ultimately have "(\<Sum>i\<in>T. c i *\<^sub>R i) /\<^sub>R (1 - k) \<in> convex hull T"
           apply (simp add: convex_hull_finite fin)
-          apply (rule_tac x="\<lambda>i. inverse (1-k) * c i" in exI)
-          by (metis (mono_tags, lifting) eq1 ge0 scaleR_scaleR scale_sum_right sum.cong)
+          by (metis (mono_tags, lifting) scaleR_right.sum scaleR_scaleR sum.cong)
         with \<open>0 < k\<close>  have "inverse(k) *\<^sub>R (w - sum (\<lambda>i. c i *\<^sub>R i) T) \<in> affine hull T"
           by (simp add: affine_diff_divide [OF affine_affine_hull] False waff convex_hull_subset_affine_hull [THEN subsetD])
         moreover have "inverse(k) *\<^sub>R (w - sum (\<lambda>x. c x *\<^sub>R x) T) \<in> convex hull (S - T)"
           apply (simp add: weq_sumsum convex_hull_finite fin)
           apply (rule_tac x="\<lambda>i. inverse k * c i" in exI)
           using \<open>k > 0\<close> cge0
-          apply (auto simp: scaleR_right.sum sum_distrib_left [symmetric] k_def [symmetric])
+          apply (auto simp: scaleR_right.sum simp flip: sum_distrib_left k_def)
           done
         ultimately show ?thesis
           using disj by blast
@@ -402,12 +397,9 @@
       case True with \<open>a \<in> T\<close> show ?thesis by auto
     next
       case False
-      then have "a \<noteq> 2 *\<^sub>R a - b"
-        by (simp add: scaleR_2)
-        with False have "a \<in> open_segment (2 *\<^sub>R a - b) b"
-        apply (clarsimp simp: open_segment_def closed_segment_def)
-        apply (rule_tac x="1/2" in exI)
-          by (simp add: algebra_simps)
+      then have "a \<in> open_segment (2 *\<^sub>R a - b) b"
+        by (metis diff_add_cancel inverse_eq_divide midpoint_def midpoint_in_open_segment 
+            scaleR_2 scaleR_half_double)
       moreover have "2 *\<^sub>R a - b \<in> S"
         by (rule mem_affine [OF \<open>affine S\<close> \<open>a \<in> S\<close> \<open>b \<in> S\<close>, of 2 "-1", simplified])
       moreover note \<open>b \<in> S\<close> \<open>a \<in> T\<close>
@@ -648,10 +640,12 @@
          T face_of S \<and> (\<exists>a b. S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b})"
 
 lemma empty_exposed_face_of [iff]: "{} exposed_face_of S"
-  apply (simp add: exposed_face_of_def)
-  apply (rule_tac x=0 in exI)
-  apply (rule_tac x=1 in exI, force)
-  done
+proof -
+  have "S \<subseteq> {x. 0 \<bullet> x \<le> 1} \<and> {} = S \<inter> {x. 0 \<bullet> x = 1}"
+    by force
+  then show ?thesis
+    using exposed_face_of_def by blast
+qed
 
 lemma exposed_face_of_refl_eq [simp]: "S exposed_face_of S \<longleftrightarrow> convex S"
 proof
@@ -671,9 +665,6 @@
      (T = {} \<or> T = S \<or>
       (\<exists>a b. a \<noteq> 0 \<and> S \<subseteq> {x. a \<bullet> x \<le> b} \<and> T = S \<inter> {x. a \<bullet> x = b}))"
 proof (cases "T = {}")
-  case True then show ?thesis
-    by simp
-next
   case False
   show ?thesis
   proof (cases "T = S")
@@ -686,7 +677,7 @@
       apply (metis inner_zero_left)
       done
   qed
-qed
+qed auto
 
 lemma exposed_face_of_Int_supporting_hyperplane_le:
    "\<lbrakk>convex S; \<And>x. x \<in> S \<Longrightarrow> a \<bullet> x \<le> b\<rbrakk> \<Longrightarrow> (S \<inter> {x. a \<bullet> x = b}) exposed_face_of S"
@@ -713,13 +704,10 @@
     using T teq u ueq by (simp add: face_of_Int)
   have ss: "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'}"
     using S s' by (force simp: inner_left_distrib)
-  show ?thesis
-    apply (simp add: exposed_face_of_def tu)
-    apply (rule_tac x="a+a'" in exI)
-    apply (rule_tac x="b+b'" in exI)
-    using S s'
-    apply (fastforce simp: ss inner_left_distrib teq ueq)
-    done
+  have "S \<subseteq> {x. (a + a') \<bullet> x \<le> b + b'} \<and> T \<inter> u = S \<inter> {x. (a + a') \<bullet> x = b + b'}"
+    using S s' by (fastforce simp: ss inner_left_distrib teq ueq)
+  then show ?thesis
+    using exposed_face_of_def tu by auto
 qed
 
 proposition exposed_face_of_Inter:
@@ -2568,15 +2556,16 @@
           using \<open>h \<in> F\<close> F_def face_of_disjoint_rel_interior hface by auto
       qed
     qed
-    have "S \<subseteq> affine hull S \<inter> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}"
+    let ?S' = "affine hull S \<inter> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F}"
+    have "S \<subseteq> ?S'"
       using ab by (auto simp: hull_subset)
-    moreover have "affine hull S \<inter> \<Inter>{{x. a h \<bullet> x \<le> b h} |h. h \<in> F} \<subseteq> S"
+    moreover have "?S' \<subseteq> S"
       using * by blast
-    ultimately have "S = affine hull S \<inter> \<Inter> {{x. a h \<bullet> x \<le> b h} |h. h \<in> F}" ..
-    then show ?thesis
-      apply (rule ssubst)
-      apply (force intro: polyhedron_affine_hull polyhedron_halfspace_le simp: \<open>finite F\<close>)
-      done
+    ultimately have "S = ?S'" ..
+    moreover have "polyhedron ?S'"
+      by (force intro: polyhedron_affine_hull polyhedron_halfspace_le simp: \<open>finite F\<close>)
+    ultimately show ?thesis
+      by auto
   qed
 qed
 
@@ -2599,19 +2588,22 @@
   assumes "linear h" "bij h"
     shows "polyhedron (h ` S) \<longleftrightarrow> polyhedron S"
 proof -
-  have *: "{f. P f} = (image h) ` {f. P (h ` f)}" for P
-    apply safe
-    apply (rule_tac x="inv h ` x" in image_eqI)
-    apply (auto simp: \<open>bij h\<close> bij_is_surj image_f_inv_f)
-    done
-  have "inj h" using bij_is_inj assms by blast
+  have [simp]: "inj h" using bij_is_inj assms by blast
   then have injim: "inj_on ((`) h) A" for A
     by (simp add: inj_on_def inj_image_eq_iff)
-  show ?thesis
-    using \<open>linear h\<close> \<open>inj h\<close>
-    apply (simp add: polyhedron_eq_finite_faces closed_injective_linear_image_eq)
-    apply (simp add: * face_of_linear_image [of h _ S, symmetric] finite_image_iff injim)
-    done
+  { fix P
+    have "\<And>x. P x \<Longrightarrow> x \<in> (`) h ` {f. P (h ` f)}" 
+      using bij_is_surj [OF \<open>bij h\<close>]
+      by (metis image_eqI mem_Collect_eq subset_imageE top_greatest)
+    then have "{f. P f} = (image h) ` {f. P (h ` f)}"
+      by force
+  } 
+  then have "finite {F. F face_of h ` S} =finite {F. F face_of S}"
+    using \<open>linear h\<close> 
+    by (simp add: finite_image_iff injim flip: face_of_linear_image [of h _ S])
+  then show ?thesis
+    using \<open>linear h\<close> 
+    by (simp add: polyhedron_eq_finite_faces closed_injective_linear_image_eq)
 qed
 
 lemma polyhedron_negations:
@@ -2814,8 +2806,7 @@
     have x: "x < ?n * a"
       by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
     have "?n * a \<le> a + x"
-      apply (simp add: algebra_simps)
-      by (metis assms(2) floor_divide_lower mult.commute)
+      using \<open>a>0\<close> by (simp add: distrib_right floor_divide_lower)
     also have "... < y"
       by (rule 1)
     finally have "?n * a < y" .
@@ -2827,8 +2818,7 @@
     have y: "y < ?n * a"
       by (meson \<open>0 < a\<close> divide_less_eq floor_eq_iff)
     have "?n * a \<le> a + y"
-      apply (simp add: algebra_simps)
-      by (metis assms(2) floor_divide_lower mult.commute)
+      using \<open>a>0\<close> by (simp add: distrib_right floor_divide_lower)
     also have "... < x"
       by (rule 2)
     finally have "?n * a < x" .
@@ -3064,8 +3054,7 @@
   by (metis simplex add.commute add_diff_cancel_left' aff_dim_convex_hull affine_independent_iff_card)
 
 lemma zero_simplex_sing: "0 simplex {a}"
-  apply (simp add: simplex_def)
-  using affine_independent_1 card_1_singleton_iff convex_hull_singleton by blast
+  using affine_independent_1 simplex_convex_hull by fastforce
 
 lemma simplex_sing [simp]: "n simplex {a} \<longleftrightarrow> n = 0"
   using aff_dim_simplex aff_dim_sing zero_simplex_sing by blast
diff -r 1bb677cceea4 -r 19837257fd89 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Sep 13 11:56:38 2022 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Sep 13 18:56:48 2022 +0100
@@ -610,11 +610,7 @@
 lemma ennreal_minus_cancel:
   fixes a b c :: ennreal
   shows "c \<noteq> top \<Longrightarrow> a \<le> c \<Longrightarrow> b \<le> c \<Longrightarrow> c - a = c - b \<Longrightarrow> a = b"
-  apply transfer
-  subgoal for a b c
-    by (cases a b c rule: ereal3_cases)
-       (auto simp: top_ereal_def max_def split: if_splits)
-  done
+  by (metis ennreal_add_diff_cancel_left ennreal_add_diff_cancel_right ennreal_add_eq_top less_eqE)
 
 lemma sup_const_add_ennreal:
   fixes a b c :: "ennreal"
@@ -624,19 +620,14 @@
 lemma ennreal_diff_add_assoc:
   fixes a b c :: ennreal
   shows "a \<le> b \<Longrightarrow> c + b - a = c + (b - a)"
-  apply transfer
-  subgoal for a b c
-    by (cases a b c rule: ereal3_cases) (auto simp: field_simps max_absorb2)
-  done
+  by (metis add.left_commute ennreal_add_diff_cancel_left ennreal_add_eq_top ennreal_top_minus less_eqE)
 
 lemma mult_divide_eq_ennreal:
   fixes a b :: ennreal
   shows "b \<noteq> 0 \<Longrightarrow> b \<noteq> top \<Longrightarrow> (a * b) / b = a"
   unfolding divide_ennreal_def
   apply transfer
-  apply (subst mult.assoc)
-  apply (simp add: top_ereal_def flip: divide_ereal_def)
-  done
+  by (metis abs_ereal_ge0 divide_ereal_def ereal_divide_eq ereal_times_divide_eq top_ereal_def)
 
 lemma divide_mult_eq: "a \<noteq> 0 \<Longrightarrow> a \<noteq> \<infinity> \<Longrightarrow> x * a / (b * a) = x / (b::ennreal)"
   unfolding divide_ennreal_def infinity_ennreal_def
@@ -650,17 +641,12 @@
 lemma ennreal_mult_divide_eq:
   fixes a b :: ennreal
   shows "b \<noteq> 0 \<Longrightarrow> b \<noteq> top \<Longrightarrow> (a * b) / b = a"
-  unfolding divide_ennreal_def
-  apply transfer
-  apply (subst mult.assoc)
-  apply (simp add: top_ereal_def flip: divide_ereal_def)
-  done
+  by (fact mult_divide_eq_ennreal)
 
 lemma ennreal_add_diff_cancel:
   fixes a b :: ennreal
   shows "b \<noteq> \<infinity> \<Longrightarrow> (a + b) - b = a"
-  unfolding infinity_ennreal_def
-  by transfer (simp add: max_absorb2 top_ereal_def ereal_add_diff_cancel)
+  by simp
 
 lemma ennreal_minus_eq_0:
   "a - b = 0 \<Longrightarrow> a \<le> (b::ennreal)"
@@ -792,14 +778,10 @@
   by transfer (meson ereal_minus_mono max.mono order_refl)
 
 lemma ennreal_minus_eq_top[simp]: "a - (b::ennreal) = top \<longleftrightarrow> a = top"
-  by transfer (auto simp: top_ereal_def max.absorb2 ereal_minus_eq_PInfty_iff split: split_max)
+  by (metis add_top diff_add_cancel_ennreal ennreal_mono_minus ennreal_top_minus zero_le)
 
 lemma ennreal_divide_self[simp]: "a \<noteq> 0 \<Longrightarrow> a < top \<Longrightarrow> a / a = (1::ennreal)"
-  unfolding divide_ennreal_def
-  apply transfer
-  subgoal for a
-    by (cases a) (auto simp: top_ereal_def)
-  done
+  by (metis mult_1 mult_divide_eq_ennreal top.not_eq_extremum)
 
 subsection \<open>Coercion from \<^typ>\<open>real\<close> to \<^typ>\<open>ennreal\<close>\<close>
 
@@ -808,7 +790,8 @@
 
 declare [[coercion ennreal]]
 
-lemma ennreal_cong: "x = y \<Longrightarrow> ennreal x = ennreal y" by simp
+lemma ennreal_cong: "x = y \<Longrightarrow> ennreal x = ennreal y" 
+  by simp
 
 lemma ennreal_cases[cases type: ennreal]:
   fixes x :: ennreal
@@ -892,7 +875,7 @@
   by (cases "0 \<le> x") (auto simp: ennreal_neg simp flip: ennreal_1)
 
 lemma one_less_ennreal[simp]: "1 < ennreal x \<longleftrightarrow> 1 < x"
-  by transfer (auto simp: max.absorb2 less_max_iff_disj)
+  by (meson ennreal_le_1 linorder_not_le)
 
 lemma ennreal_plus[simp]:
   "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> ennreal (a + b) = ennreal a + ennreal b"
@@ -992,17 +975,11 @@
     by (cases "n = 0") auto
 next
   case (real r) then show ?thesis
-  proof cases
-    assume "x = 0" then show ?thesis
-      using power_eq_top_ennreal[of top "n - 1"]
-      by (cases n) (auto simp: ennreal_top_mult)
-  next
-    assume "x \<noteq> 0"
-    with real have "0 < r" by auto
-    with real show ?thesis
-      by (induction n)
-         (auto simp add: ennreal_power ennreal_mult[symmetric] inverse_ennreal)
-  qed
+  proof (cases "x = 0")
+    case False then show ?thesis
+      by (smt (verit, best) ennreal_0 ennreal_power inverse_ennreal 
+               inverse_nonnegative_iff_nonnegative power_inverse real zero_less_power)
+  qed (simp add: top_power_ennreal)
 qed
 
 lemma power_divide_distrib_ennreal [algebra_simps]:
@@ -1547,12 +1524,8 @@
   fixes f :: "nat \<Rightarrow> ennreal"
   shows "(\<And>n. f n \<le> c) \<Longrightarrow> liminf (\<lambda>n. c - f n) = c - limsup f"
   apply transfer
-  apply (simp add: ereal_diff_positive max.absorb2 liminf_ereal_cminus)
-  apply (subst max.absorb2)
-  apply (rule ereal_diff_positive)
-  apply (rule Limsup_bounded)
-  apply auto
-  done
+  apply (simp add: ereal_diff_positive liminf_ereal_cminus)
+  by (metis max.absorb2 ereal_diff_positive Limsup_bounded eventually_sequentiallyI)
 
 lemma ennreal_continuous_on_cmult:
   "(c::ennreal) < top \<Longrightarrow> continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. c * f x)"
@@ -1606,7 +1579,6 @@
 
 lemma ennreal_Inf_countable_INF:
   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ennreal. decseq f \<and> range f \<subseteq> A \<and> Inf A = (INF i. f i)"
-  including ennreal.lifting
   unfolding decseq_def
   apply transfer
   subgoal for A
@@ -1655,9 +1627,7 @@
   shows "I \<noteq> {} \<Longrightarrow> (SUP i\<in>I. f i + c) = (SUP i\<in>I. f i) + c"
   apply transfer
   apply (simp add: SUP_ereal_add_left)
-  apply (subst (1 2) max.absorb2)
-  apply (auto intro: SUP_upper2 add_nonneg_nonneg)
-  done
+  by (metis SUP_upper all_not_in_conv ereal_le_add_mono1 max.absorb2 max.bounded_iff)
 
 lemma ennreal_SUP_const_minus:
   fixes f :: "'a \<Rightarrow> ennreal"
@@ -1689,13 +1659,9 @@
 
     fix t assume \<open>open t \<and> ennreal_of_enat x \<in> t\<close>
     then have \<open>\<exists>y<\<infinity>. {y <.. \<infinity>} \<subseteq> t\<close>
-      apply (rule_tac open_left[where y=0])
-      by (auto simp: True)
+      by (rule_tac open_left[where y=0]) (auto simp: True)
     then obtain y where \<open>{y<..} \<subseteq> t\<close> and \<open>y \<noteq> \<infinity>\<close>
-      apply atomize_elim
-      apply (auto simp: greaterThanAtMost_def)
-      by (metis atMost_iff inf.orderE subsetI top.not_eq_extremum top_greatest)
-
+      by fastforce
     from \<open>y \<noteq> \<infinity>\<close>
     obtain x' where x'y: \<open>ennreal_of_enat x' > y\<close> and \<open>x' \<noteq> \<infinity>\<close>
       by (metis enat.simps(3) ennreal_Ex_less_of_nat ennreal_of_enat_enat infinity_ennreal_def top.not_eq_extremum)
@@ -1907,9 +1873,7 @@
 lemma add_diff_eq_ennreal:
   fixes x y z :: ennreal
   shows "z \<le> y \<Longrightarrow> x + (y - z) = x + y - z"
-  including ennreal.lifting
-  by transfer
-     (insert add_mono[of "0::ereal"], auto simp add: ereal_diff_positive max.absorb2 add_diff_eq_ereal)
+  using ennreal_diff_add_assoc by auto
 
 lemma add_diff_inverse_ennreal:
   fixes x y :: ennreal shows "x \<le> y \<Longrightarrow> x + (y - x) = y"
@@ -2035,11 +1999,8 @@
   fixes f g :: "_ \<Rightarrow> ennreal"
   assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
   shows "(SUP i\<in>I. f i + g i) = (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
-proof cases
-  assume "I = {}" then show ?thesis
-    by (simp add: bot_ereal_def)
-next
-  assume "I \<noteq> {}"
+proof (cases "I = {}")
+  case False
   show ?thesis
   proof (rule antisym)
     show "(SUP i\<in>I. f i + g i) \<le> (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
@@ -2053,7 +2014,8 @@
       using directed by (intro SUP_least) (blast intro: SUP_upper2)
     finally show "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) \<le> (SUP i\<in>I. f i + g i)" .
   qed
-qed
+qed (simp add: bot_ereal_def)
+
 
 lemma enn2real_eq_0_iff: "enn2real x = 0 \<longleftrightarrow> x = 0 \<or> x = top"
   by (cases x) auto