no goals
α β : Type u
c : Cardinal
f : α → β
hf : ∀ (b : β), (#↑(f ⁻¹' {b})) ≤ c
⊢ (#α) ≤ (#β) * c
simpa only [← mk_congr (@Equiv.sigmaFiberEquiv α β f), mk_sigma, ← sum_const'] using
  sum_le_sum _ _ hf