-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem isStrongLimit_beth {o : Ordinal} (H : IsSuccPrelimit o) : IsStrongLimit (ℶ_ o)

Proof state:
case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha : a < ℶ_ o
⊢ o.IsLimit

Tactic:
rw [isLimit_iff]

Result:
case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha : a < ℶ_ o
⊢ o ≠ 0 ∧ IsSuccPrelimit o

Proof state:
case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
⊢ (ℶ_ o).IsStrongLimit

Tactic:
refine ⟨beth_ne_zero o, fun a ha ↦ ?_⟩

Result:
case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha : a < ℶ_ o
⊢ 2 ^ a < ℶ_ o

Proof state:
case inl
H : IsSuccPrelimit 0
⊢ (ℶ_ 0).IsStrongLimit

Tactic:
rw [beth_zero]

Result:
case inl
H : IsSuccPrelimit 0
⊢ ℵ₀.IsStrongLimit

Proof state:
case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha : a < ⨆ a, ℶ_ ↑a
⊢ 2 ^ a < ℶ_ o

Tactic:
rcases exists_lt_of_lt_ciSup' ha with ⟨⟨i, hi⟩, ha⟩

Result:
case inr.intro.mk
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha✝ : a < ⨆ a, ℶ_ ↑a
i : Ordinal.{u_1}
hi : i ∈ Iio o
ha : a < ℶ_ ↑⟨i, hi⟩
⊢ 2 ^ a < ℶ_ o

Proof state:
case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha : a < ℶ_ o
⊢ o ≠ 0 ∧ IsSuccPrelimit o

Tactic:
exact ⟨h, H⟩

Result:
no goals

Proof state:
o : Ordinal.{u_1}
H : IsSuccPrelimit o
⊢ (ℶ_ o).IsStrongLimit

Tactic:
rcases eq_or_ne o 0 with (rfl | h)

Result:
case inl
H : IsSuccPrelimit 0
⊢ (ℶ_ 0).IsStrongLimit

case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
⊢ (ℶ_ o).IsStrongLimit

Proof state:
case inr.intro.mk
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha✝ : a < ⨆ a, ℶ_ ↑a
i : Ordinal.{u_1}
hi : i ∈ Iio o
ha : a < ℶ_ ↑⟨i, hi⟩
this : 2 ^ a ≤ ℶ_ (succ ↑⟨i, hi⟩)
⊢ 2 ^ a < ℶ_ o

Tactic:
exact this.trans_lt (beth_lt.2 (H.succ_lt hi))

Result:
no goals

Proof state:
case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha : a < ℶ_ o
⊢ 2 ^ a < ℶ_ o

Tactic:
rw [beth_limit] at ha

Result:
case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha : a < ⨆ a, ℶ_ ↑a
⊢ 2 ^ a < ℶ_ o

case inr
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha : a < ℶ_ o
⊢ o.IsLimit

Proof state:
case inl
H : IsSuccPrelimit 0
⊢ ℵ₀.IsStrongLimit

Tactic:
exact isStrongLimit_aleph0

Result:
no goals

Proof state:
case inr.intro.mk
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha✝ : a < ⨆ a, ℶ_ ↑a
i : Ordinal.{u_1}
hi : i ∈ Iio o
ha : a < ℶ_ ↑⟨i, hi⟩
this : 2 ^ a ≤ 2 ^ ℶ_ ↑⟨i, hi⟩
⊢ 2 ^ a < ℶ_ o

Tactic:
rw [← beth_succ] at this

Result:
case inr.intro.mk
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha✝ : a < ⨆ a, ℶ_ ↑a
i : Ordinal.{u_1}
hi : i ∈ Iio o
ha : a < ℶ_ ↑⟨i, hi⟩
this : 2 ^ a ≤ ℶ_ (succ ↑⟨i, hi⟩)
⊢ 2 ^ a < ℶ_ o

Proof state:
case inr.intro.mk
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha✝ : a < ⨆ a, ℶ_ ↑a
i : Ordinal.{u_1}
hi : i ∈ Iio o
ha : a < ℶ_ ↑⟨i, hi⟩
⊢ 2 ^ a < ℶ_ o

Tactic:
have := power_le_power_left two_ne_zero ha.le

Result:
case inr.intro.mk
o : Ordinal.{u_1}
H : IsSuccPrelimit o
h : o ≠ 0
a : Cardinal.{u_1}
ha✝ : a < ⨆ a, ℶ_ ↑a
i : Ordinal.{u_1}
hi : i ∈ Iio o
ha : a < ℶ_ ↑⟨i, hi⟩
this : 2 ^ a ≤ 2 ^ ℶ_ ↑⟨i, hi⟩
⊢ 2 ^ a < ℶ_ o