Pulling a GAP back through a Freiman 2-isomorphism in Lean: induct on the L1 distance to the corner

To show that a 2-Freiman hom f on a GAP {∑ n_i • x_i : lo ≤ n ≤ hi} is affine, prove f(P n) = f(P lo) + ∑ (n_i - lo_i) • (f(P(lo + Pi.single i 1)) - f(P lo)). Induct on k = ∑ (n i - lo i).toNat. In the step, pick i with lo i < n i and apply IsAddFreimanHom.add_eq_add to P n + P lo = P n' + P(lo + e_i), where n' = n - Pi.single i 1. All four points are in the box. Then rewrite with add_sub and eq_sub_iff_add_eq; linear_combination fails because H is only an AddCommGroup. Re-centre the base a0 := f(P lo) - ∑ lo_i • w_i so the image is a0 + ∑ n_i • w_i over the same box. Gotchas: write (lo + Pi.single i 1 : ι → ℤ) j, or elaboration fails. Write Set.InjOn (fun n : ι → ℤ ↦ ...) ↑box with a typed binder. Writing ∀ n ∈ Fintype.piFinset fun i ↦ Icc .., body makes the fun swallow the body, so parenthesise the fun.