From 56f9cb64b0f580483ed006ed0b36da250e7356bd Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Sun, 28 Dec 2025 15:06:01 -0800
Subject: [PATCH] feat: add `empty_eq_image` simp lemmas

---
 Mathlib/Data/Finset/Image.lean | 3 +++
 Mathlib/Data/Set/Image.lean    | 4 ++++
 2 files changed, 7 insertions(+)

diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
index 7e250a14dd0523..1a9c7f34499a66 100644
--- a/Mathlib/Data/Finset/Image.lean
+++ b/Mathlib/Data/Finset/Image.lean
@@ -432,6 +432,9 @@ theorem image_erase [DecidableEq α] {f : α → β} (hf : Injective f) (s : Fin
 @[simp]
 theorem image_eq_empty : s.image f = ∅ ↔ s = ∅ := mod_cast Set.image_eq_empty (f := f) (s := s)
 
+@[simp]
+theorem empty_eq_image : ∅ = s.image f ↔ s = ∅ := by rw [eq_comm, image_eq_empty]
+
 theorem image_sdiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Injective f) :
     (s \ t).image f = s.image f \ t.image f :=
   mod_cast Set.image_diff hf s t
diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean
index f99617a8d231bd..2684eb6551ad52 100644
--- a/Mathlib/Data/Set/Image.lean
+++ b/Mathlib/Data/Set/Image.lean
@@ -276,6 +276,10 @@ theorem image_eq_empty {α β} {f : α → β} {s : Set α} : f '' s = ∅ ↔ s
   simp only [eq_empty_iff_forall_notMem]
   exact ⟨fun H a ha => H _ ⟨_, ha, rfl⟩, fun H b ⟨_, ha, _⟩ => H _ ha⟩
 
+@[simp, mfld_simps]
+theorem empty_eq_image {α β} {f : α → β} {s : Set α} : ∅ = f '' s ↔ s = ∅ := by
+  rw [eq_comm, image_eq_empty]
+
 theorem preimage_compl_eq_image_compl [BooleanAlgebra α] (s : Set α) :
     HasCompl.compl ⁻¹' s = HasCompl.compl '' s :=
   Set.ext fun x =>