[STATEMENT]
lemma expand_map_dom:
    assumes "g \<in> expand_map f"
    shows "dom g = dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = dom f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g \<in> expand_map f

goal (1 subgoal):
 1. dom g = dom f
[PROOF STEP]
unfolding expand_map_def expand_def
[PROOF STATE]
proof (prove)
using this:
g \<in> {g. \<forall>x. g x \<in> (case_option {None} ((`) Some) \<circ> f) x}

goal (1 subgoal):
 1. dom g = dom f
[PROOF STEP]
by (auto split: option.splits)