o : Ordinal
⊢ alephIdx (aleph' (succ o)) ≤ alephIdx (succ (aleph' o))
o : Ordinal
⊢ aleph' (succ o) = succ (aleph' o)
apply (succ_le_of_lt <| aleph'_lt.2 <| lt_succ o).antisymm' (Cardinal.alephIdx_le.1 <| _)
o : Ordinal
⊢ aleph' o < succ (aleph' o)
o : Ordinal
⊢ alephIdx (aleph' (succ o)) ≤ alephIdx (succ (aleph' o))
rw [alephIdx_aleph', succ_le_iff, ← aleph'_lt, aleph'_alephIdx]
no goals
o : Ordinal
⊢ aleph' o < succ (aleph' o)
apply lt_succ