[Merged by Bors] - feat(logic/basic): ulift.down is injective

src/logic/basic.lean

@@ -155,7 +155,10 @@ assume ⟨h⟩, h.elim
 lemma congr_arg_heq {α} {β : α → Sort*} (f : ∀ a, β a) : ∀ {a₁ a₂ : α}, a₁ = a₂ → f a₁ == f a₂
 | a _ rfl := heq.rfl
 
-lemma plift.down_inj {α : Sort*} : ∀ (a b : plift α), a.down = b.down → a = b
+lemma ulift.down_injective {α : Sort*} : function.injective (@ulift.down α)
+| ⟨a⟩ ⟨b⟩ rfl := rfl
+
+lemma plift.down_injective {α : Sort*} : function.injective (@plift.down α)
 | ⟨a⟩ ⟨b⟩ rfl := rfl
 
 -- missing [symm] attribute for ne in core.