diff -r 295609359b58 -r ce92360f0692 src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Wed Nov 06 11:08:10 2019 +0100
+++ b/src/HOL/Library/Ramsey.thy	Fri Nov 08 16:07:22 2019 +0000
@@ -161,11 +161,7 @@
 text \<open>For induction, we decrease the value of \<^term>\<open>r\<close> in partitions.\<close>
 lemma part_Suc_imp_part:
   "\<lbrakk>infinite Y; part (Suc r) s Y f; y \<in> Y\<rbrakk> \<Longrightarrow> part r s (Y - {y}) (\<lambda>u. f (insert y u))"
-  apply (simp add: part_def)
-  apply clarify
-  apply (drule_tac x="insert y X" in spec)
-  apply force
-  done
+  by (simp add: part_def subset_Diff_insert)
 
 lemma part_subset: "part r s YY f \<Longrightarrow> Y \<subseteq> YY \<Longrightarrow> part r s Y f"
   unfolding part_def by blast
@@ -356,11 +352,13 @@
 text \<open>To be equal to the union of some well-founded relations is equivalent
   to being the subset of such a union.\<close>
 lemma disj_wf: "disj_wf r \<longleftrightarrow> (\<exists>T. \<exists>n::nat. (\<forall>i<n. wf(T i)) \<and> r \<subseteq> (\<Union>i<n. T i))"
-  apply (auto simp add: disj_wf_def)
-  apply (rule_tac x="\<lambda>i. T i Int r" in exI)
-  apply (rule_tac x=n in exI)
-  apply (force simp add: wf_Int1)
-  done
+proof -
+  have *: "\<And>T n. \<lbrakk>\<forall>i<n. wf (T i); r \<subseteq> \<Union> (T ` {..<n})\<rbrakk>
+           \<Longrightarrow> (\<forall>i<n. wf (T i \<inter> r)) \<and> r = (\<Union>i<n. T i \<inter> r)"
+    by (force simp add: wf_Int1)
+  show ?thesis
+    unfolding disj_wf_def by auto (metis "*")
+qed
 
 theorem trans_disj_wf_implies_wf:
   assumes "trans r"
@@ -384,12 +382,10 @@
     qed
     then show ?thesis by (auto simp add: r)
   qed
-  have trless: "i \<noteq> j \<Longrightarrow> transition_idx s T {i, j} < n" for i j
-    apply (auto simp add: linorder_neq_iff)
-     apply (blast dest: s_in_T transition_idx_less)
-    apply (subst insert_commute)
-    apply (blast dest: s_in_T transition_idx_less)
-    done
+  have "i < j \<Longrightarrow> transition_idx s T {i, j} < n" for i j
+    using s_in_T transition_idx_less by blast
+  then have trless: "i \<noteq> j \<Longrightarrow> transition_idx s T {i, j} < n" for i j
+    by (metis doubleton_eq_iff less_linear)
   have "\<exists>K k. K \<subseteq> UNIV \<and> infinite K \<and> k < n \<and>
       (\<forall>i\<in>K. \<forall>j\<in>K. i \<noteq> j \<longrightarrow> transition_idx s T {i, j} = k)"
     by (rule Ramsey2) (auto intro: trless infinite_UNIV_nat)
@@ -407,7 +403,7 @@
     then show "(s ?j, s ?i) \<in> T k" by (simp add: k transition_idx_in ij)
   qed
   then have "\<not> wf (T k)"
-    unfolding wf_iff_no_infinite_down_chain by fast
+    by (meson wf_iff_no_infinite_down_chain)
   with wfT \<open>k < n\<close> show False by blast
 qed