From d62e5c080fef8f563a34c3cc10afdcfaac9cefbe Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Wed, 6 May 2026 12:33:08 +0300
Subject: [PATCH 1/2] feat(Order/WellFounded): the minimum of `f '' s` is `f`
 applied to the minimum of `s`

---
 Mathlib/Order/WellFounded.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Mathlib/Order/WellFounded.lean b/Mathlib/Order/WellFounded.lean
index b5a3e9ade3bea9..41d6b001fc3422 100644
--- a/Mathlib/Order/WellFounded.lean
+++ b/Mathlib/Order/WellFounded.lean
@@ -154,6 +154,14 @@ theorem isWellOrder_iff_exists_not_lt_and_eq_or_gt :
   · grind [wellFounded_iff_has_min]
   · grind [h {a, b} <| by simp]
 
+/-- The minimum of `f '' s` is `f` applied to the minimum of `s`. -/
+theorem min_image {r : β → β → Prop} [Std.Trichotomous r] (wf : WellFounded r) (f : α → β)
+    {s : Set α} (hne : s.Nonempty) :
+    wf.min (f '' s) (hne.image f) = f (wf.onFun (f := f).min s hne) := by
+  apply min_eq_of_forall_not_lt wf <| Set.mem_image_of_mem f <| min_mem wf.onFun s hne
+  rintro _ ⟨a, has, rfl⟩
+  exact wf.onFun.not_lt_min s has
+
 theorem not_rel_apply_succ [h : IsWellFounded α r] (f : ℕ → α) : ∃ n, ¬ r (f (n + 1)) (f n) := by
   by_contra! hf
   exact (wellFounded_iff_isEmpty_descending_chain.1 h.wf).elim ⟨f, hf⟩

From 528a566d2f70ccc715541115506d93e052d24e68 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 7 May 2026 04:31:23 +0300
Subject: [PATCH 2/2] add `|>`

---
 Mathlib/Order/WellFounded.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Order/WellFounded.lean b/Mathlib/Order/WellFounded.lean
index 41d6b001fc3422..f8d03a2d796658 100644
--- a/Mathlib/Order/WellFounded.lean
+++ b/Mathlib/Order/WellFounded.lean
@@ -157,7 +157,7 @@ theorem isWellOrder_iff_exists_not_lt_and_eq_or_gt :
 /-- The minimum of `f '' s` is `f` applied to the minimum of `s`. -/
 theorem min_image {r : β → β → Prop} [Std.Trichotomous r] (wf : WellFounded r) (f : α → β)
     {s : Set α} (hne : s.Nonempty) :
-    wf.min (f '' s) (hne.image f) = f (wf.onFun (f := f).min s hne) := by
+    wf.min (f '' s) (hne.image f) = f (wf.onFun (f := f) |>.min s hne) := by
   apply min_eq_of_forall_not_lt wf <| Set.mem_image_of_mem f <| min_mem wf.onFun s hne
   rintro _ ⟨a, has, rfl⟩
   exact wf.onFun.not_lt_min s has