feat: add a lemma relating minKey? and min? for DTreeMap

src/Init/Data/Order/ClassesExtra.lean

@@ -36,4 +36,6 @@ public theorem LawfulOrderOrd.isGE_compare_eq_false {α : Type u} [Ord α] [LE 
     (compare a b).isGE = false ↔ ¬ b ≤ a := by
   simp [← isGE_compare]
 
+public abbrev LawfulOrderCmp (cmp : α → α → Ordering) [LE α] := @Std.LawfulOrderOrd α ⟨cmp⟩ _
+
 end Std

src/Init/Data/Order/LemmasExtra.lean

@@ -147,6 +147,18 @@ public theorem max_eq_if_isGE_compare {α : Type u} [Ord α] [LE α] {_ : Max α
     {a b : α} : max a b = if (compare a b).isGE then a else b := by
   open Classical in simp [max_eq_if, isGE_compare]
 
+private theorem min_le_min [LE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [IsLinearOrder α] (a b : α) : min a b ≤ min b a := by
+  apply (LawfulOrderInf.le_min_iff (min a b) b a).2
+  rw [And.comm]
+  by_cases h : a ≤ b
+  case pos =>
+    simp [LawfulOrderLeftLeaningMin.min_eq_left, h, le_refl]
+  case neg =>
+    simp [LawfulOrderLeftLeaningMin.min_eq_right _ _ h, le_of_not_ge h, le_refl]
+
+public instance [LE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [IsLinearOrder α] : Commutative (min : α → α → α) where
+  comm a b := by apply le_antisymm <;> simp [min_le_min]
+
 end Std
 
 namespace Classical.Order

src/Std/Data/DTreeMap/Internal/Lemmas.lean

@@ -9,6 +9,7 @@ prelude
 public import Std.Data.HashMap.Basic
 meta import Std.Data.HashMap.Basic
 public import Std.Data.DTreeMap.Internal.WF.Lemmas
+public import Init.Data.Order.ClassesExtra
 
 @[expose] public section
 
@@ -6135,6 +6136,13 @@ theorem minKey?_mem [TransOrd α] (h : t.WF) {km} :
     km ∈ t := by
   simp_to_model [minKey?, contains] using List.containsKey_minKey?
 
+theorem minKey?_eq_min?_keys [TransOrd α] [Min α]
+    [LE α] [LawfulOrderOrd α] [LawfulOrderMin α]
+    [LawfulOrderLeftLeaningMin α] [LawfulEqOrd α]
+    (h : t.WF) :
+    t.minKey? = t.keys.min? := by
+  simp_to_model using List.minKey?_eq_min?_keys
+
 theorem isSome_minKey?_of_contains [TransOrd α] (h : t.WF) {k} :
     (hc : t.contains k) → t.minKey?.isSome := by
   simp_to_model [minKey?, contains] using List.isSome_minKey?_of_containsKey

src/Std/Data/DTreeMap/Lemmas.lean

@@ -3690,6 +3690,11 @@ theorem contains_minKey? [TransCmp cmp] {km} :
     t.contains km :=
   Impl.contains_minKey? t.wf
 
+theorem minKey?_eq_min?_keys [TransCmp cmp] [Min α]
+    [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α] [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] :
+    t.minKey? = t.keys.min? :=
+  Impl.minKey?_eq_min?_keys t.wf
+
 theorem minKey?_mem [TransCmp cmp] {km} :
     (hkm : t.minKey? = some km) →
     km ∈ t:=

src/Std/Data/DTreeMap/Raw/Lemmas.lean

@@ -3847,6 +3847,13 @@ theorem contains_minKey? [TransCmp cmp] (h : t.WF) {km} :
     t.contains km :=
   Impl.contains_minKey? h
 
+theorem minKey?_eq_min?_keys [TransCmp cmp] [Min α]
+    [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α]
+    [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp]
+    (h : t.WF) :
+    t.minKey? = t.keys.min? :=
+  Impl.minKey?_eq_min?_keys h.out
+
 theorem minKey?_mem [TransCmp cmp] (h : t.WF) {km} :
     (hkm : t.minKey? = some km) →
     km ∈ t:=

src/Std/Data/ExtDTreeMap/Lemmas.lean

@@ -3799,6 +3799,12 @@ theorem minKey?_mem [TransCmp cmp] {km} :
     km ∈ t :=
   t.inductionOn fun _ => DTreeMap.minKey?_mem
 
+theorem minKey?_eq_min?_keys [TransCmp cmp] [Min α]
+    [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α]
+    [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] :
+    t.minKey? = t.keys.min? :=
+  t.inductionOn fun _ => DTreeMap.minKey?_eq_min?_keys
+
 theorem isSome_minKey?_of_contains [TransCmp cmp] {k} :
     (hc : t.contains k) → t.minKey?.isSome :=
   t.inductionOn fun _ => DTreeMap.isSome_minKey?_of_contains

src/Std/Data/ExtTreeMap/Lemmas.lean

@@ -2344,6 +2344,12 @@ theorem minKey?_mem [TransCmp cmp] {km} :
     (hkm : t.minKey? = some km) → km ∈ t :=
   ExtDTreeMap.minKey?_mem
 
+theorem minKey?_eq_min?_keys [TransCmp cmp] [Min α]
+    [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α]
+    [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] :
+    t.minKey? = t.keys.min? :=
+  ExtDTreeMap.minKey?_eq_min?_keys
+
 theorem isSome_minKey?_of_contains [TransCmp cmp] {k} :
     (hc : t.contains k) → t.minKey?.isSome :=
   ExtDTreeMap.isSome_minKey?_of_contains

src/Std/Data/ExtTreeSet/Lemmas.lean

@@ -1062,6 +1062,12 @@ theorem min?_mem [TransCmp cmp] {km} :
     (hkm : t.min? = some km) → km ∈ t :=
   ExtTreeMap.minKey?_mem
 
+theorem min?_eq_min?_toList [TransCmp cmp] [Min α]
+    [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α]
+    [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] :
+    t.min? = t.toList.min? :=
+  ExtDTreeMap.minKey?_eq_min?_keys
+
 theorem isSome_min?_of_contains [TransCmp cmp] {k} :
     (hc : t.contains k) → t.min?.isSome :=
   ExtTreeMap.isSome_minKey?_of_contains

src/Std/Data/Internal/List/Associative.lean

@@ -13,6 +13,8 @@ public import Std.Data.Internal.List.Defs
 import all Std.Data.Internal.List.Defs
 public import Init.Data.Order.Ord
 import Init.Data.Subtype.Order
+public import Init.Data.Order.ClassesExtra
+public import Init.Data.Order.LemmasExtra
 
 public section
 
@@ -8249,6 +8251,29 @@ theorem containsKey_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l
   obtain ⟨e, ⟨hm, _⟩, rfl⟩ := hkm
   exact containsKey_of_mem hm
 
+theorem minKey?_eq_min?_keys [Ord α] [TransOrd α]
+    [LawfulEqOrd α] [LE α] [LawfulOrderOrd α] [Min α]
+    [LawfulOrderLeftLeaningMin α] (l : List ((a : α) × β a)) :
+    minKey? l = (List.keys l).min? := by
+  have : IsLinearOrder α := IsLinearOrder.of_ord
+  rw [keys_eq_map]
+  induction l with
+  | nil => simp [minKey?_of_isEmpty]
+  | cons h t ih =>
+    rw [minKey?, minEntry?_cons, minEntry?, Option.map_some, List.map_cons, List.min?_cons]
+    split
+    · simp only [← ih, minKey?, minEntry?, Option.map_none, Option.elim_none, *]
+    · simp only [Option.some.injEq, ← ih, minKey?, minEntry?, *, min, Option.map_some,
+                 Option.elim_some]
+      split
+      · rw [LawfulOrderLeftLeaningMin.min_eq_left _ _ <|
+            (LawfulOrderOrd.isLE_compare _ _).1 ‹_›]
+      · rename_i w _ hyp
+        simp only [Bool.not_eq_true, Ordering.isLE_eq_false] at hyp
+        simp only [Commutative.comm h.fst w.fst]
+        rw [LawfulOrderLeftLeaningMin.min_eq_left _ _ <|
+            (LawfulOrderOrd.isGE_compare _ _).1 (Ordering.isGE_of_eq_gt hyp)]
+
 theorem minKey?_eraseKey_eq_iff_beq_minKey?_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
     {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
     minKey? (eraseKey k l) = minKey? l ↔ ∀ {km}, minKey? l = some km → (k == km) = false := by

src/Std/Data/TreeMap/Lemmas.lean

@@ -2500,6 +2500,12 @@ theorem minKey?_modify [TransCmp cmp] {k f} :
     (t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
   DTreeMap.Const.minKey?_modify
 
+theorem minKey?_eq_min?_keys [TransCmp cmp] [Min α]
+    [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α]
+    [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] :
+    t.minKey? = t.keys.min? :=
+  DTreeMap.minKey?_eq_min?_keys
+
 @[simp, grind =]
 theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
     (t.modify k f).minKey? = t.minKey? :=

src/Std/Data/TreeMap/Raw/Lemmas.lean

@@ -2547,6 +2547,13 @@ theorem minKey?_modify [TransCmp cmp] (h : t.WF) {k f} :
     (t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
   DTreeMap.Raw.Const.minKey?_modify h
 
+theorem minKey?_eq_min?_keys [TransCmp cmp] [Min α]
+    [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α]
+    [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp]
+    (h : t.WF) :
+    t.minKey? = t.keys.min? :=
+  DTreeMap.Raw.minKey?_eq_min?_keys h
+
 @[simp, grind =]
 theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} :
     (t.modify k f).minKey? = t.minKey? :=

src/Std/Data/TreeSet/Lemmas.lean

@@ -1053,6 +1053,11 @@ theorem min?_eq_none_iff [TransCmp cmp] :
     t.min? = none ↔ t.isEmpty :=
   TreeMap.minKey?_eq_none_iff
 
+theorem min?_eq_min?_toList [TransCmp cmp] [Min α]
+    [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α][LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp] :
+    t.min? = t.toList.min? :=
+  TreeMap.minKey?_eq_min?_keys
+
 theorem min?_eq_some_iff_get?_eq_self_and_forall [TransCmp cmp] {km} :
     t.min? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
   TreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall

src/Std/Data/TreeSet/Raw/Lemmas.lean

@@ -10,6 +10,7 @@ import Std.Data.TreeMap.Raw.Lemmas
 import Std.Data.DTreeMap.Raw.Lemmas
 public import Std.Data.TreeSet.Raw.Basic
 public import Init.Data.List.BasicAux
+public import Init.Data.Order.ClassesExtra
 
 @[expose] public section
 
@@ -1114,6 +1115,13 @@ theorem min?_insert [TransCmp cmp] (h : t.WF) {k} :
       some (t.min?.elim k fun k' => if cmp k k' = .lt then k else k') :=
   TreeMap.Raw.minKey?_insertIfNew h
 
+theorem min?_eq_min?_toList [TransCmp cmp] [Min α]
+    [LE α] [LawfulOrderCmp cmp] [LawfulOrderMin α]
+    [LawfulOrderLeftLeaningMin α] [LawfulEqCmp cmp]
+    (h : t.WF) :
+    t.min? = t.toList.min? :=
+  TreeMap.Raw.minKey?_eq_min?_keys h
+
 theorem isSome_min?_insert [TransCmp cmp] (h : t.WF) {k} :
     (t.insert k).min?.isSome :=
   TreeMap.Raw.isSome_minKey?_insertIfNew h