Why are two rings needed here?

Stream: mathlib4

[Terence Tao]

To solve this problem

import Mathlib

example (n: ℕ) (X : ℝ) : n * X * n = X * (n^2) := by
  ring
  norm_cast
  ring

it appears necessary to apply two ring and one norm_cast tactic in precisely the order indicated here; any shorter combination does not seem to work. I am aware of the real powers bug but I don't think it is to blame for this issue. Is this expected behavior?

[Ruben Van de Velde]

Interesting. The issue is that ring needs to collect the ns on both sides into a power to allow norm_cast to move the cast out of the power. Incidentally, this also works:

import Mathlib

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220

example (n: ℕ) (X : ℝ) : n * X * n = X * (n^2) := by
  push_cast
  ring

[Alex J. Best]

There is an open PR to support automatically pushing ring homs inwards when using ring, #7601, but even that wouldn't quite do this in one fell swoop yet, its a step in the right direction though I think