case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ (#ℝ) ≤ 𝔠

case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 𝔠 ≤ (#ℝ)
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ (#ℝ) = 𝔠
apply le_antisymm
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ (#CauSeq.Completion.Cauchy abs) ≤ 𝔠
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ (#ℝ) ≤ 𝔠
rw [Real.equivCauchy.cardinal_eq]
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ (#CauSeq ℚ abs) ≤ 𝔠
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ (#CauSeq.Completion.Cauchy abs) ≤ 𝔠
apply mk_quotient_le.trans
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ (#ℕ → ℚ) = 𝔠
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ (#CauSeq ℚ abs) ≤ 𝔠
apply (mk_subtype_le _).trans_eq
no goals
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ (#ℕ → ℚ) = 𝔠
rw [← power_def, mk_nat, mkRat, aleph0_power_aleph0]
case h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 𝔠 = (#ℕ → Bool)

case a.convert_1
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℝ

case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < ?a.convert_1✝

case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ?a.convert_1✝ < 1 / 2
case a
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 𝔠 ≤ (#ℝ)
convert mk_le_of_injective (cantorFunction_injective _ _)
case a.convert_1
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℝ

case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < ?a.convert_1✝

case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ?a.convert_1✝ < 1 / 2
case h.e'_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 𝔠 = (#ℕ → Bool)

case a.convert_1
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℝ

case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < ?a.convert_1✝

case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ?a.convert_1✝ < 1 / 2
rw [← power_def, mk_bool, mk_nat, two_power_aleph0]
case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < 1 / 3

case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 1 / 3 < 1 / 2
case a.convert_1
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ℝ

case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < ?a.convert_1✝

case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ ?a.convert_1✝ < 1 / 2
exact 1 / 3
case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 1 / 3 < 1 / 2
case a.convert_2
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 0 < 1 / 3

case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 1 / 3 < 1 / 2
norm_num
no goals
case a.convert_3
c : ℝ
f g : ℕ → Bool
n : ℕ
⊢ 1 / 3 < 1 / 2
norm_num