# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1648161821 0
# Node ID c3f1bf2824bcd4cf494b795ed52fc09cae6d09d1
# Parent  bcb7d5f1f535975fae115c77c23dad6e4293f295
Some new library lemmas

diff -r bcb7d5f1f535 -r c3f1bf2824bc src/HOL/Library/Equipollence.thy
--- a/src/HOL/Library/Equipollence.thy	Thu Mar 24 22:21:24 2022 +0000
+++ b/src/HOL/Library/Equipollence.thy	Thu Mar 24 22:43:41 2022 +0000
@@ -378,17 +378,22 @@
 lemma times_0_eqpoll: "{} \<times> A \<approx> {}"
   by (simp add: eqpoll_iff_bijections)
 
+lemma Sigma_inj_lepoll_mono:
+  assumes h: "inj_on h A" "h ` A \<subseteq> C" and "\<And>x. x \<in> A \<Longrightarrow> B x \<lesssim> D (h x)" 
+  shows "Sigma A B \<lesssim> Sigma C D"
+proof -
+  have "\<And>x. x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B x) \<and> f ` (B x) \<subseteq> D (h x)"
+    by (meson assms lepoll_def)
+  then obtain f where  "\<And>x. x \<in> A \<Longrightarrow> inj_on (f x) (B x) \<and> f x ` B x \<subseteq> D (h x)"
+    by metis
+  with h show ?thesis
+    unfolding lepoll_def inj_on_def
+    by (rule_tac x="\<lambda>(x,y). (h x, f x y)" in exI) force
+qed
+
 lemma Sigma_lepoll_mono:
   assumes "A \<subseteq> C" "\<And>x. x \<in> A \<Longrightarrow> B x \<lesssim> D x" shows "Sigma A B \<lesssim> Sigma C D"
-proof -
-  have "\<And>x. x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B x) \<and> f ` (B x) \<subseteq> D x"
-    by (meson assms lepoll_def)
-  then obtain f where  "\<And>x. x \<in> A \<Longrightarrow> inj_on (f x) (B x) \<and> f x ` B x \<subseteq> D x"
-    by metis
-  with \<open>A \<subseteq> C\<close> show ?thesis
-    unfolding lepoll_def inj_on_def
-    by (rule_tac x="\<lambda>(x,y). (x, f x y)" in exI) force
-qed
+  using Sigma_inj_lepoll_mono [of id] assms by auto
 
 lemma sum_times_distrib_eqpoll: "(A <+> B) \<times> C \<approx> (A \<times> C) <+> (B \<times> C)"
   unfolding eqpoll_def
@@ -397,6 +402,18 @@
     by (rule bij_betw_byWitness [where f' = "case_sum (\<lambda>(x,z). (Inl x, z)) (\<lambda>(y,z). (Inr y, z))"]) auto
 qed
 
+lemma Sigma_eqpoll_cong:
+  assumes h: "bij_betw h A C"  and BD: "\<And>x. x \<in> A \<Longrightarrow> B x \<approx> D (h x)" 
+  shows "Sigma A B \<approx> Sigma C D"
+proof (intro lepoll_antisym)
+  show "Sigma A B \<lesssim> Sigma C D"
+    by (metis Sigma_inj_lepoll_mono bij_betw_def eqpoll_imp_lepoll subset_refl assms)
+  have "inj_on (inv_into A h) C \<and> inv_into A h ` C \<subseteq> A"
+    by (metis bij_betw_def bij_betw_inv_into h set_eq_subset)
+  then show "Sigma C D \<lesssim> Sigma A B"
+    by (smt (verit, best) BD Sigma_inj_lepoll_mono bij_betw_inv_into_right eqpoll_sym h image_subset_iff lepoll_refl lepoll_trans2)
+qed
+
 lemma prod_insert_eqpoll:
   assumes "a \<notin> A" shows "insert a A \<times> B \<approx> B <+> A \<times> B"
   unfolding eqpoll_def