src/HOL/Probability/Probability_Measure.thy

       using prob_space by (simp add: X)
     also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
       using \<open>x \<in> I\<close> \<open>open I\<close> X(2)
       apply (intro integral_mono_AE integrable_add integrable_mult_right integrable_diff
                 integrable_const X q)
-      apply (elim eventually_elim1)
+      apply (elim eventually_mono)
       apply (intro convex_le_Inf_differential)
       apply (auto simp: interior_open q)
       done
     finally show "k \<le> expectation (\<lambda>w. q (X w))" using x by auto
   qed