diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index f19aebc8f6968..545bb74dc003f 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -408,6 +408,14 @@ protected def ulift {α : Type v} : ulift.{u} α ≃ α :=
 protected def plift : plift α ≃ α :=
 ⟨plift.down, plift.up, plift.up_down, plift.down_up⟩
 
+/-- `pprod α β` is equivalent to `α × β` -/
+@[simps apply symm_apply]
+def pprod_equiv_prod {α β : Type*} : pprod α β ≃ α × β :=
+{ to_fun := λ x, (x.1, x.2),
+  inv_fun := λ x, ⟨x.1, x.2⟩,
+  left_inv := λ ⟨x, y⟩, rfl,
+  right_inv := λ ⟨x, y⟩, rfl }
+
 /-- equivalence of propositions is the same as iff -/
 def of_iff {P Q : Prop} (h : P ↔ Q) : P ≃ Q :=
 { to_fun := h.mp,
diff --git a/src/data/pprod.lean b/src/data/pprod.lean
index 94ee99b10f2fe..2f91209ec7404 100644
--- a/src/data/pprod.lean
+++ b/src/data/pprod.lean
@@ -3,12 +3,14 @@ Copyright (c) 2020 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
+import logic.basic
 
 /-!
 # Extra facts about `pprod`
 -/
 
-variables {α : Sort*} {β : Sort*}
+open function
+variables {α β γ δ : Sort*}
 
 namespace pprod
 
@@ -28,3 +30,10 @@ theorem exists' {p : α → β → Prop} : (∃ x : pprod α β, p x.1 x.2) ↔
 pprod.exists
 
 end pprod
+
+lemma function.injective.pprod_map {f : α → β} {g : γ → δ} (hf : injective f) (hg : injective g) :
+  injective (λ x, ⟨f x.1, g x.2⟩ : pprod α γ → pprod β δ) :=
+λ ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ h,
+have A : _ := congr_arg pprod.fst h,
+have B : _ := congr_arg pprod.snd h,
+congr_arg2 pprod.mk (hf A) (hg B)
diff --git a/src/logic/embedding.lean b/src/logic/embedding.lean
index f43d3e88b7f57..4758fe7cb0b7b 100644
--- a/src/logic/embedding.lean
+++ b/src/logic/embedding.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import data.equiv.basic
 import data.set.basic
 import data.sigma.basic
+import data.pprod
 
 /-!
 # Injective functions
@@ -199,6 +200,10 @@ def prod_map {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α ×
   ⇑(e₁.prod_map e₂) = prod.map e₁ e₂ :=
 rfl
 
+/-- If `e₁` and `e₂` are embeddings, then so is `λ ⟨a, b⟩, ⟨e₁ a, e₂ b⟩ : pprod α γ → pprod β δ`. -/
+def pprod_map {α β γ δ : Sort*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : pprod α γ ↪ pprod β δ :=
+⟨λ x, ⟨e₁ x.1, e₂ x.2⟩, e₁.injective.pprod_map e₂.injective⟩
+
 section sum
 open sum