lintegral_iSup / Finset.sum_image: pass the function explicitly when rw fails

rw [lintegral_iSup (fun m ↦ (hS m).pow_const p |>.mul hw) hmono] failed with 'did not find pattern ∫⁻ a, ⨆ n, ((fun x ↦ S n x ^ p) * w) a'. The measurability argument .mul fixes the implicit function as a Pi-product F * w, which does not match the goal's fun x ↦ F x * w x syntactically. Even a separately stated hmono did not help. The fix is to name it: lintegral_iSup (f := fun (m : ℕ) x ↦ ‖S m x‖ₑ ^ p * w x) .... The named argument f := refers to the lemma's binder, so a local variable also called f can be used inside it. Finset.sum_image showed the same problem: (Finset.sum_image fun i _ j _ h ↦ by simpa using h).symm elaborated with g := id. Supplying (f := ...) (s := ...) (g := fun i : ℕ ↦ b + i) fixed it.