From de3ca0d8c3c9d43b8c715146f5d7350278bcbccf Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Wed, 30 Oct 2024 23:21:04 -0400
Subject: [PATCH] feat(Order/WellFoundedOn): wfon.mapsTo and sdff_singleton

---
 Mathlib/Order/WellFoundedSet.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/Mathlib/Order/WellFoundedSet.lean b/Mathlib/Order/WellFoundedSet.lean
index e6c840cc1936d..93938b86e100f 100644
--- a/Mathlib/Order/WellFoundedSet.lean
+++ b/Mathlib/Order/WellFoundedSet.lean
@@ -469,10 +469,24 @@ protected theorem Subsingleton.wellFoundedOn (hs : s.Subsingleton) : s.WellFound
 theorem wellFoundedOn_insert : WellFoundedOn (insert a s) r ↔ WellFoundedOn s r := by
   simp only [← singleton_union, wellFoundedOn_union, wellFoundedOn_singleton, true_and]
 
+@[simp]
+theorem wellFoundedOn_sdiff_singleton : WellFoundedOn (s \ {a}) r ↔ WellFoundedOn s r := by
+  simp only [← wellFoundedOn_insert (a := a), insert_diff_singleton, mem_insert_iff, true_or,
+    insert_eq_of_mem]
+
 protected theorem WellFoundedOn.insert (h : WellFoundedOn s r) (a : α) :
     WellFoundedOn (insert a s) r :=
   wellFoundedOn_insert.2 h
 
+protected theorem WellFoundedOn.sdiff_singleton (h : WellFoundedOn s r) (a : α) :
+    WellFoundedOn (s \ {a}) r :=
+  wellFoundedOn_sdiff_singleton.2 h
+
+lemma WellFoundedOn.mapsTo {α β : Type*} {r : α → α → Prop} (f : β → α)
+    {s : Set α} {t : Set β} (h : MapsTo f t s) (hw : s.WellFoundedOn r) :
+    t.WellFoundedOn (r on f) := by
+  exact InvImage.wf (fun x : t ↦ ⟨f x, h x.prop⟩) hw
+
 end WellFoundedOn
 
 section LinearOrder