[STATEMENT]
lemma (in Group) Nset_Suc_im:"\<forall>l \<le> (Suc n). G \<guillemotright> (f l) \<Longrightarrow>
                 insert (f (Suc n)) (f ` {i. i \<le> n}) = f ` {i. i \<le> (Suc n)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> insert (f (Suc n)) (f ` {i. i \<le> n}) = f ` {i. i \<le> Suc n}
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> insert (f (Suc n)) (f ` {i. i \<le> n}) \<subseteq> f ` {i. i \<le> Suc n}
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (rule subsetI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; x \<in> insert (f (Suc n)) (f ` {i. i \<le> n})\<rbrakk> \<Longrightarrow> x \<in> f ` {i. i \<le> Suc n}
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (simp add:image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; x = f (Suc n) \<or> (\<exists>xa\<le>n. x = f xa)\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; x = f (Suc n)\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 2. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; \<exists>xa\<le>n. x = f xa\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 3. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; \<exists>xa\<le>n. x = f xa\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (erule exE, erule conjE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>\<forall>l\<le>Suc n. G \<guillemotright> f l ; xa \<le> n; x = f xa\<rbrakk> \<Longrightarrow> \<exists>xa\<le>Suc n. x = f xa
 2. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (frule_tac x = xa and y = n and z = "Suc n" in le_less_trans,
         simp,
         frule_tac x = xa and y = "Suc n" in less_imp_le, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<le>Suc n. G \<guillemotright> f l  \<Longrightarrow> f ` {i. i \<le> Suc n} \<subseteq> insert (f (Suc n)) (f ` {i. i \<le> n})
[PROOF STEP]
apply (cut_tac Nset_Suc [of "n"], simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done