I'm dubious about this. Overloading have causes some problems for parsing, and so this would be better placed in lean core where it can actually cooperate with the existing tactic. Moreover, we already have have := by ... and have := ?_ for making have subgoals, so it's not obvious that this is actually needed and not just a lean3-ism.

Indeed. I actually wanted to upstream replace, but the Mathlib implementation imported this file so I blindly did that first. 🤦‍♀️

If the diff isn't too bad, would you be happy with deleting these tactics from Mathlib?

Okay, I did some of this at leanprover-community/mathlib4#6964, and I absolutely agree these tactics should be removed rather than upstreamed. :-)