ULift and PLift

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

@[simp]

theorem ULift.down_inj {α : Type u_1} {a : ULift.{u_2, u_1} α} {b : ULift.{u_2, u_1} α} : 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 : PLift α} {b : PLift α} : a.down = b.down ↔ a = b