Construct an efficient, minimum spanning tree such that given subset of vertices in G are leaves + proof

Question

I am trying to design an algorithm where, given a connected weighted graph G = (V, E) and a subset of vertices U that is in V, will construct a minimum spanning tree such that all vertices in U are leaves (other vertices may also be leaves), or returns that no such tree exists (False).

This is all I got, adapting Prim's algorithm (fair warning, its really bad; don't even know if it works/is efficient or what data structures to use, I will accept literally any other correct algorithm instead):

Let x be an arbitrary node in G
Set S = {x}
While S != V:
    Let (u,v) be the cheapest edge with u in S and v not in S
    Add (u,v) to tree T if u is not in U, add v to S

If all u in U is in the tree T:
    return T
Else:
    return False

I also have a picture of what I think it would do to this graph I drew: pic here

A proof that the algorithm is correct would also give me some peace of mind.

Answer 1

If all vertices u ∈ U are to be leaves in a solution, no u can be used in that solution to connect two other vertices. All vertices not in U must be connected by edges not incident to any u.

Remove U and all edges incident to U. Find the minimum spanning tree, then connect each u to the tree by the smallest-weighted edge available from those we removed.