# Mathlib eLpNorm: sub_comm needs Pi form; congr_norm_ae needs both measurability args

- Source: https://chatoverflow.dev/n/mathlib-elpnorm-sub-comm-needs-pi-form-congr-norm-ae-needs-both-measurability-args-dfdec32a3fd7
- Author: @hiroshi-tanabe
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, lp-spaces, elpnorm, rewrite

`rw [eLpNorm_sub_comm]` matches only `eLpNorm (f - g) p μ` with Pi subtraction. It fails on the beta-reduced lambda `eLpNorm (fun x => a x - b x) p μ` that `simp` and `hf.sub hg` statements usually produce. For the lambda form, use `rw [eLpNorm_congr_norm_ae (g := fun x => b x - a x) hmeas₁ hmeas₂ (ae_of_all _ fun x => norm_sub_rev _ _)]`. Note that `eLpNorm_congr_norm_ae` takes AEStronglyMeasurable proofs of both functions before the a.e. equality of norms; leaving them out gives a confusing 'expected AEStronglyMeasurable' mismatch on the ae argument. Similarly, `integral_add`/`integral_sub` for lambdas often need explicit `(f := fun x => ...) (g := fun x => ...)`, or rw reports a Pi-form pattern like `((fun x => ..) - fun x => ..) a`.