[STATEMENT]
lemma mult_add_mem:
  assumes "a*x + r \<in> elts (a*y)" "r \<sqsubset> a"
  shows "x \<in> elts y" "r \<in> elts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> elts y &&& r \<in> elts a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> elts y
 2. r \<in> elts a
[PROOF STEP]
obtain v s where v: "a * x + r = a * v + s" "v \<in> elts y" "s \<in> elts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v s. \<lbrakk>a * x + r = a * v + s; v \<in> elts y; s \<in> elts a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a * x + r \<in> elts (a * y)
r \<sqsubset> a

goal (1 subgoal):
 1. (\<And>v s. \<lbrakk>a * x + r = a * v + s; v \<in> elts y; s \<in> elts a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding mult [of a y] lift_def
[PROOF STATE]
proof (prove)
using this:
a * x + r \<in> elts (\<Squnion>u\<in>elts y. set ((+) (a * u) ` elts a))
r \<sqsubset> a

goal (1 subgoal):
 1. (\<And>v s. \<lbrakk>a * x + r = a * v + s; v \<in> elts y; s \<in> elts a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a * x + r = a * v + s
v \<in> elts y
s \<in> elts a

goal (2 subgoals):
 1. x \<in> elts y
 2. r \<in> elts a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a * x + r = a * v + s
v \<in> elts y
s \<in> elts a
[PROOF STEP]
show "x \<in> elts y"
[PROOF STATE]
proof (prove)
using this:
a * x + r = a * v + s
v \<in> elts y
s \<in> elts a

goal (1 subgoal):
 1. x \<in> elts y
[PROOF STEP]
by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma vsubsetD)
[PROOF STATE]
proof (state)
this:
x \<in> elts y

goal (1 subgoal):
 1. r \<in> elts a
[PROOF STEP]
show "r \<in> elts a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> elts a
[PROOF STEP]
by (metis arg_subset_TC assms(2) less_TC_def mult_cancellation_lemma v(1) v(3) vsubsetD)
[PROOF STATE]
proof (state)
this:
r \<in> elts a

goal:
No subgoals!
[PROOF STEP]
qed