case inl
α : Type ?u.100268
r : α → α → Prop
⊢ ℵ₀ ≤ cof 0 ↔ IsLimit 0

case inr.inl.intro
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
⊢ ℵ₀ ≤ cof (succ o) ↔ IsLimit (succ o)

case inr.inr
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
⊢ ℵ₀ ≤ cof o ↔ IsLimit o
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
⊢ ℵ₀ ≤ cof o ↔ IsLimit o
rcases zero_or_succ_or_limit o with (rfl | ⟨o, rfl⟩ | l)
no goals
case inl
α : Type ?u.100268
r : α → α → Prop
⊢ ℵ₀ ≤ cof 0 ↔ IsLimit 0
simp [not_zero_isLimit, Cardinal.aleph0_ne_zero]
no goals
case inr.inl.intro
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
⊢ ℵ₀ ≤ cof (succ o) ↔ IsLimit (succ o)
simp [not_succ_isLimit, Cardinal.one_lt_aleph0]
case inr.inr
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
⊢ ℵ₀ ≤ cof o
case inr.inr
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
⊢ ℵ₀ ≤ cof o ↔ IsLimit o
simp [l]
case inr.inr
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
⊢ False
case inr.inr
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
⊢ ℵ₀ ≤ cof o
refine' le_of_not_lt fun h => _
case inr.inr.intro
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n : ℕ
e : cof o = ↑n
⊢ False
case inr.inr
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
⊢ False
cases' Cardinal.lt_aleph0.1 h with n e
case inr.inr.intro
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n : ℕ
e : cof o = ↑n
this : cof (ord (cof o)) = cof o
⊢ False
case inr.inr.intro
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n : ℕ
e : cof o = ↑n
⊢ False
have := cof_cof o
case inr.inr.intro
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n : ℕ
e : cof o = ↑n
this : cof ↑n = ↑n
⊢ False
case inr.inr.intro
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n : ℕ
e : cof o = ↑n
this : cof (ord (cof o)) = cof o
⊢ False
rw [e, ord_nat] at this
case inr.inr.intro.zero
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
e : cof o = ↑Nat.zero
this : cof ↑Nat.zero = ↑Nat.zero
⊢ False

case inr.inr.intro.succ
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n✝ : ℕ
e : cof o = ↑(Nat.succ n✝)
this : cof ↑(Nat.succ n✝) = ↑(Nat.succ n✝)
⊢ False
case inr.inr.intro
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n : ℕ
e : cof o = ↑n
this : cof ↑n = ↑n
⊢ False
cases n
case inr.inr.intro.zero
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
this : cof ↑Nat.zero = ↑Nat.zero
e : o = 0
⊢ False
case inr.inr.intro.zero
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
e : cof o = ↑Nat.zero
this : cof ↑Nat.zero = ↑Nat.zero
⊢ False
simp at e
no goals
case inr.inr.intro.zero
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
this : cof ↑Nat.zero = ↑Nat.zero
e : o = 0
⊢ False
simp [e, not_zero_isLimit] at l
case inr.inr.intro.succ
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n✝ : ℕ
e : cof o = ↑(Nat.succ n✝)
this : 1 = ↑(Nat.succ n✝)
⊢ False
case inr.inr.intro.succ
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n✝ : ℕ
e : cof o = ↑(Nat.succ n✝)
this : cof ↑(Nat.succ n✝) = ↑(Nat.succ n✝)
⊢ False
rw [nat_cast_succ, cof_succ] at this
case inr.inr.intro.succ
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n✝ : ℕ
e : ∃ a, o = succ a
this : 1 = ↑(Nat.succ n✝)
⊢ False
case inr.inr.intro.succ
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n✝ : ℕ
e : cof o = ↑(Nat.succ n✝)
this : 1 = ↑(Nat.succ n✝)
⊢ False
rw [← this, cof_eq_one_iff_is_succ] at e
case inr.inr.intro.succ.intro
α : Type ?u.100268
r : α → α → Prop
n✝ : ℕ
this : 1 = ↑(Nat.succ n✝)
a : Ordinal
l : IsLimit (succ a)
h : cof (succ a) < ℵ₀
⊢ False
case inr.inr.intro.succ
α : Type ?u.100268
r : α → α → Prop
o : Ordinal
l : IsLimit o
h : cof o < ℵ₀
n✝ : ℕ
e : ∃ a, o = succ a
this : 1 = ↑(Nat.succ n✝)
⊢ False
rcases e with ⟨a, rfl⟩
no goals
case inr.inr.intro.succ.intro
α : Type ?u.100268
r : α → α → Prop
n✝ : ℕ
this : 1 = ↑(Nat.succ n✝)
a : Ordinal
l : IsLimit (succ a)
h : cof (succ a) < ℵ₀
⊢ False
exact not_succ_isLimit _ l