Rewriting x^p as x * x^(p-1) without touching other p's in Lean
conv_rhs => rw [show p = 1 + (p - 1) by ring] rewrites every occurrence of p on that side, including p inside apChar p w, and the next rewrite then fails. Instead, state the exact equation you need: have e : a ^ p = a ^ ((1 : ℝ) + (p - 1)) := by congr 1; ring. Then rw [e, ENNReal.rpow_add_of_nonneg (x := a) 1 (p - 1) zero_le_one hp1.le, ENNReal.rpow_one]. The rpow_add_of_nonneg form needs no a ≠ 0, ∞ side conditions, which matters for constants such as A_p characteristics that are only known to be ≥ 1.
Confirmed on Lean/Mathlib v4.35.0 with a stand-in
apChar p w := w ^ p:conv_lhs => rw [show p = 1 + (p - 1) by ring]turnsa ^ p * apChar p wintoa ^ (1 + (p - 1)) * apChar (1 + (p - 1)) w, and thehave e ... ; rw [e, ENNReal.rpow_add_of_nonneg (x := a) 1 (p - 1) zero_le_one _, ENNReal.rpow_one]route closesa ^ p * apChar p w = a * a ^ (p - 1) * apChar p w. The signature isrpow_add_of_nonneg {x} (y z : ℝ) : 0 ≤ y → 0 ≤ z → x ^ (y + z) = x ^ y * x ^ z, with nox ≠ 0/x ≠ ∞hypotheses, as stated.Two shorter ways to rewrite only the one occurrence, both tested on the same goal:
nth_rw 1 [show p = 1 + (p - 1) by ring](the firstpin the goal is the exponent here), orconv_lhs => enter [1, 2]; rw [show p = 1 + (p - 1) by ring]to point at the exponent of the first factor explicitly. Either is followed by the samerw [ENNReal.rpow_add_of_nonneg 1 (p - 1) zero_le_one _, ENNReal.rpow_one]; in that position the(x := a)can be left out. Thehaveversion has the advantage of not depending on occurrence order or term shape.