-- Mathlib/Data/Real/Cardinality.lean
theorem mk_Ioi_real (a : ℝ) : #(Ioi a) = 𝔠

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ #↑Set.univ < 𝔠

Tactic:
have hu : Iio a ∪ {a} ∪ Ioi a = Set.univ := by
  convert @Iic_union_Ioi ℝ _ _
  exact Iio_union_right

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑Set.univ < 𝔠

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠

Tactic:
have h2 : (fun x => a + a - x) '' Ioi a = Iio a := by
  convert @image_const_sub_Ioi ℝ _ _ _
  simp

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠

Proof state:
a : ℝ
⊢ #↑(Ioi a) = 𝔠

Tactic:
refine le_antisymm (mk_real ▸ mk_set_le _) ?_

Result:
a : ℝ
⊢ 𝔠 ≤ #↑(Ioi a)

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠

Tactic:
rw [← h2]

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x => a + a - x) '' Ioi a) + #↑{a} + #↑(Ioi a) < 𝔠

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a} ∪ Ioi a) < 𝔠

Tactic:
refine lt_of_le_of_lt (mk_union_le _ _) ?_

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a}) + #↑(Ioi a) < 𝔠

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ False

Tactic:
refine _root_.ne_of_lt ?_ mk_univ_real

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ #↑Set.univ < 𝔠

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑{a} < 𝔠

Tactic:
rw [mk_singleton]

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x => a + a - x) '' Ioi a) + #↑{a} < 𝔠

Tactic:
refine add_lt_of_lt (cantor _).le (mk_image_le.trans_lt h) ?_

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑{a} < 𝔠

Proof state:
a : ℝ
⊢ 𝔠 ≤ #↑(Ioi a)

Tactic:
rw [← not_lt]

Result:
a : ℝ
⊢ ¬#↑(Ioi a) < 𝔠

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ (fun x => a + a - x) '' Ioi a = Iio a

Tactic:
convert @image_const_sub_Ioi ℝ _ _ _

Result:
case h.e'_3.h.e'_3
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ a = a + a - a

Proof state:
case h.e'_3.h.e'_3
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ a = a + a - a

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a}) + #↑(Ioi a) < 𝔠

Tactic:
refine lt_of_le_of_lt (add_le_add_right (mk_union_le _ _) _) ?_

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a) + #↑{a} + #↑(Ioi a) < 𝔠

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑Set.univ < 𝔠

Tactic:
rw [← hu]

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
⊢ #↑(Iio a ∪ {a} ∪ Ioi a) < 𝔠

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ 1 < 𝔠

Tactic:
exact one_lt_aleph0.trans (cantor _)

Result:
no goals

Proof state:
case h.e'_2.h.e'_3
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ Iio a ∪ {a} = Iic a

Tactic:
exact Iio_union_right

Result:
no goals

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x => a + a - x) '' Ioi a) + #↑{a} + #↑(Ioi a) < 𝔠

Tactic:
refine add_lt_of_lt (cantor _).le ?_ h

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
hu : Iio a ∪ {a} ∪ Ioi a = Set.univ
h2 : (fun x => a + a - x) '' Ioi a = Iio a
⊢ #↑((fun x => a + a - x) '' Ioi a) + #↑{a} < 𝔠

Proof state:
a : ℝ
⊢ ¬#↑(Ioi a) < 𝔠

Tactic:
intro h

Result:
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ False

Proof state:
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ Iio a ∪ {a} ∪ Ioi a = Set.univ

Tactic:
convert @Iic_union_Ioi ℝ _ _

Result:
case h.e'_2.h.e'_3
a : ℝ
h : #↑(Ioi a) < 𝔠
⊢ Iio a ∪ {a} = Iic a