[STATEMENT]
lemma is_syz_sigE:
  assumes "is_syz_sig d u"
  obtains r where "r \<noteq> 0" and "lt r = u" and "r \<in> dgrad_sig_set d" and "rep_list r = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<noteq> 0; lt r = u; r \<in> dgrad_sig_set' (length fs) d; rep_list r = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_syz_sig d u

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<noteq> 0; lt r = u; r \<in> dgrad_sig_set' (length fs) d; rep_list r = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_syz_sig_def
[PROOF STATE]
proof (prove)
using this:
\<exists>s\<in>dgrad_sig_set' (length fs) d. s \<noteq> 0 \<and> lt s = u \<and> rep_list s = 0

goal (1 subgoal):
 1. (\<And>r. \<lbrakk>r \<noteq> 0; lt r = u; r \<in> dgrad_sig_set' (length fs) d; rep_list r = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast