src/HOL/Library/Extended_Real.thy

     have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
       by simp
     also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
       by (subst sum.reindex) auto
     also have "\<dots> \<le> sum f {..<n + k}"
-      by (intro sum_mono3) (auto simp: f)
+      by (intro sum_mono2) (auto simp: f)
     finally show "(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}" .
   qed
 qed
 
 lemma sums_suminf_ereal: "f sums x \<Longrightarrow> (\<Sum>i. ereal (f i)) = ereal x"