[STATEMENT]
lemma min_set_min_union[simp]:
  "(min_set A) \<union>\<^sub>m B = A \<union>\<^sub>m B"
  "A \<union>\<^sub>m (min_set B) = A \<union>\<^sub>m B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_set A \<union>\<^sub>m B = A \<union>\<^sub>m B &&& A \<union>\<^sub>m min_set B = A \<union>\<^sub>m B
[PROOF STEP]
proof (unfold min_union_def min_set_def, safe)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 2. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 3. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 4. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 5. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; x \<notin> B; xa \<in> A; xa |\<subseteq>| x; xb |\<in>| x\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 6. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 7. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 8. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 9. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 10. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
A total of 18 subgoals...
[PROOF STEP]
show "\<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
[PROOF STEP]
by (metis (mono_tags) UnCI dual_order.trans fequalityI min_set_def min_set_obtains)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| ?x \<longrightarrow> xa = ?x; ?x \<in> B; ?xa |\<subseteq>| ?x; ?xb |\<in>| ?x; ?xa \<in> A\<rbrakk> \<Longrightarrow> ?xb |\<in>| ?xa

goal (17 subgoals):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 2. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 3. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 4. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; x \<notin> B; xa \<in> A; xa |\<subseteq>| x; xb |\<in>| x\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 5. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 6. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 7. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 8. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 9. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 10. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 2. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 3. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 4. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; x \<notin> B; xa \<in> A; xa |\<subseteq>| x; xb |\<in>| x\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 5. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 6. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 7. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 8. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 9. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 10. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
A total of 17 subgoals...
[PROOF STEP]
show "\<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
[PROOF STEP]
by (metis (mono_tags) UnCI dual_order.trans fequalityI min_set_def min_set_obtains)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| ?x \<longrightarrow> xa = ?x; ?x \<in> A; ?xa |\<subseteq>| ?x; ?xb |\<in>| ?x; ?xa \<in> B\<rbrakk> \<Longrightarrow> ?xb |\<in>| ?xa

goal (16 subgoals):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 2. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 3. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 4. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; x \<notin> B; xa \<in> A; xa |\<subseteq>| x; xb |\<in>| x\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 5. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 6. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 7. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 8. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 9. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 10. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; \<forall>xa\<in>B. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
A total of 16 subgoals...
[PROOF STEP]
qed blast+