src/HOL/Cardinals/Wellorder_Constructions.thy

      and IH1b: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g ` under r a1 = under s (g a1)"
      and IH2: "\<And> a1. a1 \<in> underS r a \<Longrightarrow> g a1 \<in> under s (f a1)"
      unfolding underS_def Field_def bij_betw_def by auto
      have fa: "f a \<in> Field s" using f[OF a] by auto
      have g: "g a = suc s (g ` underS r a)"
-     using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by simp
+       using r.worec_fixpoint[OF adm] unfolding g_def fun_eq_iff by blast
      have A0: "g ` underS r a \<subseteq> Field s"
      using IH1b by (metis IH2 image_subsetI in_mono under_Field)
      {fix a1 assume a1: "a1 \<in> underS r a"
       from IH2[OF this] have "g a1 \<in> under s (f a1)" .
       moreover have "f a1 \<in> underS s (f a)" using f[OF a] a1 by auto