Prod embedding from function

Stream: Is there code for X?

[Aaron Liu]

Do we have any of these?

import Mathlib.Logic.Embedding.Basic

example {α β : Type*} (f : α → β) : α ↪ α × β where
  toFun a := ⟨a, f a⟩
  inj' _ _ := congrArg Prod.fst

example {α β : Type*} (f : β → α) : β ↪ α × β where
  toFun b := ⟨f b, b⟩
  inj' _ _ := congrArg Prod.snd

example {α : Type*} {β : α → Type*} (f : (a : α) → β a) : α ↪ (a : α) × β a where
  toFun a := ⟨a, f a⟩
  inj' _ _ := congrArg Sigma.fst

[Bhavik Mehta]

Not as far as I know, there's docs#Function.Embedding.sectL and docs#Function.Embedding.prodMap but neither of these are quite what you're looking for (I note your first is a generalisation of sectL though)