Change type of variable in local context with equivalence

Stream: lean4

[Alex Keizer]

Suppose I have two equivalent types Foo and Bar, is there some way to change a goal

foo x y

Where x y : Foo into:

foo (Foo.ofBar x') (Foo.ofBar y')

Where x' y' : Bar?

[Kevin Buzzard]

If they're equivalent then you can set x' = Bar.ofFoo x and then invoke the fact that Foo.ofBar (Bar.ofFoo x) = x.

[Alex Keizer]

That works, thanks!