change ... with replacement

Stream: mathlib4

[Arien Malec]

What's the general way (or patterns of replacement) to handle change...with in the port?

[Kevin Buzzard]

one meh way is revert h, change [what you want h to be] -> _, intro h I guess. This sounds like an easy job for a tactic writer just to make change ... with work.