From 710d22679f75bd470702f23e2f6875ea0f685140 Mon Sep 17 00:00:00 2001
From: Bhavik Mehta <bhavikmehta8@gmail.com>
Date: Mon, 20 Apr 2026 03:44:38 +0200
Subject: [PATCH 1/2] feat(Data/Set/Function): add prod lemmas for InjOn,
 SurjOn, MapsTo, LeftInvOn

---
 Mathlib/Data/Set/Function.lean | 42 ++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean
index 8dc96468812a72..9bb9c243e76384 100644
--- a/Mathlib/Data/Set/Function.lean
+++ b/Mathlib/Data/Set/Function.lean
@@ -474,6 +474,11 @@ theorem surjOn_image (f : α → β) (s : Set α) : SurjOn f s (f '' s) :=
 theorem SurjOn.comap_nonempty (h : SurjOn f s t) (ht : t.Nonempty) : s.Nonempty :=
   (ht.mono h).of_image
 
+lemma SurjOn.nonempty_or_eq_empty (h : SurjOn f s t) :
+    s.Nonempty ∨ t = ∅ := by
+  by_contra!
+  grind [surjOn_empty_iff, Set.not_nonempty_iff_eq_empty]
+
 theorem SurjOn.congr (h : SurjOn f₁ s t) (H : EqOn f₁ f₂ s) : SurjOn f₂ s t := by
   rwa [SurjOn, ← H.image_eq]
 
@@ -1240,6 +1245,41 @@ protected lemma InvOn.extendDomain (h : InvOn g₁ g₂ s t) :
 end Set
 
 namespace Set
+
+section Prod
+
+variable {α β₁ β₂ : Type*} {s : Set α} {t₁ : Set β₁} {t₂ : Set β₂}
+  {f₁ : α → β₁} {f₂ : α → β₂} {g₁ : β₁ → α} {g₂ : β₂ → α}
+
+lemma InjOn.left_prodMk (h₁ : s.InjOn f₁) : s.InjOn fun x ↦ (f₁ x, f₂ x) :=
+  fun _ hx _ hy h => h₁ hx hy (Prod.ext_iff.1 h).1
+
+lemma InjOn.right_prodMk (h₂ : s.InjOn f₂) : s.InjOn fun x ↦ (f₁ x, f₂ x) :=
+  fun _ hx _ hy h => h₂ hx hy (Prod.ext_iff.1 h).2
+
+lemma surjOn_fst (h : t₂.Nonempty) : (t₁ ×ˢ t₂).SurjOn Prod.fst t₁ := fun _ h => by simpa [h]
+lemma surjOn_snd (h : t₁.Nonempty) : (t₁ ×ˢ t₂).SurjOn Prod.snd t₂ := fun _ h => by simpa [h]
+
+lemma surjOn_fst_iff : (t₁ ×ˢ t₂).SurjOn Prod.fst t₁ ↔ t₁ = ∅ ∨ t₂.Nonempty :=
+  ⟨by by_contra!; aesop, by simp +contextual [or_imp, surjOn_fst]⟩
+
+lemma surjOn_snd_iff : (t₁ ×ˢ t₂).SurjOn Prod.snd t₂ ↔ t₁.Nonempty ∨ t₂ = ∅ :=
+  ⟨by by_contra!; aesop, by simp +contextual [or_imp, surjOn_snd]⟩
+
+lemma MapsTo.prodMk (h₁ : MapsTo f₁ s t₁) (h₂ : MapsTo f₂ s t₂) :
+    MapsTo (fun x => (f₁ x, f₂ x)) s (t₁ ×ˢ t₂) :=
+  fun _ hx => ⟨h₁ hx, h₂ hx⟩
+
+lemma LeftInvOn.left_prodMk (h₁ : LeftInvOn g₁ f₁ s) :
+    LeftInvOn (fun x ↦ g₁ x.1) (fun x ↦ (f₁ x, f₂ x)) s := h₁
+
+lemma LeftInvOn.right_prodMk (h₂ : LeftInvOn g₂ f₂ s) :
+    LeftInvOn (fun x ↦ g₂ x.2) (fun x ↦ (f₁ x, f₂ x)) s := h₂
+
+end Prod
+
+section ProdMap
+
 variable {α₁ α₂ β₁ β₂ : Type*} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂}
   {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂}
 
@@ -1274,6 +1314,8 @@ lemma InvOn.prodMap (h₁ : InvOn g₁ f₁ s₁ t₁) (h₂ : InvOn g₂ f₂ s
     InvOn (fun x ↦ (g₁ x.1, g₂ x.2)) (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) :=
   ⟨h₁.1.prodMap h₂.1, h₁.2.prodMap h₂.2⟩
 
+end ProdMap
+
 end Set
 
 namespace Equiv

From ba9e7e25e0e74fe9708bb99c7ef8b7fb7ab7adb0 Mon Sep 17 00:00:00 2001
From: Bhavik Mehta <bhavikmehta8@gmail.com>
Date: Mon, 20 Apr 2026 09:58:06 +0200
Subject: [PATCH 2/2] refactor: use comap_nonempty in
 SurjOn.nonempty_or_eq_empty

---
 Mathlib/Data/Set/Function.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Data/Set/Function.lean b/Mathlib/Data/Set/Function.lean
index 9bb9c243e76384..6bcf022e6e5096 100644
--- a/Mathlib/Data/Set/Function.lean
+++ b/Mathlib/Data/Set/Function.lean
@@ -477,7 +477,7 @@ theorem SurjOn.comap_nonempty (h : SurjOn f s t) (ht : t.Nonempty) : s.Nonempty
 lemma SurjOn.nonempty_or_eq_empty (h : SurjOn f s t) :
     s.Nonempty ∨ t = ∅ := by
   by_contra!
-  grind [surjOn_empty_iff, Set.not_nonempty_iff_eq_empty]
+  exact (h.comap_nonempty this.2).ne_empty this.1
 
 theorem SurjOn.congr (h : SurjOn f₁ s t) (H : EqOn f₁ f₂ s) : SurjOn f₂ s t := by
   rwa [SurjOn, ← H.image_eq]