[STATEMENT]
lemma (in finite_group) finite_generate:
  assumes "A \<subseteq> carrier G"
  shows "finite (generate G A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (generate G A)
[PROOF STEP]
using generate_incl[of A] rev_finite_subset[of "carrier G" "generate G A"] assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> carrier G \<Longrightarrow> generate G A \<subseteq> carrier G
\<lbrakk>finite (carrier G); generate G A \<subseteq> carrier G\<rbrakk> \<Longrightarrow> finite (generate G A)
A \<subseteq> carrier G

goal (1 subgoal):
 1. finite (generate G A)
[PROOF STEP]
by simp