case intro
α : Type ?u.113582
r : α → α → Prop
n : ℕ
hx : ↑n < ℵ₀
⊢ 2 ^ ↑n < ℵ₀
α : Type ?u.113582
r : α → α → Prop
x : Cardinal
hx : x < ℵ₀
⊢ 2 ^ x < ℵ₀
rcases lt_aleph0.1 hx with ⟨n, rfl⟩
no goals
case intro
α : Type ?u.113582
r : α → α → Prop
n : ℕ
hx : ↑n < ℵ₀
⊢ 2 ^ ↑n < ℵ₀
exact_mod_cast nat_lt_aleph0 (2 ^ n)