α : Type ?u.164415
r : α → α → Prop
f : Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hc' : c ≠ ℵ₀
hf : ∀ (i : Ordinal), i < ord c → f i < ord c
a : Ordinal
⊢ ℵ₀ < c
α : Type ?u.164415
r : α → α → Prop
f : Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hc' : c ≠ ℵ₀
hf : ∀ (i : Ordinal), i < ord c → f i < ord c
a : Ordinal
⊢ ℵ₀ < Ordinal.cof (ord c)
rw [hc.cof_eq]
no goals
α : Type ?u.164415
r : α → α → Prop
f : Ordinal → Ordinal
c : Cardinal
hc : IsRegular c
hc' : c ≠ ℵ₀
hf : ∀ (i : Ordinal), i < ord c → f i < ord c
a : Ordinal
⊢ ℵ₀ < c
exact lt_of_le_of_ne hc.1 hc'.symm