α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A * C⁻¹) * card B ≤ card (A * B) * card (B * C⁻¹)
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A / C) * card B ≤ card (A * B) * card (B / C)
rw [div_eq_mul_inv, div_eq_mul_inv]
no goals
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
A✝ B✝ C✝ A B C : Finset α
⊢ card (A * C⁻¹) * card B ≤ card (A * B) * card (B * C⁻¹)
exact card_mul_mul_card_le_card_mul_mul_card_mul _ _ _