# HG changeset patch
# User desharna
# Date 1674834759 -3600
# Node ID bbe33afcfe1edee51ddd7f4e11992f2e5db392cf
# Parent  11d844d21f5cd2c16e9e6595456ffc523387642a# Parent  9678b533119e8da3458edd198943ce1fe76b4ae9
merged

diff -r 9678b533119e -r bbe33afcfe1e src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Fri Jan 27 12:25:36 2023 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Jan 27 16:52:39 2023 +0100
@@ -494,23 +494,8 @@
 lemma cos_gt_neg1:
   assumes "(t::real) \<in> {-pi<..<pi}"
   shows   "cos t > -1"
-proof -
-  have "cos t \<ge> -1"
-    by simp
-  moreover have "cos t \<noteq> -1"
-  proof
-    assume "cos t = -1"
-    then obtain n where n: "t = (2 * of_int n + 1) * pi"
-      by (subst (asm) cos_eq_minus1) auto
-    from assms have "t / pi \<in> {-1<..<1}"
-      by (auto simp: field_simps)
-    also from n have "t / pi = of_int (2 * n + 1)"
-      by auto
-    finally show False
-      by auto
-  qed
-  ultimately show ?thesis by linarith
-qed
+  using assms
+  by simp (metis cos_minus cos_monotone_0_pi cos_monotone_minus_pi_0 cos_pi linorder_le_cases)
 
 lemma dist_exp_i_1: "norm(exp(\<i> * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
 proof -