# HG changeset patch
# User desharna
# Date 1742821745 -3600
# Node ID 06c1c163b66c3e281e29ec34bff09c1798f680c6
# Parent  df714fc6c6bb2026f50b428aee7c7b95e47fe5e6
tuned proof

diff -r df714fc6c6bb -r 06c1c163b66c src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 24 14:08:20 2025 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 24 14:09:05 2025 +0100
@@ -217,7 +217,7 @@
   by (simp add: reflp_on_mono_strong le_fun_def)
 
 lemma reflp_on_subset: "reflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> reflp_on B R"
-  by (auto intro: reflp_onI dest: reflp_onD)
+  using reflp_on_mono_strong .
 
 lemma reflp_on_image: "reflp_on (f ` A) R \<longleftrightarrow> reflp_on A (\<lambda>a b. R (f a) (f b))"
   by (simp add: reflp_on_def)