Tactic for changing hypothesis

Stream: lean4

[Chris Hughes]

What's the canonical way of changing the type of a hypothesis in the context, given an Expr for the new type, and another Expr for the proof that the types are equal?

[Leonardo de Moura]

Theses functions might be useful
https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Replace.lean