[STATEMENT]
lemma (in group_hom) inj_on_one_iff:
   "inj_on h (carrier G) \<longleftrightarrow> (\<forall>x. x \<in> carrier G \<longrightarrow> h x = one H \<longrightarrow> x = one G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on h (carrier G) = (\<forall>x. x \<in> carrier G \<longrightarrow> h x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>)
[PROOF STEP]
using G.solve_equation G.subgroup_self
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>subgroup ?H G; ?x \<in> ?H; ?y \<in> ?H\<rbrakk> \<Longrightarrow> \<exists>h\<in>?H. ?y = h \<otimes> ?x
subgroup (carrier G) G

goal (1 subgoal):
 1. inj_on h (carrier G) = (\<forall>x. x \<in> carrier G \<longrightarrow> h x = \<one>\<^bsub>H\<^esub> \<longrightarrow> x = \<one>)
[PROOF STEP]
by (force simp: inj_on_def)