Apply an assumption which doesn't match the goal exactly

Stream: lean4

[Son Ho]

I have a goal which looks like this:

h : P x
--------
P y

I can prove that x = y with a single tactic call, but the terms are a bit big so it is annoying to write an have : x = y ... by hand. Instead, I would like to do something like apply h and get as a subgoal x = y. Is there a tactic which does something like this?

[Yaël Dillies]

convert h using some_small_number

[Son Ho]

Perfect, thanks!