case a
α β : Type u
c : Cardinal
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)
α β : Type u
c : Cardinal
⊢ ↑toNat (lift c) = ↑toNat c
apply natCast_injective
case a.inl
α β : Type u
c : Cardinal
hc : c < ℵ₀
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)

case a.inr
α β : Type u
c : Cardinal
hc : c ≥ ℵ₀
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)
case a
α β : Type u
c : Cardinal
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)
cases' lt_or_ge c ℵ₀ with hc hc
case a.inl
α β : Type u
c : Cardinal
hc : c < ℵ₀
⊢ lift c < ℵ₀
case a.inl
α β : Type u
c : Cardinal
hc : c < ℵ₀
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)
rw [cast_toNat_of_lt_aleph0, ← lift_natCast.{u,v}, cast_toNat_of_lt_aleph0 hc]
no goals
case a.inl
α β : Type u
c : Cardinal
hc : c < ℵ₀
⊢ lift c < ℵ₀
rwa [lift_lt_aleph0]
case a.inr
α β : Type u
c : Cardinal
hc : c ≥ ℵ₀
⊢ ℵ₀ ≤ lift c
case a.inr
α β : Type u
c : Cardinal
hc : c ≥ ℵ₀
⊢ ↑(↑toNat (lift c)) = ↑(↑toNat c)
rw [cast_toNat_of_aleph0_le, ← lift_natCast.{u,v}, cast_toNat_of_aleph0_le hc, lift_zero]
no goals
case a.inr
α β : Type u
c : Cardinal
hc : c ≥ ℵ₀
⊢ ℵ₀ ≤ lift c
rwa [aleph0_le_lift]