case inl
α : Type ?u.114391
r : α → α → Prop
H : IsSuccLimit 0
⊢ IsStrongLimit (beth 0)

case inr
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
⊢ IsStrongLimit (beth o)
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
⊢ IsStrongLimit (beth o)
rcases eq_or_ne o 0 with (rfl | h)
case inl
α : Type ?u.114391
r : α → α → Prop
H : IsSuccLimit 0
⊢ IsStrongLimit ℵ₀
case inl
α : Type ?u.114391
r : α → α → Prop
H : IsSuccLimit 0
⊢ IsStrongLimit (beth 0)
rw [beth_zero]
no goals
case inl
α : Type ?u.114391
r : α → α → Prop
H : IsSuccLimit 0
⊢ IsStrongLimit ℵ₀
exact isStrongLimit_aleph0
case inr
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha : a < beth o
⊢ 2 ^ a < beth o
case inr
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
⊢ IsStrongLimit (beth o)
refine' ⟨beth_ne_zero o, fun a ha => _⟩
case inr
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha : a < ⨆ (a : ↑(Iio o)), beth ↑a
⊢ 2 ^ a < beth o
case inr
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha : a < beth o
⊢ 2 ^ a < beth o
rw [beth_limit ⟨h, isSuccLimit_iff_succ_lt.1 H⟩] at ha
case inr.intro.mk
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha✝ : a < ⨆ (a : ↑(Iio o)), beth ↑a
i : Ordinal
hi : i ∈ Iio o
ha : a < beth ↑{ val := i, property := hi }
⊢ 2 ^ a < beth o
case inr
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha : a < ⨆ (a : ↑(Iio o)), beth ↑a
⊢ 2 ^ a < beth o
rcases exists_lt_of_lt_ciSup' ha with ⟨⟨i, hi⟩, ha⟩
case inr.intro.mk
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha✝ : a < ⨆ (a : ↑(Iio o)), beth ↑a
i : Ordinal
hi : i ∈ Iio o
ha : a < beth ↑{ val := i, property := hi }
this : 2 ^ a ≤ 2 ^ beth ↑{ val := i, property := hi }
⊢ 2 ^ a < beth o
case inr.intro.mk
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha✝ : a < ⨆ (a : ↑(Iio o)), beth ↑a
i : Ordinal
hi : i ∈ Iio o
ha : a < beth ↑{ val := i, property := hi }
⊢ 2 ^ a < beth o
have := power_le_power_left two_ne_zero ha.le
case inr.intro.mk
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha✝ : a < ⨆ (a : ↑(Iio o)), beth ↑a
i : Ordinal
hi : i ∈ Iio o
ha : a < beth ↑{ val := i, property := hi }
this : 2 ^ a ≤ beth (succ ↑{ val := i, property := hi })
⊢ 2 ^ a < beth o
case inr.intro.mk
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha✝ : a < ⨆ (a : ↑(Iio o)), beth ↑a
i : Ordinal
hi : i ∈ Iio o
ha : a < beth ↑{ val := i, property := hi }
this : 2 ^ a ≤ 2 ^ beth ↑{ val := i, property := hi }
⊢ 2 ^ a < beth o
rw [← beth_succ] at this
no goals
case inr.intro.mk
α : Type ?u.114391
r : α → α → Prop
o : Ordinal
H : IsSuccLimit o
h : o ≠ 0
a : Cardinal
ha✝ : a < ⨆ (a : ↑(Iio o)), beth ↑a
i : Ordinal
hi : i ∈ Iio o
ha : a < beth ↑{ val := i, property := hi }
this : 2 ^ a ≤ beth (succ ↑{ val := i, property := hi })
⊢ 2 ^ a < beth o
exact this.trans_lt (beth_lt.2 (H.succ_lt hi))