feat: a ^ b ≤ ℵ₀ if a ≤ ℵ₀ and b < ℵ₀ (leanprover-community#21060)

From PFR

The corresponding `Cardinal.power_lt_aleph0` already exists.

Co-authored-by: Sébastien Gouëzel <sebastien.gouezel@univ-rennes1.fr>

Author: YaelDillies

Mathlib/SetTheory/Cardinal/Arithmetic.lean

@@ -527,6 +527,9 @@ theorem power_nat_le_max {c : Cardinal.{u}} {n : ℕ} : c ^ (n : Cardinal.{u}) 
   · exact le_max_of_le_left (power_nat_le hc)
   · exact le_max_of_le_right (power_lt_aleph0 hc (nat_lt_aleph0 _)).le
 
+lemma power_le_aleph0 {a b : Cardinal.{u}} (ha : a ≤ ℵ₀) (hb : b < ℵ₀) : a ^ b ≤ ℵ₀ := by
+  lift b to ℕ using hb; simpa [ha] using power_nat_le_max (c := a)
+
 theorem powerlt_aleph0 {c : Cardinal} (h : ℵ₀ ≤ c) : c ^< ℵ₀ = c := by
   apply le_antisymm
   · rw [powerlt_le]