Transport a `partial_order` instance?

Stream: Is there code for X?

[Michael Stoll]

I have a definition like the following

structure foo {α} := (to_fun : α → ℕ) (bar : (some statement)) ...

instance {α} : has_coe_to_fun (foo α) (λ _, α → ℕ) := {coe := foo.to_fun}

where all the fields except the first capture some properties of the function. Now I would like to put a partial_order instance on foo via the pi.partial_order instance on α → ℕ. How can I do this without repeating all the boilerplate proofs?
(@[derive partial_order] does not work, which is not suprising, since it is not necessarily clear what the instance should be derived from. Basically, I want to pull it back via coe.)

[Reid Barton]

docs#partial_order.lift

[Michael Stoll]

Thanks! (I needed to add a lemma that coe_fn is injective, but it works now.)