α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
h✝ : IsLimit (type r)
S : Set α
H : Unbounded r S
e : (#↑S) = cof (type r)
a : α
a' : α := enum r (succ (typein r a)) (_ : succ (typein r a) < type r)
b : α
h : b ∈ S
ab : ¬r b a'
⊢ typein r a < succ (typein r a)
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
h✝ : IsLimit (type r)
S : Set α
H : Unbounded r S
e : (#↑S) = cof (type r)
a : α
a' : α := enum r (succ (typein r a)) (_ : succ (typein r a) < type r)
b : α
h : b ∈ S
ab : ¬r b a'
⊢ typein r a < typein r a'
rw [typein_enum]
no goals
α : Type u_1
r✝ r : α → α → Prop
inst✝ : IsWellOrder α r
h✝ : IsLimit (type r)
S : Set α
H : Unbounded r S
e : (#↑S) = cof (type r)
a : α
a' : α := enum r (succ (typein r a)) (_ : succ (typein r a) < type r)
b : α
h : b ∈ S
ab : ¬r b a'
⊢ typein r a < succ (typein r a)
exact lt_succ (typein _ _)