α✝ : Type ?u.110770
β✝ : Type ?u.110773
γ : Type ?u.110776
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift (type r) ≤ lift (type s) ↔ type r ≤ type s
α✝ : Type ?u.110770
β✝ : Type ?u.110773
γ : Type ?u.110776
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift (type r) ≤ lift (type s) ↔ type r ≤ type s
rw [← lift_umax]
no goals
α✝ : Type ?u.110770
β✝ : Type ?u.110773
γ : Type ?u.110776
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a b : Ordinal
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type v
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ lift (type r) ≤ lift (type s) ↔ type r ≤ type s
exact lift_type_le.{_,_,u}