feat: add minimum_le_coe_iff for List.minimum (#5845)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Data/List/MinMax.lean

@@ -391,6 +391,18 @@ theorem minimum_eq_coe_iff : minimum l = m ↔ m ∈ l ∧ ∀ a ∈ l, m ≤ a
   @maximum_eq_coe_iff αᵒᵈ _ _ _
 #align list.minimum_eq_coe_iff List.minimum_eq_coe_iff
 
+theorem coe_le_maximum_iff : a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b := by
+  induction l with
+  | nil => simp
+  | cons h t ih =>
+    simp [List.maximum_cons, ih]
+
+theorem minimum_le_coe_iff : l.minimum ≤ a ↔ ∃ b, b ∈ l ∧ b ≤ a := by
+  induction l with
+  | nil => simp
+  | cons h t ih =>
+    simp [List.minimum_cons, ih]
+
 end LinearOrder
 
 end MaximumMinimum