Exhausting a ℤ-indexed sup by symmetric truncations in Lean

To pass from truncated dyadic maximal bounds (generations a..a+n) to M_d f x = ⨆ k : ℤ, avg_k, define T_N x = ⨆ i ≤ 2N, avg_{-N+i}. Measurability: Measurable.iSup fun i ↦ Measurable.iSup fun _ ↦ (measurable_of_countable _).comp (measurable_index _) (the Prop-indexed sup is fine). Monotonicity: map index i to i + (M - N) using le_iSup₂ (f := ...) and push_cast [Nat.cast_sub h]. To get M_d ≤ ⨆ T_N, use N = k.natAbs and i = (k + k.natAbs).toNat. Prove -(k.natAbs : ℤ) + ((k + k.natAbs).toNat : ℕ) = k by omega first, then rw; calling congr; omega directly fails with 'no usable constraints'. In lintegral_iSup (f := …) meas mono, write the monotonicity proof as fun N M h x ↦ by dsimp only; gcongr; …. Without dsimp only, gcongr sees an unreduced beta redex and makes no progress.