--- a/src/HOL/Series.thy Tue Dec 22 23:36:32 2020 +0100
+++ b/src/HOL/Series.thy Wed Dec 23 16:25:52 2020 +0000
@@ -614,7 +614,7 @@
lemma suminf_geometric: "norm c < 1 \<Longrightarrow> suminf (\<lambda>n. c^n) = 1 / (1 - c)"
by (rule sums_unique[symmetric]) (rule geometric_sums)
-lemma summable_geometric_iff: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
+lemma summable_geometric_iff [simp]: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
proof
assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)"
then have "(\<lambda>n. norm c ^ n) \<longlonglongrightarrow> 0"
--- a/src/HOL/Transcendental.thy Tue Dec 22 23:36:32 2020 +0100
+++ b/src/HOL/Transcendental.thy Wed Dec 23 16:25:52 2020 +0000
@@ -1886,10 +1886,8 @@
next
fix x :: real
assume "x \<in> {- 1<..<1}"
- then have "norm (-x) < 1" by auto
- show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
- unfolding One_nat_def
- by (auto simp: power_mult_distrib[symmetric] summable_geometric[OF \<open>norm (-x) < 1\<close>])
+ then show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
+ by (simp add: abs_if flip: power_mult_distrib)
qed
then have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
unfolding One_nat_def by auto