MacLaurin.patch

diff -r f274b63c5b44 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Sat Dec 06 23:51:17 2025 +0100
+++ b/src/HOL/MacLaurin.thy	Wed Dec 17 17:39:06 2025 +0900
@@ -12,14 +12,6 @@
 
 subsection \<open>Maclaurin's Theorem with Lagrange Form of Remainder\<close>
 
-text \<open>This is a very long, messy proof even now that it's been broken down
-  into lemmas.\<close>
-
-lemma Maclaurin_lemma:
-  "0 < h \<Longrightarrow>
-    \<exists>B::real. f h = (\<Sum>m<n. (j m / (fact m)) * (h^m)) + (B * ((h^n) /(fact n)))"
-  by (rule exI[where x = "(f h - (\<Sum>m<n. (j m / (fact m)) * h^m)) * (fact n) / (h^n)"]) simp
-
 lemma eq_diff_eq': "x = y - z \<longleftrightarrow> y = x + z"
   for x y z :: real
   by arith
@@ -27,41 +19,6 @@
 lemma fact_diff_Suc: "n < Suc m \<Longrightarrow> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
   by (subst fact_reduce) auto
 
-lemma Maclaurin_lemma2:
-  fixes B
-  assumes DERIV: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-    and INIT: "n = Suc k"
-  defines "difg \<equiv>
-    (\<lambda>m t::real. diff m t -
-      ((\<Sum>p<n - m. diff (m + p) 0 / fact p * t ^ p) + B * (t ^ (n - m) / fact (n - m))))"
-    (is "difg \<equiv> (\<lambda>m t. diff m t - ?difg m t)")
-  shows "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
-proof (rule allI impI)+
-  fix m t
-  assume INIT2: "m < n \<and> 0 \<le> t \<and> t \<le> h"
-  have "DERIV (difg m) t :> diff (Suc m) t -
-    ((\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / fact x) +
-     real (n - m) * t ^ (n - Suc m) * B / fact (n - m))"
-    by (auto simp: difg_def intro!: derivative_eq_intros DERIV[rule_format, OF INIT2])
-  moreover
-  from INIT2 have intvl: "{..<n - m} = insert 0 (Suc ` {..<n - Suc m})" and "0 < n - m"
-    unfolding atLeast0LessThan[symmetric] by auto
-  have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / fact x) =
-      (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x))"
-    unfolding intvl by (subst sum.insert) (auto simp: sum.reindex)
-  moreover
-  have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
-    by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2
-        less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff)
-  have "\<And>x. (Suc x) * t ^ x * diff (Suc m + x) 0 / fact (Suc x) = diff (Suc m + x) 0 * t^x / fact x"
-    by (rule nonzero_divide_eq_eq[THEN iffD2]) auto
-  moreover
-  have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))"
-    using \<open>0 < n - m\<close> by (simp add: field_split_simps fact_reduce)
-  ultimately show "DERIV (difg m) t :> difg (Suc m) t"
-    unfolding difg_def  by (simp add: mult.commute)
-qed
-
 lemma Maclaurin:
   assumes h: "0 < h"
     and n: "0 < n"
@@ -69,74 +26,74 @@
     and diff_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   shows
     "\<exists>t::real. 0 < t \<and> t < h \<and>
-      f h = sum (\<lambda>m. (diff m 0 / fact m) * h ^ m) {..<n} + (diff n t / fact n) * h ^ n"
+      f h = (\<Sum>m<n. diff m 0 / fact m * h^m) + diff n t / fact n * h^n"
 proof -
-  from n obtain m where m: "n = Suc m"
-    by (cases n) (simp add: n)
-  from m have "m < n" by simp
 
-  obtain B where f_h: "f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + B * (h ^ n / fact n)"
-    using Maclaurin_lemma [OF h] ..
-
-  define g where [abs_def]: "g t =
-    f t - (sum (\<lambda>m. (diff m 0 / fact m) * t^m) {..<n} + B * (t^n / fact n))" for t
-  have g2: "g 0 = 0" "g h = 0"
-    by (simp_all add: m f_h g_def lessThan_Suc_eq_insert_0 image_iff diff_0 sum.reindex)
+  define B where "B = (f h - (\<Sum>m<n. diff m 0 / fact m * h^m)) * fact n / h^n"  
 
   define difg where [abs_def]: "difg m t =
-    diff m t - (sum (\<lambda>p. (diff (m + p) 0 / fact p) * (t ^ p)) {..<n-m} +
-      B * ((t ^ (n - m)) / fact (n - m)))" for m t
-  have difg_0: "difg 0 = g"
-    by (simp add: difg_def g_def diff_0)
-  have difg_Suc: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
-    using diff_Suc m unfolding difg_def [abs_def] by (rule Maclaurin_lemma2)
-  have difg_eq_0: "\<forall>m<n. difg m 0 = 0"
-    by (auto simp: difg_def m Suc_diff_le lessThan_Suc_eq_insert_0 image_iff sum.reindex)
-  have isCont_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> isCont (difg m) x"
-    by (rule DERIV_isCont [OF difg_Suc [rule_format]]) simp
-  have differentiable_difg: "\<And>m x. m < n \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> h \<Longrightarrow> difg m differentiable (at x)"
-    using difg_Suc real_differentiable_def by auto
-  have difg_Suc_eq_0:
-    "\<And>m t. m < n \<Longrightarrow> 0 \<le> t \<Longrightarrow> t \<le> h \<Longrightarrow> DERIV (difg m) t :> 0 \<Longrightarrow> difg (Suc m) t = 0"
-    by (rule DERIV_unique [OF difg_Suc [rule_format]]) simp
+    diff m t - (\<Sum>p<n-m. diff (m + p) 0 / fact p * t^p) -
+    B * (t ^ (n - m) / fact (n - m))" for m t
 
-  have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0"
-  using \<open>m < n\<close>
+  have difg_Suc: "DERIV (difg m) t :> difg (Suc m) t"
+    if mn: "m < n" and t0: "0 \<le> t" and th: "t \<le> h" for m t
+  proof-
+    have "DERIV (difg m) t :>
+      diff (Suc m) t -
+      (\<Sum>x \<in> {..< n - m}. real x * t ^ (x - 1) * diff (m + x) 0 / fact x) -
+      real (n - m) * t ^ (n - Suc m) * B / fact (n - m)"
+      by (auto simp: difg_def intro!: derivative_eq_intros diff_Suc[rule_format] mn t0 th)
+    also from mn have "{..< n - m} = insert 0 (Suc ` {..< n - Suc m})"
+      unfolding atLeast0LessThan[symmetric] by auto
+    also have "(\<Sum>x \<in> \<dots>. real x * t ^ (x - 1) * diff (m + x) 0 / fact x) =
+        (\<Sum>x < n - Suc m. (1 + real x) * t ^ x * diff (m + 1 + x) 0 / fact (Suc x))"
+      by (subst sum.insert) (auto simp: sum.reindex)
+    also have "\<dots> = (\<Sum>x < n - Suc m. diff (m + 1 + x) 0 * t^x / fact x)"
+      by (rule sum.cong) (simp_all add: nonzero_divide_eq_eq)
+    also have "(n - m) * t ^ (n - Suc m) * B / fact (n - m) = B * (t ^ (n - Suc m) / fact (n - Suc m))"
+      using mn by (simp add: field_split_simps fact_reduce)
+    finally show "DERIV (difg m) t :> difg (Suc m) t"
+      by (simp add: difg_def)
+  qed
+
+  have myRolle: "\<exists>t. 0 < t \<and> t < h' \<and> DERIV (difg m) t :> 0"
+    if mn: "m < n" and eq: "difg m 0 = difg m h'" and h'0: "0 < h'" and h'h: "h' \<le> h" for m h'
+  proof (intro Rolle[OF h'0 eq])
+    show "continuous_on {0..h'} (difg m)"
+      using mn h'h by (auto intro!: continuous_at_imp_continuous_on DERIV_isCont[OF difg_Suc])
+    fix x assume x0: "0 < x" and xh': "x < h'"
+    with h'h have "0 \<le> x" "x \<le> h" by auto
+    from difg_Suc[OF mn this]
+    show "difg m differentiable (at x)"
+      by (auto simp: real_differentiable_def)
+  qed
+  from n obtain m where nm: "n = Suc m" by (auto simp: gr0_conv_Suc)
+  then have "m < n" by simp
+  then have "\<exists>t. 0 < t \<and> t < h \<and> DERIV (difg m) t :> 0"
   proof (induct m)
     case 0
-    show ?case
-    proof (rule Rolle)
-      show "0 < h" by fact
-      show "difg 0 0 = difg 0 h"
-        by (simp add: difg_0 g2)
-      show "continuous_on {0..h} (difg 0)"
-        by (simp add: continuous_at_imp_continuous_on isCont_difg n)
-    qed (simp add: differentiable_difg n)
+    from n have "difg 0 0 = difg 0 h" by (auto simp: difg_def B_def diff_0)
+    with n h show ?case
+      by (auto intro!: myRolle)
   next
-    case (Suc m')
-    then obtain t where t: "0 < t" "t < h" "DERIV (difg m') t :> 0"
-      by force
-    have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m')) t' :> 0"
-    proof (rule Rolle)
-      show "0 < t" by fact
-      show "difg (Suc m') 0 = difg (Suc m') t"
-        using t \<open>Suc m' < n\<close> by (simp add: difg_Suc_eq_0 difg_eq_0)
-      have "\<And>x. 0 \<le> x \<and> x \<le> t \<Longrightarrow> isCont (difg (Suc m')) x"
-        using \<open>t < h\<close> \<open>Suc m' < n\<close> by (simp add: isCont_difg)
-      then show "continuous_on {0..t} (difg (Suc m'))"
-        by (simp add: continuous_at_imp_continuous_on)
-    qed (use \<open>t < h\<close> \<open>Suc m' < n\<close> in \<open>simp add: differentiable_difg\<close>)
-    with \<open>t < h\<close> show ?case
+    case (Suc m)
+    from Suc have dSm0: "difg (Suc m) 0 = 0"
+      by (auto simp: difg_def)
+    from Suc obtain t where t0: "0 < t" and th: "t < h" and mt: "DERIV (difg m) t :> 0"
+      by auto
+    from t0 th DERIV_unique[OF difg_Suc mt] Suc
+    have "difg (Suc m) 0 = difg (Suc m) t"
+      by (auto simp: dSm0)
+    with t0 th \<open>Suc m < n\<close>
+    have "\<exists>t'. 0 < t' \<and> t' < t \<and> DERIV (difg (Suc m)) t' :> 0"
+      by (auto intro!: myRolle)
+    with th show ?case
       by auto
   qed
-  then obtain t where "0 < t" "t < h" "difg (Suc m) t = 0"
-    using \<open>m < n\<close> difg_Suc_eq_0 by force
-  show ?thesis
-  proof (intro exI conjI)
-    show "0 < t" "t < h" by fact+
-    show "f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / (fact n) * h ^ n"
-      using \<open>difg (Suc m) t = 0\<close> by (simp add: m f_h difg_def)
-  qed
+  from this nm DERIV_unique[OF difg_Suc]
+  obtain t where "0 < t" "t < h" "difg n t = 0"
+    by auto
+  then show ?thesis by (auto simp: B_def difg_def)
 qed
 
 lemma Maclaurin2:
@@ -145,7 +102,7 @@
   assumes INIT1: "0 < h"
     and INIT2: "diff 0 = f"
     and DERIV: "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-  shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / fact n * h ^ n"
+  shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n"
 proof (cases n)
   case 0
   with INIT1 INIT2 show ?thesis by fastforce
@@ -189,7 +146,7 @@
   fixes n :: nat and x :: real
   assumes "diff 0 = f"
     and DERIV : "\<forall>m t. m < n \<and> \<bar>t\<bar> \<le> \<bar>x\<bar> \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) + diff n t / (fact n) * x ^ n"
+  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> f x = (\<Sum>m<n. diff m 0 / fact m * x ^ m) + diff n t / fact n * x ^ n"
     (is "\<exists>t. _ \<and> f x = ?f x t")
 proof (cases "n = 0")
   case True
@@ -279,12 +236,12 @@
   fixes x :: real and n :: nat
   shows
     "x \<noteq> 0 \<Longrightarrow> n > 0 \<Longrightarrow>
-      (\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n)"
+      (\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. x ^ m / fact m) + exp t / fact n * x ^ n)"
  using Maclaurin_all_lt [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
 
 lemma Maclaurin_exp_le:
   fixes x :: real and n :: nat
-  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n"
+  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. x ^ m / fact m) + exp t / fact n * x ^ n"
   using Maclaurin_all_le_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
 
 corollary exp_lower_Taylor_quadratic: "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
@@ -303,70 +260,52 @@
 
 text \<open>It is unclear why so many variant results are needed.\<close>
 
-lemma sin_expansion_lemma: "sin (x + real (Suc m) * pi / 2) = cos (x + real m * pi / 2)"
+lemma sin_expansion_lemma: "sin (x + (1 + real m) * pi / 2) = cos (x + real m * pi / 2)"
   by (auto simp: cos_add sin_add add_divide_distrib distrib_right)
 
+lemma sin_coeff_lemma: "sin_coeff m * x ^ m = sin (1 / 2 * real m * pi) / fact m * x ^ m"
+  by (cases "even m") (auto simp: sin_zero_iff sin_coeff_def elim!: oddE)
+
 lemma Maclaurin_sin_expansion2:
   "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
-    sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
-proof (cases "n = 0 \<or> x = 0")
-  case False
+    sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + sin (t + 1/2 * real n * pi) / fact n * x ^ n"
+proof-
   let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"
-  have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> sin x =
+  have "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> sin x =
       (\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n"
-  proof (rule Maclaurin_all_lt)
-    show "\<forall>m x. ((\<lambda>t. sin (t + 1/2 * real m * pi)) has_real_derivative
-           sin (x + 1/2 * real (Suc m) * pi)) (at x)"
-      by (rule allI derivative_eq_intros | use sin_expansion_lemma in force)+
-  qed (use False in auto)
+    apply (rule Maclaurin_all_le)
+    by (auto simp: sin_expansion_lemma intro!: derivative_eq_intros)
   then show ?thesis
-    apply (rule ex_forward, simp)
-    apply (rule sum.cong[OF refl])
-    apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
-    done
-qed auto
+    by (simp add: sin_coeff_lemma)
+qed
 
 lemma Maclaurin_sin_expansion:
-  "\<exists>t. sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
+  "\<exists>t. sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + sin (t + 1/2 * real n * pi) / fact n * x ^ n"
   using Maclaurin_sin_expansion2 [of x n] by blast
 
 lemma Maclaurin_sin_expansion3:
   assumes "n > 0" "x > 0"
     shows "\<exists>t. 0 < t \<and> t < x \<and>
-          sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
+          sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + sin (t + 1/2 * real n * pi) / fact n * x ^ n"
 proof -
   let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"
-  have "\<exists>t. 0 < t \<and> t < x \<and> sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
-  proof (rule Maclaurin)
-    show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
-                ((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative
-                 sin (t + 1/2 * real (Suc m) * pi)) (at t)"
-      using DERIV_shift sin_expansion_lemma by fastforce
-  qed (use assms in auto)
+  have "\<exists>t. 0 < t \<and> t < x \<and> sin x = (\<Sum>m<n. ?diff m 0 / fact m * x ^ m) + ?diff n t / fact n * x ^ n"
+    apply (rule Maclaurin)
+    by (auto intro!: derivative_eq_intros simp: assms sin_expansion_lemma)
   then show ?thesis
-    apply (rule ex_forward, simp)
-    apply (rule sum.cong[OF refl])
-    apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
-    done
+    by (simp add: sin_coeff_lemma)
 qed
 
 lemma Maclaurin_sin_expansion4:
   assumes "0 < x"
-  shows "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
+  shows "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + sin (t + 1/2 * real n * pi) / fact n * x ^ n"
 proof -
   let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"
-  have "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
-  proof (rule Maclaurin2)
-    show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
-                ((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative
-                 sin (t + 1/2 * real (Suc m) * pi)) (at t)"
-      using DERIV_shift sin_expansion_lemma by fastforce
-  qed (use assms in auto)
+  have "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. ?diff m 0 / fact m * x ^ m) + ?diff n t / fact n * x ^ n"
+    apply (rule Maclaurin2)
+    by (auto intro!: derivative_eq_intros simp: assms sin_expansion_lemma)
   then show ?thesis
-    apply (rule ex_forward, simp)
-    apply (rule sum.cong[OF refl])
-    apply (auto simp: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
-    done
+    by (simp add: sin_coeff_lemma)
 qed
 
 
@@ -375,68 +314,49 @@
 lemma sumr_cos_zero_one [simp]: "(\<Sum>m<Suc n. cos_coeff m * 0 ^ m) = 1"
   by (induct n) auto
 
-lemma cos_expansion_lemma: "cos (x + real (Suc m) * pi / 2) = - sin (x + real m * pi / 2)"
+lemma cos_expansion_lemma: "cos (x + (1 + real m) * pi / 2) = - sin (x + real m * pi / 2)"
   by (auto simp: cos_add sin_add distrib_right add_divide_distrib)
 
+lemma cos_coeff_lemma: "cos_coeff m * x ^ m  = cos (1 / 2 * real m * pi) / fact m * x ^ m"
+  by (cases "even m") (auto simp add: cos_coeff_def cos_zero_iff)
+
 lemma Maclaurin_cos_expansion:
   "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
-    cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos(t + 1/2 * real n * pi) / fact n) * x ^ n"
-proof (cases "n = 0 \<or> x = 0")
-  case False
+    cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + cos(t + 1/2 * real n * pi) / fact n * x ^ n"
+proof-
   let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"
-  have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> cos x =
-      (\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n"
-  proof (rule Maclaurin_all_lt)
-    show "\<forall>m x. ((\<lambda>t. cos (t + 1/2 * real m * pi)) has_real_derivative
-           cos (x + 1/2 * real (Suc m) * pi)) (at x)"
-      using cos_expansion_lemma
-      by (intro allI derivative_eq_intros | simp)+
-  qed (use False in auto)
+  have "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and> cos x =
+      (\<Sum>m<n. ?diff m 0 / fact m * x ^ m) + ?diff n t / fact n * x ^ n"
+    apply (rule Maclaurin_all_le)
+    by (simp_all add: cos_expansion_lemma)
   then show ?thesis
-    apply (rule ex_forward, simp)
-    apply (rule sum.cong[OF refl])
-    apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE simp del: of_nat_Suc)
-    done
-qed auto
+    by (simp add: cos_coeff_lemma)
+qed
 
 lemma Maclaurin_cos_expansion2:
   assumes "x > 0" "n > 0"
   shows "\<exists>t. 0 < t \<and> t < x \<and>
-      cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos (t + 1/2 * real n * pi) / fact n) * x ^ n"
+      cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + cos (t + 1/2 * real n * pi) / fact n * x ^ n"
 proof -
   let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"
-  have "\<exists>t. 0 < t \<and> t < x \<and> cos x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
-  proof (rule Maclaurin)
-    show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
-              ((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative 
-               cos (t + 1 / 2 * real (Suc m) * pi)) (at t)"
-      by (simp add: cos_expansion_lemma del: of_nat_Suc)
-  qed (use assms in auto)
+  have "\<exists>t. 0 < t \<and> t < x \<and> cos x = (\<Sum>m<n. ?diff m 0 / fact m * x ^ m) + ?diff n t / fact n * x ^ n"
+    apply (rule Maclaurin)
+    by (simp_all add: cos_expansion_lemma assms)
   then show ?thesis
-    apply (rule ex_forward, simp)
-    apply (rule sum.cong[OF refl])
-    apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
-    done
+    by (simp add: cos_coeff_lemma)
 qed
 
 lemma Maclaurin_minus_cos_expansion:
   assumes "n > 0" "x < 0"
   shows "\<exists>t. x < t \<and> t < 0 \<and>
-         cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + ((cos (t + 1/2 * real n * pi) / fact n) * x ^ n)"
+         cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + cos (t + 1/2 * real n * pi) / fact n * x ^ n"
 proof -
   let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"
-  have "\<exists>t. x < t \<and> t < 0 \<and> cos x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
-  proof (rule Maclaurin_minus)
-    show "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow>
-              ((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative 
-               cos (t + 1 / 2 * real (Suc m) * pi)) (at t)"
-      by (simp add: cos_expansion_lemma del: of_nat_Suc)
-  qed (use assms in auto)
+  have "\<exists>t. x < t \<and> t < 0 \<and> cos x = (\<Sum>m<n. ?diff m 0 / fact m * x ^ m) + ?diff n t / fact n * x ^ n"
+    apply (rule Maclaurin_minus)
+    by (simp_all add: assms cos_expansion_lemma)
   then show ?thesis
-    apply (rule ex_forward, simp)
-    apply (rule sum.cong[OF refl])
-    apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
-    done
+    by (simp add: cos_coeff_lemma)
 qed
 
 
diff -r f274b63c5b44 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sat Dec 06 23:51:17 2025 +0100
+++ b/src/HOL/Transcendental.thy	Wed Dec 17 17:39:06 2025 +0900
@@ -3547,8 +3547,9 @@
         using \<open>n \<le> p\<close> neq0_conv that(1) by blast
       then have \<section>: "(- 1::real) ^ (p div 2 - Suc 0) = - ((- 1) ^ (p div 2))"
         using \<open>even p\<close> by (auto simp add: dvd_def power_eq_if)
-      from \<open>n \<le> p\<close> np have *: "n - Suc 0 + (p - Suc n) = p - Suc (Suc 0)" "Suc (Suc 0) \<le> p"
-        by arith+
+      from \<open>n \<le> p\<close> np have *: "n - Suc 0 + (p - Suc n) = p - Suc (Suc 0)"
+        (* by arith somehow takes forever when exporting proofs *)
+        by (metis Nat.add_diff_assoc add.commute diff_Suc_diff_eq1 diff_diff_cancel le0 le_antisym nat_le_linear not_less_eq_eq odd_Suc_minus_one)
       have "(p - Suc (Suc 0)) div 2 = p div 2 - Suc 0"
         by simp
       with \<open>n \<le> p\<close> np  \<section> * show ?thesis
@@ -4445,7 +4446,7 @@
 
 subsection \<open>More Corollaries about Sine and Cosine\<close>
 
-lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi/2) = (-1) ^ n"
+lemma sin_cos_npi [simp]: "sin ((1 + 2 * real n) * pi/2) = (-1) ^ n"
 proof -
   have "sin ((real n + 1/2) * pi) = cos (real n * pi)"
     by (auto simp: algebra_simps sin_add)
@@ -4479,7 +4480,7 @@
   finally show ?thesis .
 qed
 
-lemma cos_pi_eq_zero [simp]: "cos (pi * real (Suc (2 * m)) / 2) = 0"
+lemma cos_pi_eq_zero [simp]: "cos (pi * (1 + 2 * real m) / 2) = 0"
   by (simp only: cos_add sin_add of_nat_Suc distrib_right distrib_left add_divide_distrib, auto)
 
 lemma DERIV_cos_add [simp]: "DERIV (\<lambda>x. cos (x + k)) xa :> - sin (xa + k)"