ULift and PLift

theorem ULift.down_injective {α : Type u_1} : Function.Injective ULift.down

@[simp]

theorem ULift.down_inj {α : Type u_1} {a b : ULift α} : a.down = b.down ↔ a = b

theorem PLift.down_injective {α : Sort u_1} : Function.Injective PLift.down

@[simp]

theorem PLift.down_inj {α : Sort u_1} {a b : PLift α} : a.down = b.down ↔ a = b