# HG changeset patch
# User desharna
# Date 1710925034 -3600
# Node ID b045d20c9c3c2bc2d590ef78c07f4239733e70fa
# Parent  890c250feab79494d2006f78de7f664627b8a14d
tuned proof

diff -r 890c250feab7 -r b045d20c9c3c src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Mar 20 09:26:25 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Mar 20 09:57:14 2024 +0100
@@ -91,26 +91,8 @@
 lemma antisymp_on_reflclp_if_asymp_on:
   assumes "asymp_on A R"
   shows "antisymp_on A R\<^sup>=\<^sup>="
-proof (rule antisymp_onI)
-  fix x y
-  assume "x \<in> A" and "y \<in> A" and "R\<^sup>=\<^sup>= x y" and "R\<^sup>=\<^sup>= y x"
-  show "x = y"
-  proof (cases "x = y")
-    case True
-    thus ?thesis .
-  next
-    case False
-    hence "R x y"
-      using \<open>R\<^sup>=\<^sup>= x y\<close> by simp
-    hence "\<not> R y x"
-      using \<open>asymp_on A R\<close>[THEN asymp_onD, OF \<open>x \<in> A\<close> \<open>y \<in> A\<close>] by iprover
-    moreover have "R y x"
-      using \<open>R\<^sup>=\<^sup>= y x\<close> False by simp
-    ultimately have False
-      by contradiction
-    thus ?thesis ..
-  qed
-qed
+  unfolding antisymp_on_reflcp
+  using antisymp_on_if_asymp_on[OF \<open>asymp_on A R\<close>] .
 
 lemma antisym_on_reflcl_if_asym_on: "asym_on A R \<Longrightarrow> antisym_on A (R\<^sup>=)"
   using antisymp_on_reflclp_if_asymp_on[to_set] .