src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy

   assume A: "\<forall>a\<in>A. closed a" "\<forall>B\<subseteq>A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" "U \<inter> \<Inter>A = {}"
   define F where "F = (INF a:insert U A. principal a)"
   have "F \<noteq> bot"
     unfolding F_def
   proof (rule INF_filter_not_bot)
-    fix X assume "X \<subseteq> insert U A" "finite X"
-    moreover with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
+    fix X
+    assume X: "X \<subseteq> insert U A" "finite X"
+    with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
       by auto
-    ultimately show "(INF a:X. principal a) \<noteq> bot"
+    with X show "(INF a:X. principal a) \<noteq> bot"
       by (auto simp add: INF_principal_finite principal_eq_bot_iff)
   qed
   moreover
   have "F \<le> principal U"
     unfolding F_def by auto

       assume "x \<notin> X"
       have "x \<in> closure X" using Y by auto
       then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
         by (auto simp: closure_sequential)
       from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
-      have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
+      have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
         by (auto simp: set_mp extension)
-      moreover
       then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
         using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
         by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
-      ultimately have "h x = y x" by (rule LIMSEQ_unique)
+      with hx have "h x = y x" by (rule LIMSEQ_unique)
     } then
     have "h x = ?g x"
       using extension by auto
   }
   ultimately show ?thesis ..