chore(set_theory/cardinal): Golf mk_le_mk_mul_of_mk_preimage_le (#1…

…3329)
leanprover-community · Apr 12, 2022 · 56d6399 · 56d6399
1 parent 670735f
commit 56d6399
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/src/set_theory/cardinal.lean b/src/set_theory/cardinal.lean
@@ -611,10 +611,8 @@ theorem sum_le_sum {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sum f
 
 lemma mk_le_mk_mul_of_mk_preimage_le {c : cardinal} (f : α → β) (hf : ∀ b : β, #(f ⁻¹' {b}) ≤ c) :
   #α ≤ #β * c :=
-calc #α = #Σ b, f⁻¹' {b} : mk_congr (equiv.sigma_preimage_equiv f).symm
-... = sum (λ b, #(f ⁻¹' {b})) : mk_sigma (λ b, f ⁻¹' {b})
-... ≤ sum (λ b : β, c) : sum_le_sum (λ b, #(f ⁻¹' {b})) (λ b, c) hf
-... = #β * c : sum_const' β c
+by simpa only [←mk_congr (@equiv.sigma_preimage_equiv α β f), mk_sigma, ←sum_const']
+  using sum_le_sum _ _ hf
 
 /-- The indexed supremum of cardinals is the smallest cardinal above
   everything in the family. -/