chore: address Markus' comments

Author: wkrozowski

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

@@ -61,8 +61,8 @@ public def valuesIter {α : Type u} {β : Type u} {cmp : α → α → Ordering}
   @Raw.valuesIter _ _ cmp  ⟨m.inner⟩
 
 @[simp]
-public theorem iter_toList {cmp : α → α → Ordering} (m : DTreeMap α β cmp) :
-    m.iter.toList = m.toList := Raw.iter_toList ⟨m.inner⟩
+public theorem toList_iter {cmp : α → α → Ordering} (m : DTreeMap α β cmp) :
+    m.iter.toList = m.toList := Raw.toList_iter ⟨m.inner⟩
 
 @[simp]
 public theorem keysIter_toList {cmp : α → α → Ordering} (m : DTreeMap α β cmp) :

src/Std/Data/DTreeMap/Iterator.lean

@@ -63,21 +63,21 @@ public def valuesIter {α : Type u} {β : Type u}
   (m.iter.map fun e => e.2 : Iter β)
 
 @[simp]
-public theorem iter_toList {cmp : α → α → Ordering} (m : Raw α β cmp) :
+public theorem toList_iter {cmp : α → α → Ordering} (m : Raw α β cmp) :
     (m.iter).toList = m.toList := by
   rw [iter, toList]
-  apply Internal.Zipper.toList.iterOfTree
+  apply Internal.Zipper.toList_iterOfTree
 
 @[simp]
 public theorem keysIter_toList {cmp : α → α → Ordering} (m : Raw α β cmp) :
     (m.keysIter).toList = m.keys := by
   rw [keysIter, keys, iter, ← Internal.Impl.map_fst_toList_eq_keys]
-  apply Internal.Zipper.map_iterOfTree_eq_tree_toList_map
+  rw [Iter.toList_map, Internal.Zipper.toList_iterOfTree]
 
 @[simp]
 public theorem valuesIter_toList {cmp : α → α → Ordering} (m : Raw α (fun _ => β) cmp) :
     (m.valuesIter).toList = m.values := by
   rw [valuesIter, values, iter, Internal.Impl.values_eq_map_snd, ← Internal.Impl.toList_eq_toListModel]
-  apply Internal.Zipper.map_iterOfTree_eq_tree_toList_map
+  rw [Iter.toList_map, Internal.Zipper.toList_iterOfTree]
 
 end Std.DTreeMap.Raw

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

@@ -82,7 +82,7 @@ public instance {α : Type u} {β : α → Type v} (cmp : α → α → Ordering
 
 @[simp] public theorem toList_roi {α : Type u} {β : α → Type v}
     (cmp : α → α → Ordering := by exact compare) [TransCmp cmp]
-    {t : DTreeMap α β cmp} {bound : α} :t[bound<...*].toList =
+    {t : DTreeMap α β cmp} {bound : α} : t[bound<...*].toList =
       t.toList.filter (fun e => (cmp e.fst bound).isGT) :=
   @Internal.toList_roi α β ⟨cmp⟩ _ t.inner (@t.wf.ordered α β ⟨cmp⟩ _) bound
 

src/Std/Data/DTreeMap/Slice.lean

@@ -63,9 +63,9 @@ public def valuesIter {α : Type u} {β : Type u} {cmp : α → α → Ordering}
   m.inner.valuesIter
 
 @[simp]
-public theorem iter_toList {cmp : α → α → Ordering} (m : TreeMap α β cmp) :
+public theorem toList_iter {cmp : α → α → Ordering} (m : TreeMap α β cmp) :
     m.iter.toList = m.toList := by
-  simp only [iter, Iter.toList_map, DTreeMap.iter_toList, DTreeMap.toList,
+  simp only [iter, Iter.toList_map, DTreeMap.toList_iter, DTreeMap.toList,
     DTreeMap.Internal.Impl.toList_eq_toListModel, toList, DTreeMap.Const.toList,
     DTreeMap.Internal.Impl.Const.toList_eq_toListModel_map]
 

src/Std/Data/TreeMap/Iterator.lean

@@ -63,9 +63,9 @@ public def valuesIter {α : Type u} {β : Type u}
   (m.inner.valuesIter : Iter β)
 
 @[simp]
-public theorem iter_toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} (m : Raw α β cmp) :
+public theorem toList_iter {α : Type u} {β : Type v} {cmp : α → α → Ordering} (m : Raw α β cmp) :
     (m.iter.toList) = m.toList := by
-  simp only [iter, Iter.toList_map, DTreeMap.Raw.iter_toList]
+  simp only [iter, Iter.toList_map, DTreeMap.Raw.toList_iter]
   simp only [DTreeMap.Raw.toList, DTreeMap.Internal.Impl.toList_eq_toListModel, toList,
     DTreeMap.Raw.Const.toList, DTreeMap.Internal.Impl.Const.toList_eq_toListModel_map]
 

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

@@ -35,7 +35,7 @@ public theorem toList_ric {α : Type u} {β : Type v} (cmp : α → α → Order
     [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound : α} :
     t[*...=bound].toList = t.toList.filter (fun e => (cmp e.fst bound).isLE) := by
   apply @DTreeMap.Internal.Const.toList_ric _ _ ⟨cmp⟩ _ _
-  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+  · exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
 public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
     Rio.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RioSlice α β ⟨cmp⟩) :=
@@ -45,7 +45,7 @@ public theorem toList_rio {α : Type u} {β : Type v} (cmp : α → α → Order
     [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound : α} :
     t[*...<bound].toList = t.toList.filter (fun e => (cmp e.fst bound).isLT) := by
   apply @DTreeMap.Internal.Const.toList_rio _ _ ⟨cmp⟩ _ _
-  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+  · exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
 public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
     Rci.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RciSlice α β ⟨cmp⟩) :=
@@ -55,7 +55,7 @@ public theorem toList_rci {α : Type u} {β : Type v} (cmp : α → α → Order
     [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound : α} :
     t[bound...*].toList = t.toList.filter (fun e => (cmp e.fst bound).isGE) := by
   apply @DTreeMap.Internal.Const.toList_rci _ _ ⟨cmp⟩ _ _
-  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+  · exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
 public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
     Rco.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RcoSlice α β ⟨cmp⟩) :=
@@ -66,7 +66,7 @@ public theorem toList_rco {α : Type u} {β : Type v} (cmp : α → α → Order
     t[lowerBound...<upperBound].toList =
       t.toList.filter (fun e => (cmp e.fst lowerBound).isGE ∧ (cmp e.fst upperBound).isLT) := by
   apply @DTreeMap.Internal.Const.toList_rco _ _ ⟨cmp⟩ _ _
-  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+  · exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
 public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
     Rcc.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RccSlice α β ⟨cmp⟩) :=
@@ -77,7 +77,7 @@ public theorem toList_rcc {α : Type u} {β : Type v} (cmp : α → α → Order
     t[lowerBound...=upperBound].toList =
       t.toList.filter (fun e => (cmp e.fst lowerBound).isGE ∧ (cmp e.fst upperBound).isLE) := by
   apply @DTreeMap.Internal.Const.toList_rcc _ _ ⟨cmp⟩ _ _
-  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+  · exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
 public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
     Roi.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RoiSlice α β ⟨cmp⟩) :=
@@ -87,7 +87,7 @@ public theorem toList_roi {α : Type u} {β : Type v} (cmp : α → α → Order
     [TransCmp cmp] {t : Raw α β cmp} {wf : t.WF} {bound: α} : t[bound<...*].toList =
       t.toList.filter (fun e => (cmp e.fst bound).isGT) := by
   apply @DTreeMap.Internal.Const.toList_roi _ _ ⟨cmp⟩ _
-  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+  · exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
 public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
     Roc.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RocSlice α β ⟨cmp⟩) :=
@@ -98,7 +98,7 @@ public theorem toList_roc {α : Type u} {β : Type v} (cmp : α → α → Order
     t[lowerBound<...=upperBound].toList =
       t.toList.filter (fun e => (cmp e.fst lowerBound).isGT ∧ (cmp e.fst upperBound).isLE) := by
   apply @DTreeMap.Internal.Const.toList_roc _ _ ⟨cmp⟩ _
-  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+  · exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
 public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) :
     Roo.Sliceable (Raw α β cmp) α (@DTreeMap.Internal.Const.RooSlice α β ⟨cmp⟩) :=
@@ -109,6 +109,6 @@ public theorem toList_roo {α : Type u} {β : Type v} (cmp : α → α → Order
     t[lowerBound<...upperBound].toList =
       t.toList.filter (fun e => (cmp e.fst lowerBound).isGT ∧ (cmp e.fst upperBound).isLT) := by
   apply @DTreeMap.Internal.Const.toList_roo _ _ ⟨cmp⟩ _
-  . exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
+  · exact @wf.out.out.ordered _ _ ⟨cmp⟩ _
 
 end Std.TreeMap.Raw

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

@@ -83,7 +83,7 @@ public instance {α : Type u} {β : Type v} (cmp : α → α → Ordering := by
 
 @[simp] public theorem toList_roi {α : Type u} {β : Type v}
     (cmp : α → α → Ordering := by exact compare) [TransCmp cmp]
-    {t : TreeMap α β cmp} {bound : α} :t[bound<...*].toList =
+    {t : TreeMap α β cmp} {bound : α} : t[bound<...*].toList =
       t.toList.filter (fun e => (cmp e.fst bound).isGT) :=
   @DTreeMap.Internal.Const.toList_roi α β ⟨cmp⟩ _ t.inner.inner (@t.inner.wf.ordered α (fun _ => β) ⟨cmp⟩ _) bound
 

src/Std/Data/TreeMap/Slice.lean

@@ -32,8 +32,8 @@ public def iter {α : Type u}
   (m.inner.iter.map fun e => e.1 : Iter α)
 
 @[simp]
-public theorem iter_toList {cmp : α → α → Ordering} (m : TreeSet α cmp) :
+public theorem toList_iter {cmp : α → α → Ordering} (m : TreeSet α cmp) :
     m.iter.toList = m.toList := by
-  rw [iter, Iter.toList_map, TreeMap.iter_toList, toList, TreeMap.toList, TreeMap.keys, Std.DTreeMap.Const.map_fst_toList_eq_keys]
+  rw [iter, Iter.toList_map, TreeMap.toList_iter, toList, TreeMap.toList, TreeMap.keys, Std.DTreeMap.Const.map_fst_toList_eq_keys]
 
 end Std.TreeSet

src/Std/Data/TreeSet/Iterator.lean

@@ -32,9 +32,9 @@ public def iter {α : Type u}
   (m.inner.iter.map fun e => e.1 : Iter α)
 
 @[simp]
-public theorem iter_toList {cmp : α → α → Ordering} (m : Raw α cmp) :
+public theorem toList_iter {cmp : α → α → Ordering} (m : Raw α cmp) :
     m.iter.toList = m.toList := by
-  rw [iter, Iter.toList_map, TreeMap.Raw.iter_toList, TreeMap.Raw.toList]
+  rw [iter, Iter.toList_map, TreeMap.Raw.toList_iter, TreeMap.Raw.toList]
   rw [TreeSet.Raw.toList]
   rw [Std.DTreeMap.Internal.Impl.foldr_eq_foldr_toList]
   simp only [DTreeMap.Raw.Const.map_fst_toList_eq_keys, List.empty_eq, List.foldr_cons_eq_append,