[STATEMENT]
lemma set_take_two:
  assumes "card A \<ge> 2"
  obtains x y where "x \<in> A" "y \<in> A" "x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
2 \<le> card A
[PROOF STEP]
obtain k where "card A = Suc (Suc k)"
[PROOF STATE]
proof (prove)
using this:
2 \<le> card A

goal (1 subgoal):
 1. (\<And>k. card A = Suc (Suc k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: le_iff_add)
[PROOF STATE]
proof (state)
this:
card A = Suc (Suc k)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from card_eq_SucD[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = Suc k \<and> (Suc k = 0 \<longrightarrow> B = {})
[PROOF STEP]
obtain x B where x: "A = insert x B" "x \<notin> B" "card B = Suc k"
[PROOF STATE]
proof (prove)
using this:
\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = Suc k \<and> (Suc k = 0 \<longrightarrow> B = {})

goal (1 subgoal):
 1. (\<And>x B. \<lbrakk>A = insert x B; x \<notin> B; card B = Suc k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = insert x B
x \<notin> B
card B = Suc k

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from card_eq_SucD[OF this(3)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>b Ba. B = insert b Ba \<and> b \<notin> Ba \<and> card Ba = k \<and> (k = 0 \<longrightarrow> Ba = {})
[PROOF STEP]
obtain y where y: "y \<in> B"
[PROOF STATE]
proof (prove)
using this:
\<exists>b Ba. B = insert b Ba \<and> b \<notin> Ba \<and> card Ba = k \<and> (k = 0 \<longrightarrow> Ba = {})

goal (1 subgoal):
 1. (\<And>y. y \<in> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> B

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x y
[PROOF STATE]
proof (chain)
picking this:
A = insert x B
x \<notin> B
card B = Suc k
y \<in> B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A = insert x B
x \<notin> B
card B = Suc k
y \<in> B

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by - (rule that[of x y], auto)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed