chore: typesetting

Author: wkrozowski

src/Init/Data/Order/LemmasExtra.lean

@@ -147,7 +147,7 @@ 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]
 
-theorem min_le_min [LE α] [Min α] [Std.LawfulOrderLeftLeaningMin α] [IsLinearOrder α] (a b : α) : min a b ≤ min b a := by
+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

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

@@ -6136,7 +6136,10 @@ 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 α] [Std.LawfulOrderOrd α] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α] [LawfulEqOrd α] (h : t.WF) :
+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
 

src/Std/Data/DTreeMap/Lemmas.lean

@@ -3690,7 +3690,8 @@ 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] :
+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
 

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

@@ -3847,7 +3847,10 @@ 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) :
+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
 

src/Std/Data/ExtDTreeMap/Lemmas.lean

@@ -3799,7 +3799,9 @@ 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] :
+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
 

src/Std/Data/ExtTreeMap/Lemmas.lean

@@ -2344,7 +2344,9 @@ 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] :
+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
 

src/Std/Data/ExtTreeSet/Lemmas.lean

@@ -1062,7 +1062,9 @@ 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] :
+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
 

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

@@ -8250,8 +8250,9 @@ 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 α] [Std.LawfulEqOrd α] [LE α] [Std.LawfulOrderOrd α] [Min α] [Std.LawfulOrderLeftLeaningMin α]
-    (l : List ((a : α) × β a)) :
+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]
@@ -8270,7 +8271,7 @@ theorem minKey?_eq_min?_keys [Ord α] [TransOrd α] [Std.LawfulEqOrd α] [LE α]
         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 ‹_›)]
+            (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) :

src/Std/Data/TreeMap/Lemmas.lean

@@ -2500,7 +2500,9 @@ 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] :
+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
 

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

@@ -2547,7 +2547,10 @@ 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) :
+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