Growth in the quotient and intersection with a subgroup

For a group G and a subgroup H ≤ G, this file gives upper and lower bounds on the growth of a finset by its growth in H and G ⧸ H.

theorem Finset.card_pow_quotient_mul_pow_inter_subgroup_le {G : Type u_1} [Group G] [DecidableEq G] {H : Subgroup G} [DecidablePred fun (x : G) => x ∈ H] [H.Normal] {A : Finset G} {m n : ℕ} : (image (⇑(QuotientGroup.mk' H)) (A ^ m)).card * {x ∈ A ^ n | x ∈ H}.card ≤ (A ^ (m + n)).card

theorem Finset.card_nsmul_quotient_add_nsmul_inter_addSubgroup_le {G : Type u_1} [AddGroup G] [DecidableEq G] {H : AddSubgroup G} [DecidablePred fun (x : G) => x ∈ H] [H.Normal] {A : Finset G} {m n : ℕ} : (image (⇑(QuotientAddGroup.mk' H)) (m • A)).card * {x ∈ n • A | x ∈ H}.card ≤ ((m + n) • A).card

theorem Finset.le_card_quotient_mul_sq_inter_subgroup {G : Type u_1} [Group G] [DecidableEq G] {H : Subgroup G} [DecidablePred fun (x : G) => x ∈ H] [H.Normal] {A : Finset G} (hAsymm : A⁻¹ = A) : A.card ≤ (image (⇑(QuotientGroup.mk' H)) A).card * {x ∈ A ^ 2 | x ∈ H}.card

theorem Finset.le_card_quotient_add_sq_inter_addSubgroup {G : Type u_1} [AddGroup G] [DecidableEq G] {H : AddSubgroup G} [DecidablePred fun (x : G) => x ∈ H] [H.Normal] {A : Finset G} (hAsymm : -A = A) : A.card ≤ (image (⇑(QuotientAddGroup.mk' H)) A).card * {x ∈ 2 • A | x ∈ H}.card