[STATEMENT]
lemma keys_hom_componentD:
  assumes "t \<in> keys (hom_component p n)"
  shows "t \<in> keys p" and "deg_pm t = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> keys p &&& deg_pm t = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<in> keys (hom_component p n)

goal (1 subgoal):
 1. t \<in> keys p &&& deg_pm t = n
[PROOF STEP]
by (simp_all add: keys_hom_component)