English
For a finite subset A of a group with certain normal subgroup H, the product of the image size in the quotient and the count of elements of A^n lying in H is bounded above by the size of A^{m+n}.
Русский
Для конечного множества A в группе с нормальной подгруппой H произведение размера образа в факторгруппе и числа элементов A^n, лежащих в H, не превосходит размер A^{m+n}.
LaTeX
$$$#((A^m). ext{image}(\operatorname{QuotientGroup.mk}' H)) \cdot #\{x \in A^n : x \in H\} \le # (A^{m+n})$$$
Lean4
@[to_additive]
theorem card_pow_quotient_mul_pow_inter_subgroup_le :
#((A ^ m).image <| QuotientGroup.mk' H) * #({x ∈ A ^ n | x ∈ H}) ≤ #(A ^ (m + n)) :=
by
set π := QuotientGroup.mk' H
let φ := invFunOn π (A ^ m)
have hφ : Set.InjOn φ (π '' (A ^ m)) := invFunOn_injOn_image ..
have hφA {a} (ha : a ∈ π '' (A ^ m)) : φ a ∈ A ^ m :=
by
have := invFunOn_mem (by simpa using ha)
norm_cast at this
simpa using this
have hπφ {a} (ha : a ∈ π '' (A ^ m)) : π (φ a) = a := invFunOn_eq (by simpa using ha)
calc
#((A ^ m).image π) * #({x ∈ A ^ n | x ∈ H})
_ = #(((A ^ m).image π).image φ) * #({x ∈ A ^ n | x ∈ H}) := by
rw [Finset.card_image_of_injOn (f := φ) (mod_cast hφ)]
_ ≤ #(((A ^ m).image π).image φ * {x ∈ A ^ n | x ∈ H}) :=
by
rw [Finset.card_mul_iff.2]
simp only [Set.InjOn, coe_image, coe_pow, coe_filter, Set.mem_prod, Set.mem_image, exists_exists_and_eq_and,
Set.mem_setOf_eq, and_imp, forall_exists_index, Prod.forall, Prod.mk.injEq]
rintro _ a₁ b₁ hb₁ rfl - ha₁ _ a₂ b₂ hb₂ rfl - ha₂ hab
have hπa₁ : π a₁ = 1 := (QuotientGroup.eq_one_iff _).2 ha₁
have hπa₂ : π a₂ = 1 := (QuotientGroup.eq_one_iff _).2 ha₂
have hπb : π b₁ = π b₂ := by simpa [hπφ, Set.mem_image_of_mem π, hb₁, hb₂, hπa₁, hπa₂] using congr(π $hab)
simp_all
_ ≤ #(A ^ (m + n)) := by
gcongr
simp only [mul_subset_iff, mem_image, exists_exists_and_eq_and, Finset.mem_filter, and_imp, forall_exists_index,
forall_apply_eq_imp_iff₂, pow_add]
rintro a ha b hb -
exact mul_mem_mul (hφA <| Set.mem_image_of_mem _ <| mod_cast ha) hb
