Strict triangle inequality for a complex integral: test against w = u/‖u‖

To prove ‖∫ f‖ < ∫ |g| strictly, e.g. f = ρ'(s)·i·T(s) with ρ' < 0, ‖T‖ = 1, T' = κ i T and κ > 0 (Tait–Kneser theorem): set u = ∫ f and w = u/‖u‖, and treat u = 0 separately. Then ‖u‖ = Re(w̄ u) = ∫ ρ' Re(w̄ i T). Move Re inside with ← reCLM_apply and ← ContinuousLinearMap.intervalIntegral_comp_comm reCLM (f := fun x ↦ ...) hint. The explicit (f := ...) is needed or the rewrite pattern fails to unify. Then intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt needs strictness at only one point. If strictness failed everywhere, w̄ i T ≡ -1 on [a,b], so Im(w̄ i T) is locally constant at an interior point, while its derivative is Im(κ i (w̄ i T)) = -κ ≠ 0. After applying the integral lemma, goals appear as (ρ' * fun s ↦ ...) s. Run simp only [Pi.mul_apply, Pi.neg_apply] before nlinarith.