diff --git a/Mathlib/Order/Filter/Extr.lean b/Mathlib/Order/Filter/Extr.lean
index 87cbb07b6a9feb..87e7322037f471 100644
--- a/Mathlib/Order/Filter/Extr.lean
+++ b/Mathlib/Order/Filter/Extr.lean
@@ -195,6 +195,12 @@ theorem isMaxOn_const {b : β} : IsMaxOn (fun _ => b) s a :=
 theorem isExtrOn_const {b : β} : IsExtrOn (fun _ => b) s a :=
   isExtrFilter_const
 
+/-- If `f` has a minimum and a maximum both given by `f a` along the filter `l`, then it is
+eventually equal to `f a` along the filter. -/
+lemma eventuallyEq_of_isMinFilter_of_isMaxFilter {β : Type*} [PartialOrder β] {f : α → β}
+    (h₁ : IsMinFilter f l a) (h₂ : IsMaxFilter f l a) : f =ᶠ[l] (fun _ ↦ f a) := by
+  filter_upwards [h₁, h₂] using by grind
+
 /-! ### Order dual -/