[GOAL]
⊢ lift 𝔠 = 𝔠
[PROOFSTEP]
rw [← two_power_aleph0, lift_two_power, lift_aleph0, two_power_aleph0]
[GOAL]
c : Cardinal.{u}
⊢ 𝔠 ≤ lift c ↔ 𝔠 ≤ c
[PROOFSTEP]
rw [← lift_continuum.{u, v}, lift_le]
[GOAL]
c : Cardinal.{u}
⊢ lift c ≤ 𝔠 ↔ c ≤ 𝔠
[PROOFSTEP]
rw [← lift_continuum.{u, v}, lift_le]
[GOAL]
c : Cardinal.{u}
⊢ 𝔠 < lift c ↔ 𝔠 < c
[PROOFSTEP]
rw [← lift_continuum.{u, v}, lift_lt]
[GOAL]
c : Cardinal.{u}
⊢ lift c < 𝔠 ↔ c < 𝔠
[PROOFSTEP]
rw [← lift_continuum.{u, v}, lift_lt]
[GOAL]
⊢ beth 1 = 𝔠
[PROOFSTEP]
simpa using beth_succ 0
[GOAL]
⊢ #(Set ℕ) = 𝔠
[PROOFSTEP]
simp
[GOAL]
⊢ aleph 1 ≤ 𝔠
[PROOFSTEP]
rw [← succ_aleph0]
[GOAL]
⊢ Order.succ ℵ₀ ≤ 𝔠
[PROOFSTEP]
exact Order.succ_le_of_lt aleph0_lt_continuum
[GOAL]
⊢ 𝔠 ^ ℵ₀ = 𝔠
[PROOFSTEP]
rw [← two_power_aleph0, ← power_mul, mul_eq_left le_rfl le_rfl aleph0_ne_zero]
