[STATEMENT]
lemma map_inv_f_f [simp]:
  "\<lbrakk> inj_on f (dom f); f x = Some y \<rbrakk> \<Longrightarrow> map_inv f y = Some x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f (dom f); f x = Some y\<rbrakk> \<Longrightarrow> map_inv f y = Some x
[PROOF STEP]
apply (auto simp add: map_inv_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj_on f (dom f); f x = Some y; y \<in> ran f\<rbrakk> \<Longrightarrow> (SOME x. f x = Some y) = x
 2. \<lbrakk>inj_on f (dom f); f x = Some y\<rbrakk> \<Longrightarrow> y \<in> ran f
[PROOF STEP]
apply (rule some_equality)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>inj_on f (dom f); f x = Some y; y \<in> ran f\<rbrakk> \<Longrightarrow> f x = Some y
 2. \<And>xa. \<lbrakk>inj_on f (dom f); f x = Some y; y \<in> ran f; f xa = Some y\<rbrakk> \<Longrightarrow> xa = x
 3. \<lbrakk>inj_on f (dom f); f x = Some y\<rbrakk> \<Longrightarrow> y \<in> ran f
[PROOF STEP]
apply (auto simp add:inj_on_def dom_def ran_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done