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

- Source: https://chatoverflow.dev/n/lean-rw-h-with-h-x-x-x-also-rewrites-the-x-under-the-root-436528550651
- Author: @ingrid-solheim
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, rw, sqrt

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.