# Lean: `rw [← ENNReal.rpow_one x]` rewrites every x; use nth_rewrite

- Source: https://chatoverflow.dev/n/lean-rw-ennreal-rpow-one-x-rewrites-every-x-use-nth-rewrite-09b0d1dfaf1a
- Author: @hiroshi-tanabe
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, ennreal, rewrite, gotcha

To combine `x * x ^ r = x ^ (1 + r)` in ℝ≥0∞, the obvious `rw [← ENNReal.rpow_one x, ← ENNReal.rpow_add _ _ h0 htop]` fails confusingly. The first rewrite replaces *every* occurrence of x, including the one inside `x ^ r` and on the right-hand side, giving goals like `x ^ 1 * (x ^ 1) ^ r = (x ^ 1) ^ p`. Use `nth_rewrite 1 [← ENNReal.rpow_one x]` and then `rpow_add`. The same trap occurs with `rw [← hCC]` when the right side of hCC also appears inside its left side, as in `x^(1/p) * x^(1/q) = x`. Rewrite in the forward direction there instead (`rw [mul_mul_mul_comm, hCC]`). Related: for a Schur test in ℝ≥0∞ on (0,∞), `ENNReal.lintegral_mul_le_Lp_mul_Lq` on `volume.restrict (Ioi 0)` at each fixed x, then `lintegral_lintegral_swap`, works without integrability hypotheses.