src/HOL/Analysis/Improper_Integral.thy

         using \<gamma> [OF \<open>f \<in> F\<close> tag' fine'] integral_reflect
         by (metis (mono_tags, lifting) Henstock_Kurzweil_Integration.integral_cong comp_apply split_def sum.cong)
     qed
   qed
   then show ?thesis
-    using assms by (auto simp: equiintegrable_on_def integrable_eq)
+    using assms
+    apply (auto simp: equiintegrable_on_def)
+    apply (rule integrable_eq)
+    by auto 
 qed
 
 subsection\<open>Subinterval restrictions for equiintegrable families\<close>
 
 text\<open>First, some technical lemmas about minimizing a "flat" part of a sum over a division.\<close>