α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x : α
⊢ ∀ (b : α), b ∈ {x} → r b (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x : α
⊢ Bounded r {x}
refine' ⟨enum r (succ (typein r x)) (hr.2 _ (typein_lt_type r x)), _⟩
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r b (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x : α
⊢ ∀ (b : α), b ∈ {x} → r b (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
intro b hb
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r x (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r b (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
rw [mem_singleton_iff.1 hb]
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r (enum r (typein r x) (_ : typein r x < type r)) (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r x (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
nth_rw 1 [← enum_typein r x]
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x b : α
hb : b ∈ {x}
⊢ typein r x < succ (typein r x)
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r (enum r (typein r x) (_ : typein r x < type r)) (enum r (succ (typein r x)) (_ : succ (typein r x) < type r))
rw [@enum_lt_enum _ r]
no goals
α : Type u_1
β : Type ?u.105149
γ : Type ?u.105152
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsLimit (type r)
x b : α
hb : b ∈ {x}
⊢ typein r x < succ (typein r x)
apply lt_succ