case inl
c : Cardinal
n : ℕ
hc : ℵ₀ ≤ c
⊢ c ^ ↑n ≤ max c ℵ₀

case inr
c : Cardinal
n : ℕ
hc : c < ℵ₀
⊢ c ^ ↑n ≤ max c ℵ₀
c : Cardinal
n : ℕ
⊢ c ^ ↑n ≤ max c ℵ₀
cases' le_or_lt ℵ₀ c with hc hc
no goals
case inl
c : Cardinal
n : ℕ
hc : ℵ₀ ≤ c
⊢ c ^ ↑n ≤ max c ℵ₀
exact le_max_of_le_left (power_nat_le hc)
no goals
case inr
c : Cardinal
n : ℕ
hc : c < ℵ₀
⊢ c ^ ↑n ≤ max c ℵ₀
exact le_max_of_le_right (power_lt_aleph0 hc (nat_lt_aleph0 _)).le