[STATEMENT]
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 STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
have "\<And>x. x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B x) \<and> f ` (B x) \<subseteq> D (h x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B x) \<and> f ` B x \<subseteq> D (h x)
[PROOF STEP]
by (meson assms lepoll_def)
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B ?x) \<and> f ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B ?x) \<and> f ` B ?x \<subseteq> D (h ?x)
[PROOF STEP]
obtain f where  "\<And>x. x \<in> A \<Longrightarrow> inj_on (f x) (B x) \<and> f x ` B x \<subseteq> D (h x)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> \<exists>f. inj_on f (B ?x) \<and> f ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. (\<And>f. (\<And>x. x \<in> A \<Longrightarrow> inj_on (f x) (B x) \<and> f x ` B x \<subseteq> D (h x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> inj_on (f ?x) (B ?x) \<and> f ?x ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
with h
[PROOF STATE]
proof (chain)
picking this:
inj_on h A
h ` A \<subseteq> C
?x \<in> A \<Longrightarrow> inj_on (f ?x) (B ?x) \<and> f ?x ` B ?x \<subseteq> D (h ?x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on h A
h ` A \<subseteq> C
?x \<in> A \<Longrightarrow> inj_on (f ?x) (B ?x) \<and> f ?x ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. Sigma A B \<lesssim> Sigma C D
[PROOF STEP]
unfolding lepoll_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<forall>y\<in>A. h x = h y \<longrightarrow> x = y
h ` A \<subseteq> C
?x \<in> A \<Longrightarrow> (\<forall>x\<in>B ?x. \<forall>y\<in>B ?x. f ?x x = f ?x y \<longrightarrow> x = y) \<and> f ?x ` B ?x \<subseteq> D (h ?x)

goal (1 subgoal):
 1. \<exists>f. (\<forall>x\<in>Sigma A B. \<forall>y\<in>Sigma A B. f x = f y \<longrightarrow> x = y) \<and> f ` Sigma A B \<subseteq> Sigma C D
[PROOF STEP]
by (rule_tac x="\<lambda>(x,y). (h x, f x y)" in exI) force
[PROOF STATE]
proof (state)
this:
Sigma A B \<lesssim> Sigma C D

goal:
No subgoals!
[PROOF STEP]
qed