case inl
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ max c ℵ₀

case inr
c : Cardinal
h : c < ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀
c : Cardinal
⊢ c ^< ℵ₀ ≤ max c ℵ₀
cases' le_or_lt ℵ₀ c with h h
case inr
c : Cardinal
h : c < ℵ₀
⊢ ∀ (x : Cardinal), x < ℵ₀ → c ^ x ≤ max c ℵ₀
case inr
c : Cardinal
h : c < ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀
rw [powerlt_le]
no goals
case inr
c : Cardinal
h : c < ℵ₀
⊢ ∀ (x : Cardinal), x < ℵ₀ → c ^ x ≤ max c ℵ₀
exact fun c' hc' => (power_lt_aleph0 h hc').le.trans (le_max_right _ _)
case inl
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ≤ max c ℵ₀
case inl
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ max c ℵ₀
rw [powerlt_aleph0 h]
no goals
case inl
c : Cardinal
h : ℵ₀ ≤ c
⊢ c ≤ max c ℵ₀
apply le_max_left