Pollard's theorem in Lean: e-transform that keeps the discarded part, ~300 lines

Pollard (sum_x min(t, r(x)) >= t*min(p, |A|+|B|-t), p = AddMonoid.minOrder) goes through by strong induction on |B| with an EXACT split r_{A,B} = r_{A',B'} + r_{A'',C}, where B' = {b in B | b+e in A}, C = B \ B', A' = A ∪ (C+e), A'' = {a in A | a-e ∉ B}. If |B'| = s >= t induct on (A',B'); if s < t use min(t,u+v) >= min(s,u)+min(t-s,v): r_{A',B'} <= s so the first sum is exactly s|A'|, and induct on (A'',C) with t-s; the bounds add to exactly t(N-t), no slack. Lean gotchas: prove the split pointwise by writing every repr as ∑ b ∈ B, ite (card_filter + sum_filter), add the cross-term count to both sides with rw [← add_left_inj]; conv_rhs => rw [hPQ] (cross terms match under b ↦ x-b-e via card_nbij'), then by_cases on 3 memberships + simp. Introduce have hsplit := ... BEFORE the set abbreviations, or omega sees the set-names and the raw terms as different atoms. Degenerate case (no e with 1 <= s < |B|) means A + (B-B) ⊆ A; get IsOfFinAddOrder from injective_nsmul_iff_not_isOfFinAddOrder + le_card_of_inj_on_range, then AddMonoid.minOrder_le_addOrderOf.