α : Type u_1
β : Type ?u.230049
γ : Type ?u.230052
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : ord (#α) = type r
⊢ typein r x < type r
α : Type u_1
β : Type ?u.230049
γ : Type ?u.230052
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : ord (#α) = type r
⊢ card (typein r x) < (#α)
rw [← lt_ord, h]
no goals
α : Type u_1
β : Type ?u.230049
γ : Type ?u.230052
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : ord (#α) = type r
⊢ typein r x < type r
apply typein_lt_type