case H₁
o : Ordinal
⊢ aleph 0 ≤ beth 0

case H₂
o : Ordinal
⊢ ∀ (o : Ordinal), aleph o ≤ beth o → aleph (succ o) ≤ beth (succ o)

case H₃
o : Ordinal
⊢ ∀ (o : Ordinal), Ordinal.IsLimit o → (∀ (o' : Ordinal), o' < o → aleph o' ≤ beth o') → aleph o ≤ beth o
o : Ordinal
⊢ aleph o ≤ beth o
apply limitRecOn o
no goals
case H₁
o : Ordinal
⊢ aleph 0 ≤ beth 0
simp
case H₂
o✝ o : Ordinal
h : aleph o ≤ beth o
⊢ aleph (succ o) ≤ beth (succ o)
case H₂
o : Ordinal
⊢ ∀ (o : Ordinal), aleph o ≤ beth o → aleph (succ o) ≤ beth (succ o)
intro o h
case H₂
o✝ o : Ordinal
h : aleph o ≤ beth o
⊢ aleph o < 2 ^ beth o
case H₂
o✝ o : Ordinal
h : aleph o ≤ beth o
⊢ aleph (succ o) ≤ beth (succ o)
rw [aleph_succ, beth_succ, succ_le_iff]
no goals
case H₂
o✝ o : Ordinal
h : aleph o ≤ beth o
⊢ aleph o < 2 ^ beth o
exact (cantor _).trans_le (power_le_power_left two_ne_zero h)
case H₃
o✝ o : Ordinal
ho : Ordinal.IsLimit o
IH : ∀ (o' : Ordinal), o' < o → aleph o' ≤ beth o'
⊢ aleph o ≤ beth o
case H₃
o : Ordinal
⊢ ∀ (o : Ordinal), Ordinal.IsLimit o → (∀ (o' : Ordinal), o' < o → aleph o' ≤ beth o') → aleph o ≤ beth o
intro o ho IH
case H₃
o✝ o : Ordinal
ho : Ordinal.IsLimit o
IH : ∀ (o' : Ordinal), o' < o → aleph o' ≤ beth o'
⊢ (⨆ (a : ↑(Iio o)), aleph ↑a) ≤ ⨆ (a : ↑(Iio o)), beth ↑a
case H₃
o✝ o : Ordinal
ho : Ordinal.IsLimit o
IH : ∀ (o' : Ordinal), o' < o → aleph o' ≤ beth o'
⊢ aleph o ≤ beth o
rw [aleph_limit ho, beth_limit ho]
no goals
case H₃
o✝ o : Ordinal
ho : Ordinal.IsLimit o
IH : ∀ (o' : Ordinal), o' < o → aleph o' ≤ beth o'
⊢ (⨆ (a : ↑(Iio o)), aleph ↑a) ≤ ⨆ (a : ↑(Iio o)), beth ↑a
exact ciSup_mono (bddAbove_of_small _) fun x => IH x.1 x.2