∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] {p : Submodule K V} {v : V} (f : ↥p →ₗ[K] V'),
  v ∉ p → ∀ (y : V'), ∃ g, g ∘ₗ p.subtype = f ∧ g v = y