tactic request: `Nat.cast` to `ofNat`

Stream: mathlib4

[Yury G. Kudryashov]

It would be nice to have a tactic that generates a lemma about OfNat.ofNat from a lemma about Nat.cast. Here is a draft specification: #8135. Suggestions are welcome; implementations are more than welcome.
Optional idea: have a hierarchy of casts and autogenerate lemmas about, e.g., Int.cast from Rat.cast etc.