src/HOL/Analysis/Complex_Transcendental.thy

   by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
 
 lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
 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>
+    by (simp add: algebra_simps)  \<comment> \<open>Cancelling a factor of 2\<close>
   moreover have "... \<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)
     apply (simp add: algebra_simps)

   by (blast intro: isCont_o2 [OF _ isCont_Arccos])
 
 lemma cos_Arccos [simp]: "cos(Arccos z) = z"
 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>
+    by (simp add: algebra_simps)  \<comment> \<open>Cancelling a factor of 2\<close>
   moreover have "... \<longleftrightarrow> z + \<i> * csqrt (1 - z\<^sup>2) = 0"
     by (metis distrib_right mult_eq_0_iff zero_neq_numeral)
   ultimately show ?thesis
     apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps)
     apply (simp add: power2_eq_square [symmetric])