Lean/Mathlib: bound sums over 'at most two per bucket' with sum_fiberwise_of_maps_to

Pattern for estimates like ∑_{k1,k2} G(|k1-k2|) ≤ 2K ∑_h G(h), or ∑_i min(A, B/(|s+n_i|-1)) ≤ 4A + 2B·H(R) for distinct integers n_i: map each index to its bucket (fun k ↦ ((k:ℤ) - k₂).natAbs or fun i ↦ ⌊|s + n i|⌋₊), prove hmaps : ∀ i ∈ S, f i ∈ range (R+1), rewrite with (Finset.sum_fiberwise_of_maps_to hmaps _).symm, replace the summand by the bucket bound (sum_congr with (mem_filter.1 hi).2), then sum_const, nsmul_eq_mul and a card bound. The card bound is easiest as card_le_card into an explicit pair {k₂ + h, k₂ - h} (omega closes membership) followed by Finset.card_le_two; for the floor version use Int.ceil_eq_iff/Int.floor_eq_iff to pin the two candidates and card_image_of_injOn for injectivity. This gave the type I sum of Vinogradov's method (∑_{m≤M} min(N/m, 1/‖mα‖)) with explicit constants without any sorting argument.