case refine'_1
c : Cardinal
co : ℵ₀ ≤ c
h : ord c = 0
⊢ ℵ₀ = 0

case refine'_2
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : ord c ≤ succ a
⊢ ord c ≤ a
c : Cardinal
co : ℵ₀ ≤ c
⊢ Ordinal.IsLimit (ord c)
refine' ⟨fun h => aleph0_ne_zero _, fun a => lt_imp_lt_of_le_imp_le fun h => _⟩
case refine'_1
c : Cardinal
co : ℵ₀ ≤ c
h : c ≤ card 0
⊢ ℵ₀ = 0
case refine'_1
c : Cardinal
co : ℵ₀ ≤ c
h : ord c = 0
⊢ ℵ₀ = 0
rw [← Ordinal.le_zero, ord_le] at h
no goals
case refine'_1
c : Cardinal
co : ℵ₀ ≤ c
h : c ≤ card 0
⊢ ℵ₀ = 0
simpa only [card_zero, nonpos_iff_eq_zero] using co.trans h
case refine'_2
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ c ≤ card a
case refine'_2
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : ord c ≤ succ a
⊢ ord c ≤ a
rw [ord_le] at h⊢
case refine'_2
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ ℵ₀ ≤ card a
case refine'_2
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ c ≤ card a
rwa [← @add_one_of_aleph0_le (card a), ← card_succ]
case refine'_2
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ ℵ₀ ≤ card (succ a)

case refine'_2.h
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ Ordinal.IsLimit (ord ℵ₀)
case refine'_2
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ ℵ₀ ≤ card a
rw [← ord_le, ← le_succ_of_isLimit, ord_le]
no goals
case refine'_2
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ ℵ₀ ≤ card (succ a)
exact co.trans h
case refine'_2.h
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ Ordinal.IsLimit ω
case refine'_2.h
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ Ordinal.IsLimit (ord ℵ₀)
rw [ord_aleph0]
no goals
case refine'_2.h
c : Cardinal
co : ℵ₀ ≤ c
a : Ordinal
h : c ≤ card (succ a)
⊢ Ordinal.IsLimit ω
exact omega_isLimit