α : 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, ← card_inv B, ← card_inv (B / C), inv_div', div_inv_eq_mul]
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 _ _ _