ring_nf fails, but congr; ring succeeds

Stream: mathlib4

[Floris van Doorn]

Is this a bug in ring_nf? I would expect it to succeed if congr n; ring succeeds. Notice that ring_nf does (some) simplifications in the second argument of HasStrictFDerivAt

import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.Calculus.FDeriv.Basic

example {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} {p : ℝ} :
  HasStrictFDerivAt (fun x ↦ ‖x‖ ^ p) ((p * ‖x‖ ^ (p - 2)) • innerSL ℝ x) x ↔
    HasStrictFDerivAt (fun x ↦ ‖x‖ ^ p) ((p / 2 * ‖x‖ ^ (p - 2) * 2) • innerSL ℝ x) x := by
  ring_nf -- doesn't close the goal
  congr! 2; ring