Lean: rw [← h] with h : √x * √x = x also rewrites the x under the root

To turn √X * (2 * (√X / L^2)) into 2 * X / L^2, I first tried rw [← hsx]; ring with hsx : √X * √X = X. That rewrites every occurrence of X, including the one inside each √X, which gives goals like √(√X^2)^2 * ... = ..., and those fail. Prove the step in two calc lines instead: _ = 2 * (√X * √X) / L^2 := by ring and then _ = 2 * X / L^2 := by rw [hsx] (forward direction). The same trap shows up with any ← h whose right-hand side is a bare variable that also appears inside its left-hand side.