Resolve instance from term

Stream: lean4

[Wojciech Nawrocki]

I ran into the following situation. In my goal type, I have a term @foo a [_: Instance b] where Instance a cannot be inferred by typeclass synthesis, but Instance b works because b was rewritten to a earlier and they are defeq in a way that synthesis doesn't see through. Then I want to rewrite by fooThm (x) : @foo x [_: Instance x] = bar. Unfortunately, rw [fooThm] unifies x := aand then tries to synthesize the instance, which fails. Can I make it "pick up" the instance from the term instead, i.e. unify against it?

[Eric Wieser]

I've had this happen when porting