From bf241f9e8649b0cb59b22ca097b3baee67121b70 Mon Sep 17 00:00:00 2001
From: Paul Reichert <datokrat@users.noreply.github.com>
Date: Wed, 19 Mar 2025 08:33:49 +0100
Subject: [PATCH] feat: List.min? lemmas and Option.bind_congr (#7529)

This PR upstreams `bind_congr` from Mathlib and proves that the minimum
of a sorted list is its head and weakens the antisymmetry condition of
`min?_eq_some_iff`. Instead of requiring an `Std.Antisymm` instance,
`min?_eq_some_iff` now only expects a proof that the relation is
antisymmetric *on the elements of the list*. If the new premise is left
out, an autoparam will try to derive it from `Std.Antisymm`, so existing
usages of the theorem will most likely continue to work.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
---
 src/Init/Data/List/MinMax.lean   | 21 ++++++++++++++++++---
 src/Init/Data/Option/Lemmas.lean |  4 ++++
 2 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/List/MinMax.lean b/src/Init/Data/List/MinMax.lean
index 7bc8b09c46..4a883b7c2f 100644
--- a/src/Init/Data/List/MinMax.lean
+++ b/src/Init/Data/List/MinMax.lean
@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Lemmas
+import Init.Data.List.Pairwise
 
 /-!
 # Lemmas about `List.min?` and `List.max?.
@@ -38,6 +39,18 @@ theorem isSome_min?_of_mem {l : List α} [Min α] {a : α} (h : a ∈ l) :
     l.min?.isSome := by
   cases l <;> simp_all [List.min?_cons']
 
+theorem min?_eq_head? {α : Type u} [Min α] {l : List α}
+    (h : l.Pairwise (fun a b => min a b = a)) : l.min? = l.head? := by
+  cases l with
+  | nil => rfl
+  | cons x l =>
+    rw [List.head?_cons, List.min?_cons', Option.some.injEq]
+    induction l generalizing x with
+    | nil => simp
+    | cons y l ih =>
+      have hx : min x y = x := List.rel_of_pairwise_cons h (List.mem_cons_self _ _)
+      rw [List.foldl_cons, ih _ (hx.symm ▸ h.sublist (by simp)), hx]
+
 theorem min?_mem [Min α] (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b) :
     {xs : List α} → xs.min? = some a → a ∈ xs := by
   intro xs
@@ -78,17 +91,19 @@ theorem le_min?_iff [Min α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
 -- and `le_min_iff`.
-theorem min?_eq_some_iff [Min α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
+theorem min?_eq_some_iff [Min α] [LE α]
     (le_refl : ∀ a : α, a ≤ a)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
-    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
+    (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α}
+    (anti : ∀ a b, a ∈ xs → b ∈ xs → a ≤ b → b ≤ a → a = b := by
+      exact fun a b _ _ => Std.Antisymm.antisymm a b) :
     xs.min? = some a ↔ a ∈ xs ∧ ∀ b, b ∈ xs → a ≤ b := by
   refine ⟨fun h => ⟨min?_mem min_eq_or h, (le_min?_iff le_min_iff h).1 (le_refl _)⟩, ?_⟩
   intro ⟨h₁, h₂⟩
   cases xs with
   | nil => simp at h₁
   | cons x xs =>
-    exact congrArg some <| anti.1 _ _
+    exact congrArg some <| anti _ _ (min?_mem min_eq_or rfl) h₁
       ((le_min?_iff le_min_iff (xs := x::xs) rfl).1 (le_refl _) _ h₁)
       (h₂ _ (min?_mem min_eq_or (xs := x::xs) rfl))
 
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index bfcc218aad..983b63e58c 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -138,6 +138,10 @@ theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β)
 theorem bind_assoc (x : Option α) (f : α → Option β) (g : β → Option γ) :
     (x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl
 
+theorem bind_congr {α β} {o : Option α} {f g : α → Option β} :
+    (h : ∀ a, o = some a → f a = g a) → o.bind f = o.bind g := by
+  cases o <;> simp
+
 theorem join_eq_some : x.join = some a ↔ x = some (some a) := by
   simp [bind_eq_some]