src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

       if inp: "(x, l) \<in> p" "(y, m) \<in> p" and ne: "(x, l) \<noteq> (y, m)" and "l = m" for x l y m
     proof -
       obtain u v where uv: "l = cbox u v"
         using inp p'(4) by blast
       have "content (cbox u v) = 0"
-        unfolding content_eq_0_interior using that p(1) uv by auto
+        unfolding content_eq_0_interior using that p(1) uv
+        by (auto dest: tagged_partial_division_ofD)
       then show ?thesis
         using uv by blast
     qed
     then have "(\<Sum>(x, K)\<in>p. integral K f) = (\<Sum>K\<in>snd ` p. integral K f)"
       apply (subst sum.reindex_nontrivial [OF \<open>finite p\<close>])

     and tag: "p tagged_partial_division_of (cbox a b)"
     and "d fine p"
   shows "sum (\<lambda>(x,k). norm (content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (DIM('n)) * e"
 proof -
   have "finite p"
-    using tag by blast
+    using tag tagged_partial_division_ofD by blast
   then show ?thesis
     unfolding split_def
   proof (rule sum_norm_allsubsets_bound)
     fix Q
     assume Q: "Q \<subseteq> p"