feat(logic/embedding): add function.embedding.coe_injective (#7383)

Prior art for this lemma name: `linear_map.coe_injective`

src/logic/embedding.lean

@@ -48,8 +48,11 @@ set.ext $ λ x, ⟨λ ⟨y, h⟩, h ▸ subtype.coe_prop (e y), λ hs, ⟨e.symm
 namespace function
 namespace embedding
 
+lemma coe_injective {α β} : @function.injective (α ↪ β) (α → β) coe_fn
+| ⟨x, _⟩ ⟨y, _⟩ rfl := rfl
+
 @[ext] lemma ext {α β} {f g : embedding α β} (h : ∀ x, f x = g x) : f = g :=
-by cases f; cases g; simpa using funext h
+coe_injective (funext h)
 
 lemma ext_iff {α β} {f g : embedding α β} : (∀ x, f x = g x) ↔ f = g :=
 ⟨ext, λ h _, by rw h⟩