o : Ordinal
ho : Ordinal.IsLimit o
⊢ aleph o ≤ ⨆ (i : ↑(Iio o)), aleph ↑i

o : Ordinal
ho : Ordinal.IsLimit o
⊢ ∀ (i : ↑(Iio o)), aleph ↑i ≤ aleph o
o : Ordinal
ho : Ordinal.IsLimit o
⊢ aleph o = ⨆ (a : ↑(Iio o)), aleph ↑a
apply le_antisymm _ (ciSup_le' _)
o : Ordinal
ho : Ordinal.IsLimit o
⊢ (⨆ (a : ↑(Iio (ω + o))), aleph' ↑a) ≤ ⨆ (i : ↑(Iio o)), aleph ↑i
o : Ordinal
ho : Ordinal.IsLimit o
⊢ aleph o ≤ ⨆ (i : ↑(Iio o)), aleph ↑i
rw [aleph, aleph'_limit (ho.add _)]
o : Ordinal
ho : Ordinal.IsLimit o
⊢ ∀ (i : ↑(Iio (ω + o))), ∃ i', aleph' ↑i ≤ aleph ↑i'
o : Ordinal
ho : Ordinal.IsLimit o
⊢ (⨆ (a : ↑(Iio (ω + o))), aleph' ↑a) ≤ ⨆ (i : ↑(Iio o)), aleph ↑i
refine' ciSup_mono' (bddAbove_of_small _) _
case mk
o : Ordinal
ho : Ordinal.IsLimit o
i : Ordinal
hi : i ∈ Iio (ω + o)
⊢ ∃ i', aleph' ↑{ val := i, property := hi } ≤ aleph ↑i'
o : Ordinal
ho : Ordinal.IsLimit o
⊢ ∀ (i : ↑(Iio (ω + o))), ∃ i', aleph' ↑i ≤ aleph ↑i'
rintro ⟨i, hi⟩
case mk.inl
o : Ordinal
ho : Ordinal.IsLimit o
i : Ordinal
hi : i ∈ Iio (ω + o)
h : i < ω
⊢ ∃ i', aleph' ↑{ val := i, property := hi } ≤ aleph ↑i'

case mk.inr
o : Ordinal
ho : Ordinal.IsLimit o
i : Ordinal
hi : i ∈ Iio (ω + o)
h : ω ≤ i
⊢ ∃ i', aleph' ↑{ val := i, property := hi } ≤ aleph ↑i'
case mk
o : Ordinal
ho : Ordinal.IsLimit o
i : Ordinal
hi : i ∈ Iio (ω + o)
⊢ ∃ i', aleph' ↑{ val := i, property := hi } ≤ aleph ↑i'
cases' lt_or_le i ω with h h
case mk.inl.intro
o : Ordinal
ho : Ordinal.IsLimit o
n : ℕ
hi : ↑n ∈ Iio (ω + o)
h : ↑n < ω
⊢ ∃ i', aleph' ↑{ val := ↑n, property := hi } ≤ aleph ↑i'
case mk.inl
o : Ordinal
ho : Ordinal.IsLimit o
i : Ordinal
hi : i ∈ Iio (ω + o)
h : i < ω
⊢ ∃ i', aleph' ↑{ val := i, property := hi } ≤ aleph ↑i'
rcases lt_omega.1 h with ⟨n, rfl⟩
case mk.inl.intro
o : Ordinal
ho : Ordinal.IsLimit o
n : ℕ
hi : ↑n ∈ Iio (ω + o)
h : ↑n < ω
⊢ aleph' ↑{ val := ↑n, property := hi } ≤ aleph ↑{ val := 0, property := (_ : 0 < o) }
case mk.inl.intro
o : Ordinal
ho : Ordinal.IsLimit o
n : ℕ
hi : ↑n ∈ Iio (ω + o)
h : ↑n < ω
⊢ ∃ i', aleph' ↑{ val := ↑n, property := hi } ≤ aleph ↑i'
use ⟨0, ho.pos⟩
no goals
case mk.inl.intro
o : Ordinal
ho : Ordinal.IsLimit o
n : ℕ
hi : ↑n ∈ Iio (ω + o)
h : ↑n < ω
⊢ aleph' ↑{ val := ↑n, property := hi } ≤ aleph ↑{ val := 0, property := (_ : 0 < o) }
simpa using (nat_lt_aleph0 n).le
no goals
case mk.inr
o : Ordinal
ho : Ordinal.IsLimit o
i : Ordinal
hi : i ∈ Iio (ω + o)
h : ω ≤ i
⊢ ∃ i', aleph' ↑{ val := i, property := hi } ≤ aleph ↑i'
exact ⟨⟨_, (sub_lt_of_le h).2 hi⟩, aleph'_le.2 (le_add_sub _ _)⟩
no goals
o : Ordinal
ho : Ordinal.IsLimit o
⊢ ∀ (i : ↑(Iio o)), aleph ↑i ≤ aleph o
exact fun i => aleph_le.2 (le_of_lt i.2)