[STATEMENT]
theorem (in group) unit_group_unique:
  assumes "card (carrier G) = 1"
  shows "\<exists> h. h \<in> iso G unit_group"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
card (carrier G) = 1
[PROOF STEP]
obtain x where "carrier G = {x}"
[PROOF STATE]
proof (prove)
using this:
card (carrier G) = 1

goal (1 subgoal):
 1. (\<And>x. carrier G = {x} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest: card_eq_SucD)
[PROOF STATE]
proof (state)
this:
carrier G = {x}

goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
hence "(\<lambda> x. ()) \<in> iso G unit_group"
[PROOF STATE]
proof (prove)
using this:
carrier G = {x}

goal (1 subgoal):
 1. (\<lambda>x. ()) \<in> Group.iso G unit_group
[PROOF STEP]
by -(rule group_isoI, auto simp add:unit_group_is_group is_group, simp add:unit_group_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. ()) \<in> Group.iso G unit_group

goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. ()) \<in> Group.iso G unit_group

goal (1 subgoal):
 1. \<exists>h. h \<in> Group.iso G unit_group
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>h. h \<in> Group.iso G unit_group

goal:
No subgoals!
[PROOF STEP]
qed