src/HOL/Analysis/Complex_Transcendental.thy

 
 lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
 proof (cases w rule: complex_split_polar)
   case (1 r a) with sin_cos_le1 [of a \<phi>] show ?thesis
     apply (simp add: norm_mult cmod_unit_one)
-    by (metis (no_types, hide_lams) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
+    by (metis (no_types, opaque_lifting) abs_le_D1 distrib_left mult.commute mult.left_commute mult_left_le)
 qed
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Analytic properties of tangent function\<close>
 
 lemma cnj_tan: "cnj(tan z) = tan(cnj z)"

     have "0 \<notin> V"
       by (meson exp_not_eq_zero hom homeomorphism_def)
     then have "\<And>y. y \<in> V \<Longrightarrow> g' y = inv ((*) y)"
       by (metis exp_Ln g' g_eq_Ln)
     then have g': "g' z = (\<lambda>x. x/z)"
-      by (metis (no_types, hide_lams) bij \<open>z \<in> V\<close> bij_inv_eq_iff exp_Ln g_eq_Ln nonzero_mult_div_cancel_left znz)
+      by (metis (no_types, opaque_lifting) bij \<open>z \<in> V\<close> bij_inv_eq_iff exp_Ln g_eq_Ln nonzero_mult_div_cancel_left znz)
     show "(g has_derivative (*) (inverse z)) (at z)"
       using g [OF \<open>z \<in> V\<close>] g'
       by (simp add: \<open>z \<in> V\<close> field_class.field_divide_inverse has_derivative_imp_has_field_derivative has_field_derivative_imp_has_derivative)
   qed (auto simp: \<open>z \<in> V\<close> \<open>open V\<close>)
 qed

               (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))"
       by simp
     also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
-      by (metis (mono_tags, hide_lams) of_int_add of_int_eq_iff of_int_mult of_int_of_nat_eq)
+      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"
       by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps)
     also have "... \<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)) =