-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem aleph0_le_cof {o} : ℵ₀ ≤ cof o ↔ IsLimit o

Proof state:
case inr.inr.intro.zero
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
this : (↑0).cof = ↑0
e : o = 0
⊢ False

Tactic:
simp [e, not_zero_isLimit] at l

Result:
no goals

Proof state:
case inr.inr.intro.succ.intro
n✝ : ℕ
this : 1 = ↑(n✝ + 1)
a : Ordinal.{u_1}
l : (succ a).IsLimit
h : (succ a).cof < ℵ₀
⊢ False

Tactic:
exact not_succ_isLimit _ l

Result:
no goals

Proof state:
case inr.inr.intro
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n : ℕ
e : o.cof = ↑n
this : (↑n).cof = ↑n
⊢ False

Tactic:
cases n

Result:
case inr.inr.intro.zero
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
e : o.cof = ↑0
this : (↑0).cof = ↑0
⊢ False

case inr.inr.intro.succ
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n✝ : ℕ
e : o.cof = ↑(n✝ + 1)
this : (↑(n✝ + 1)).cof = ↑(n✝ + 1)
⊢ False

Proof state:
case inr.inr.intro
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n : ℕ
e : o.cof = ↑n
this : o.cof.ord.cof = o.cof
⊢ False

Tactic:
rw [e, ord_nat] at this

Result:
case inr.inr.intro
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n : ℕ
e : o.cof = ↑n
this : (↑n).cof = ↑n
⊢ False

Proof state:
case inl

⊢ ℵ₀ ≤ cof 0 ↔ IsLimit 0

Tactic:
simp [not_zero_isLimit, Cardinal.aleph0_ne_zero]

Result:
no goals

Proof state:
case inr.inr
o : Ordinal.{u_1}
l : o.IsLimit
⊢ ℵ₀ ≤ o.cof

Tactic:
refine le_of_not_lt fun h => ?_

Result:
case inr.inr
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
⊢ False

Proof state:
case inr.inr.intro
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n : ℕ
e : o.cof = ↑n
⊢ False

Tactic:
have := cof_cof o

Result:
case inr.inr.intro
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n : ℕ
e : o.cof = ↑n
this : o.cof.ord.cof = o.cof
⊢ False

Proof state:
case inr.inr.intro.zero
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
e : o.cof = ↑0
this : (↑0).cof = ↑0
⊢ False

Tactic:
simp at e

Result:
case inr.inr.intro.zero
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
this : (↑0).cof = ↑0
e : o = 0
⊢ False

Proof state:
case inr.inr
o : Ordinal.{u_1}
l : o.IsLimit
⊢ ℵ₀ ≤ o.cof ↔ o.IsLimit

Tactic:
simp only [l, iff_true]

Result:
case inr.inr
o : Ordinal.{u_1}
l : o.IsLimit
⊢ ℵ₀ ≤ o.cof

Proof state:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ o.cof ↔ o.IsLimit

Tactic:
rcases zero_or_succ_or_limit o with (rfl | ⟨o, rfl⟩ | l)

Result:
case inl

⊢ ℵ₀ ≤ cof 0 ↔ IsLimit 0

case inr.inl.intro
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ (succ o).cof ↔ (succ o).IsLimit

case inr.inr
o : Ordinal.{u_1}
l : o.IsLimit
⊢ ℵ₀ ≤ o.cof ↔ o.IsLimit

Proof state:
case inr.inr.intro.succ
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n✝ : ℕ
e : o.cof = ↑(n✝ + 1)
this : (↑(n✝ + 1)).cof = ↑(n✝ + 1)
⊢ False

Tactic:
rw [natCast_succ, cof_succ] at this

Result:
case inr.inr.intro.succ
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n✝ : ℕ
e : o.cof = ↑(n✝ + 1)
this : 1 = ↑(n✝ + 1)
⊢ False

Proof state:
case inr.inl.intro
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ (succ o).cof ↔ (succ o).IsLimit

Tactic:
simp [not_succ_isLimit, Cardinal.one_lt_aleph0]

Result:
no goals

Proof state:
case inr.inr
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
⊢ False

Tactic:
obtain ⟨n, e⟩ := Cardinal.lt_aleph0.1 h

Result:
case inr.inr.intro
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n : ℕ
e : o.cof = ↑n
⊢ False

Proof state:
case inr.inr.intro.succ
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n✝ : ℕ
e : o.cof = ↑(n✝ + 1)
this : 1 = ↑(n✝ + 1)
⊢ False

Tactic:
rw [← this, cof_eq_one_iff_is_succ] at e

Result:
case inr.inr.intro.succ
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n✝ : ℕ
e : ∃ a, o = succ a
this : 1 = ↑(n✝ + 1)
⊢ False

Proof state:
case inr.inr.intro.succ
o : Ordinal.{u_1}
l : o.IsLimit
h : o.cof < ℵ₀
n✝ : ℕ
e : ∃ a, o = succ a
this : 1 = ↑(n✝ + 1)
⊢ False

Tactic:
rcases e with ⟨a, rfl⟩

Result:
case inr.inr.intro.succ.intro
n✝ : ℕ
this : 1 = ↑(n✝ + 1)
a : Ordinal.{u_1}
l : (succ a).IsLimit
h : (succ a).cof < ℵ₀
⊢ False