From 2561b7596f0a0818cb317a89aa188b216be397b7 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@lean-fro.org>
Date: Tue, 17 Sep 2024 17:13:03 +0200
Subject: [PATCH] feat: add Nonempty instances for products

---
 src/Init/Core.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 2d448344f277..5ceda4412537 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -1191,6 +1191,21 @@ end
 
 /-! # Product -/
 
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨(x, y)⟩
+
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (MProd α β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨⟨x, y⟩⟩
+
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (PProd α β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨⟨x, y⟩⟩
+
 instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
   default := (default, default)