missing code action for `try this: ring_nf`

Stream: mathlib4

[Asei Inoue]

Why is there no code action to replace ring with ring_nf? I thought it should be implemented in mathlib.

import Mathlib.Tactic

example {n : Nat} (h : n = 2) : n * (3 + n) ^ 2 = n * (n ^ 2 + 10 * n + 1) := by
  /-
  Try this: ring_nf
  -/
  ring

[Patrick Massot]

Because nobody took time to do it. You could do it if this is important to you.

[Asei Inoue]

I'm relieved to know it's worth doing. Thanks.

[Mario Carneiro]

#12320