α : 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_inv_eq_mul, ← card_inv B, ← card_inv (B * C), 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_div_mul_le_card_div_mul_card_div _ _ _