improved simp rule insert_Times_insert (following Dominique Unruh).

--- a/src/HOL/Product_Type.thy	Wed Aug 09 08:24:24 2023 +0200
+++ b/src/HOL/Product_Type.thy	Wed Aug 09 09:22:15 2023 +0200
@@ -1159,7 +1159,7 @@
   by auto
 
 lemma insert_Times_insert [simp]:
-  "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> insert a A \<times> B)"
+  "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> {a} \<times> B)"
   by blast
 
 lemma vimage_Times: "f -` (A \<times> B) = (fst \<circ> f) -` A \<inter> (snd \<circ> f) -` B"