src/HOL/Probability/Measure_Space.thy

     using I \<open>finite I\<close> by (intro antisym INF_lower INF_greatest F emeasure_mono) auto
   ultimately show ?thesis
     by simp
 next
   assume "infinite I"
-  def L \<equiv> "\<lambda>n. LEAST i. i \<in> I \<and> i \<ge> n"
+  define L where "L n = (LEAST i. i \<in> I \<and> i \<ge> n)" for n
   have L: "L n \<in> I \<and> n \<le> L n" for n
     unfolding L_def
   proof (rule LeastI_ex)
     show "\<exists>x. x \<in> I \<and> n \<le> x"
       using \<open>infinite I\<close> finite_subset[of I "{..< n}"]