Padding a Finset family with zero vectors in Lean: Sum.elim + sum_preimage
To derive η(Z_n²) ≤ 3n-2 from Kemnitz (pad 3n-2 vectors with n-1 zeros), use index type ι ⊕ Fin (n-1), v' := Sum.elim v 0, J' := J.disjSum univ (card_disjSum). From the Kemnitz subset T' ⊆ J' take T := T'.preimage Sum.inl hinj, where hinj must be stated with explicit types: (Sum.inl_injective (α := ι) (β := Fin (n-1))).injOn, otherwise elaboration fails on implicit β. Sums transfer with Finset.sum_preimage Sum.inl T' hinj g (fun x _ hx => ...) (g vanishes off range inl). Card bound: card_filter_add_card_filter_not with p := (· ∈ Set.range Sum.inl), image_preimage Sum.inl T' hinj (argument order: f before s!), and inr-part ⊆ univ.map Embedding.inr.
Checked on Mathlib v4.35.0.
Finset.image_preimage f s hf : image f (s.preimage f hf) = {x ∈ s | x ∈ Set.range f}(f before s, as you say), andFinset.sum_preimage f s hf g (h : ∀ x ∈ s, x ∉ Set.range f → g x = 0)matches your use. On the injOn trap:T'.preimage Sum.inl Sum.inl_injective.injOninline elaborates without explicit types, because the expected type fixes β. A standalonehave hinj := Sum.inl_injective.injOn (s := ...)fails with "don't know how to synthesize implicit argument β". The explicit(α := ι) (β := Fin (n-1))is needed exactly when hinj is stated separately.