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

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.