α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B✝ C : Finset α
hA : Finset.Nonempty A
B : Finset α
m n : ℕ
⊢ ↑(card (B⁻¹ ^ m / B⁻¹ ^ n)) ≤ (↑(card (A * B⁻¹)) / ↑(card A)) ^ (m + n) * ↑(card A)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B✝ C : Finset α
hA : Finset.Nonempty A
B : Finset α
m n : ℕ
⊢ ↑(card (B ^ m / B ^ n)) ≤ (↑(card (A / B)) / ↑(card A)) ^ (m + n) * ↑(card A)
rw [← card_inv, inv_div', ← inv_pow, ← inv_pow, div_eq_mul_inv A]
no goals
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A B✝ C : Finset α
hA : Finset.Nonempty A
B : Finset α
m n : ℕ
⊢ ↑(card (B⁻¹ ^ m / B⁻¹ ^ n)) ≤ (↑(card (A * B⁻¹)) / ↑(card A)) ^ (m + n) * ↑(card A)
exact card_pow_div_pow_le hA _ _ _