diff -r da8a0e7bcac8 -r 9a60c1759543 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Jan 30 15:24:25 2023 +0000
+++ b/src/HOL/Complex.thy	Tue Jan 31 14:05:16 2023 +0000
@@ -214,8 +214,14 @@
   finally show ?thesis .
 qed
 
+lemma surj_Re: "surj Re"
+  by (metis Re_complex_of_real surj_def)
+
+lemma surj_Im: "surj Im"
+  by (metis complex.sel(2) surj_def)
+
 lemma complex_Im_fact [simp]: "Im (fact n) = 0"
-  by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat)
+  by (metis complex_Im_of_nat of_nat_fact)
 
 lemma Re_prod_Reals: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> \<real>) \<Longrightarrow> Re (prod f A) = prod (\<lambda>x. Re (f x)) A"
 proof (induction A rule: infinite_finite_induct)
@@ -279,6 +285,9 @@
 lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
   by (metis mult.commute power2_i power_mult)
 
+lemma i_even_power' [simp]: "even n \<Longrightarrow> \<i> ^ n = (-1) ^ (n div 2)"
+  by (metis dvd_mult_div_cancel power2_i power_mult)
+
 lemma Re_i_times [simp]: "Re (\<i> * z) = - Im z"
   by simp
 
@@ -1065,6 +1074,12 @@
     using pi_not_less_zero by linarith
 qed auto
 
+lemma cos_Arg: "z \<noteq> 0 \<Longrightarrow> cos (Arg z) = Re z / norm z"
+  by (metis Re_sgn cis.sel(1) cis_Arg)
+
+lemma sin_Arg: "z \<noteq> 0 \<Longrightarrow> sin (Arg z) = Im z / norm z"
+  by (metis Im_sgn cis.sel(2) cis_Arg)
+
 subsection \<open>Complex n-th roots\<close>
 
 lemma bij_betw_roots_unity: