[GOAL]
⊢ #ℂ = 𝔠
[PROOFSTEP]
rw [mk_congr Complex.equivRealProd, mk_prod, lift_id, mk_real, continuum_mul_self]
[GOAL]
⊢ #↑Set.univ = 𝔠
[PROOFSTEP]
rw [mk_univ, mk_complex]
[GOAL]
⊢ ¬Set.Countable Set.univ
[PROOFSTEP]
rw [← le_aleph0_iff_set_countable, not_le, mk_univ_complex]
[GOAL]
⊢ ℵ₀ < 𝔠
[PROOFSTEP]
apply cantor
