--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Tue May 24 16:21:49 2022 +0100
@@ -30,7 +30,7 @@
Mg': "set_borel_measurable borel {a..b} g'"
by (simp_all only: set_measurable_continuous_on_ivl)
from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
- by (simp only: has_field_derivative_iff_has_vector_derivative)
+ by (simp only: has_real_derivative_iff_has_vector_derivative)
have real_ind[simp]: "\<And>A x. enn2real (indicator A x) = indicator A x"
by (auto split: split_indicator)
@@ -73,7 +73,7 @@
hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow>
(g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
by (simp only: u'v' max_absorb2 min_absorb1)
- (auto simp: has_field_derivative_iff_has_vector_derivative)
+ (auto simp: has_real_derivative_iff_has_vector_derivative)
have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))