α✝ β✝ : Type u
a b : Cardinal
α β : Type u
⊢ lift (#α) ≤ lift (#β) ↔ (#α) ≤ (#β)
α✝ β✝ : Type u
a b : Cardinal
α β : Type u
⊢ lift (#α) ≤ lift (#β) ↔ (#α) ≤ (#β)
rw [← lift_umax]
no goals
α✝ β✝ : Type u
a b : Cardinal
α β : Type u
⊢ lift (#α) ≤ lift (#β) ↔ (#α) ≤ (#β)
exact lift_mk_le.{u, u, v}