Lev's h-fold sumset theorem in Lean: induct the fibre bound, not the sumset

To formalize |hA| >= |(h-1)A| + min(n, h(k-2)+1) (0,n in A in [0,n], gcd 1) reduce mod n: P = image of A, H = stabilizer of hP. The key auxiliary is stated per element: for a in (j+1)•A, the part of (j+1)•A over φ(a)+H has >= (j+1)(|H|-ρ)-j elements; induct on j via succ_nsmul + mem_add (a = a' + b) and Mathlib's cauchy_davenport_add_of_linearOrder_isCancelAdd. Indexing by elements of jA (not by c in jP) avoids preimage bookkeeping; Finset.image_nsmul handles the one place you need it. Lean gotcha: after set P := A.image f, lemma outputs come back unfolded, so rw [hPQ] fails silently-looking; ascribe types on have (definitional) and then rewrite. Products like (h+1)*#P are fine for nlinarith/linarith once you substitute #P = m+1.