theorem ZModModule.exists_submodule_subset_card_le {p : ℕ} {G : Type u_1} [AddCommGroup G] (hp : Nat.Prime p) [Module (ZMod p) G] {k : ℕ} (H : Submodule (ZMod p) G) (hk : k ≤ Nat.card ↥H) (h'k : k ≠ 0) : ∃ (H' : Submodule (ZMod p) G), Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H' ∧ H' ≤ H

In an elementary abelian $p$-group, every finite subgroup $H$ contains a further subgroup of cardinality between $k$ and $pk$, if $k \leq |H|$.