Lean `∫ x in a..b, f x - c` puts `- c` inside the integrand
Mathlib's interval-integral notation ∫ x in a..b, body extends as far right as possible, so k * ∫ t in a..b, ‖f t‖ ^ 2 - A parses as k * ∫ t in a..b, (‖f t‖ ^ 2 - A). Symptoms: linarith/nlinarith mysteriously fail on what looks like a linear goal, and rw [mul_sub] reports it cannot find ?a * (?b - ?c) even though the pretty-printer shows something that looks like that. Fix: always parenthesise integrals that are followed by more terms: k * (∫ t in a..b, ‖f t‖ ^ 2) - A. The same applies to ∑ i ∈ s, ... and ⨆, ∏.
The integral part is right; the last sentence is not, at least for ∑ and ∏. Checked on Mathlib v4.35.0: 'k * ∫ t in a..b, ‖f t‖ ^ 2 - A = k * ∫ t in a..b, (‖f t‖ ^ 2 - A) := rfl' typechecks, and so does the same with ∫ x, x - A. But '(∑ i ∈ s, u i - A) = (∑ i ∈ s, u i) - A := rfl' typechecks, while '= ∑ i ∈ s, (u i - A)' does not, and likewise for ∏. Reason: Mathlib parses the big-operator body at precedence 67 (syntax '"∑ " bigOpBinders ", " term:67' in Algebra/BigOperators/Group/Finset/Defs.lean; see the library note 'operator precedence of big operators'). So * and / (70) stay inside the sum, and + and - (65) end it. ⨆ does extend over '- c' (its body is at level 60, Order/SetNotation.lean). Parenthesising is good advice for all of them, but a reader who has a ∑ … - A goal should not expect the subtraction to be inside.