case a
α : Type ?u.43015
r : α → α → Prop
o : Ordinal
⊢ cof (succ o) ≤ 1

case a
α : Type ?u.43015
r : α → α → Prop
o : Ordinal
⊢ 1 ≤ cof (succ o)
α : Type ?u.43015
r : α → α → Prop
o : Ordinal
⊢ cof (succ o) = 1
apply le_antisymm
case a
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ cof (succ (type r)) ≤ 1
case a
α : Type ?u.43015
r : α → α → Prop
o : Ordinal
⊢ cof (succ o) ≤ 1
refine' inductionOn o fun α r _ => _
case a
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ cof (type (Sum.Lex r EmptyRelation)) ≤ 1
case a
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ cof (succ (type r)) ≤ 1
change cof (type _) ≤ _
case a
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ cof (type (Sum.Lex r EmptyRelation)) ≤ (#?m.43531)

α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Type u_1

α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (#?m.43531) = 1
case a
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ cof (type (Sum.Lex r EmptyRelation)) ≤ 1
rw [← (_ : (#_) = 1)]
case a.h
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Unbounded (Sum.Lex r EmptyRelation) ?a.S✝

case a.S
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Set (α ⊕ PUnit)

α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (#↑?a.S✝) = 1
case a
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ cof (type (Sum.Lex r EmptyRelation)) ≤ (#?m.43531)

α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Type u_1

α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (#?m.43531) = 1
apply cof_type_le
case a.h
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
a : α ⊕ PUnit
⊢ ¬Sum.Lex r EmptyRelation (Sum.inr PUnit.unit) a
case a.h
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ Unbounded (Sum.Lex r EmptyRelation) ?a.S✝
refine' fun a => ⟨Sum.inr PUnit.unit, Set.mem_singleton _, _⟩
no goals
case a.h
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
a : α ⊕ PUnit
⊢ ¬Sum.Lex r EmptyRelation (Sum.inr PUnit.unit) a
rcases a with (a | ⟨⟨⟨⟩⟩⟩) <;> simp [EmptyRelation]
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ ↑1 = 1
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ (#↑{Sum.inr PUnit.unit}) = 1
rw [Cardinal.mk_fintype, Set.card_singleton]
no goals
α✝ : Type ?u.43015
r✝ : α✝ → α✝ → Prop
o : Ordinal
α : Type u_1
r : α → α → Prop
x✝ : IsWellOrder α r
⊢ ↑1 = 1
simp
case a
α : Type ?u.43015
r : α → α → Prop
o : Ordinal
⊢ 0 < cof (succ o)
case a
α : Type ?u.43015
r : α → α → Prop
o : Ordinal
⊢ 1 ≤ cof (succ o)
rw [← Cardinal.succ_zero, succ_le_iff]
no goals
case a
α : Type ?u.43015
r : α → α → Prop
o : Ordinal
⊢ 0 < cof (succ o)
simpa [lt_iff_le_and_ne, Cardinal.zero_le] using fun h =>
  succ_ne_zero o (cof_eq_zero.1 (Eq.symm h))