# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1674827872 0
# Node ID 11d844d21f5cd2c16e9e6595456ffc523387642a
# Parent  780161d4b55c4199b767065af97e0e76791808bd
Shortened a messy proof

diff -r 780161d4b55c -r 11d844d21f5c src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Jan 26 13:59:51 2023 +0000
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Fri Jan 27 13:57:52 2023 +0000
@@ -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 -