more @[simp]

Author: datokrat

src/Std/Data/HashMap/IteratorLemmas.lean

@@ -28,15 +28,18 @@ theorem toList_inner :
   simp [toList, DHashMap.Internal.Raw.Const.toList_eq_toListModel_map,
     ← DHashMap.Internal.Raw.toList_eq_toListModel, Function.comp_def]
 
+@[simp]
 public theorem toList_iter :
     m.iter.toList = m.toList := by
   simp [Raw.iter, Iter.toList_map, DHashMap.Raw.toList_iter, toList_inner,
     Function.comp_def]
 
+@[simp]
 public theorem toListRev_iter :
     m.iter.toListRev = m.toList.reverse := by
   simp [Iter.toListRev_eq, toList_iter]
 
+@[simp]
 public theorem toArray_iter [BEq α] [Hashable α] (h : m.WF) :
     m.iter.toArray = m.toArray := by
   simp [← Iter.toArray_toList, ← Raw.toArray_toList h, toList_iter]
@@ -51,15 +54,18 @@ theorem keys_inner :
     m.inner.keys = m.keys :=
   rfl
 
+@[simp]
 public theorem toList_keysIter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keysIter.toList = m.keys := by
   simp only [keysIter, ← map_fst_toList_eq_keys h, DHashMap.Raw.toList_keysIter h.out]
   simp [HashMap.Raw.map_fst_toList_eq_keys h, keys_inner]
 
+@[simp]
 public theorem toListRev_keysIter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keysIter.toListRev = m.keys.reverse := by
   simp [Iter.toListRev_eq, toList_keysIter h]
 
+@[simp]
 public theorem toArray_keysIter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keysIter.toArray = m.keysArray := by
   simp [← Iter.toArray_toList, ← Raw.toArray_keys h, toList_keysIter h]
@@ -70,16 +76,19 @@ section ValuesIter
 
 variable {α β : Type u} {m : Raw α β}
 
+@[simp]
 public theorem toList_valuesIter_eq_toList_map_snd :
     m.valuesIter.toList = m.toList.map Prod.snd := by
   simp [valuesIter, DHashMap.Raw.toList_valuesIter_eq_toList_map_snd,
     DHashMap.Internal.Raw.toList_eq_toListModel, toList,
     DHashMap.Internal.Raw.Const.toList_eq_toListModel_map]
 
+@[simp]
 public theorem toListRev_valuesIter :
     m.valuesIter.toListRev = (m.toList.map Prod.snd).reverse := by
   simp [Iter.toListRev_eq, toList_valuesIter_eq_toList_map_snd]
 
+@[simp]
 public theorem toArray_valuesIter :
     m.valuesIter.toArray = (m.toList.map Prod.snd).toArray := by
   simp [← Iter.toArray_toList, toList_valuesIter_eq_toList_map_snd]
@@ -100,14 +109,17 @@ theorem toList_inner :
   simp [toList, DHashMap.Const.toList, DHashMap.Internal.Raw.Const.toList_eq_toListModel_map,
     Function.comp_def, DHashMap.toList, DHashMap.Internal.Raw.toList_eq_toListModel]
 
+@[simp]
 public theorem toList_iter :
     m.iter.toList = m.toList := by
   simp [iter, DHashMap.toList_iter, toList_inner, Function.comp_def]
 
+@[simp]
 public theorem toListRev_iter :
     m.iter.toListRev = m.toList.reverse := by
   simp [Iter.toListRev_eq, toList_iter]
 
+@[simp]
 public theorem toArray_iter :
     m.iter.toArray = m.toArray := by
   simp [← Iter.toArray_toList, toList_iter]
@@ -122,14 +134,17 @@ theorem keys_inner {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : HashM
 
 variable {α : Type u} {β : Type u} [BEq α] [Hashable α] {m : HashMap α β}
 
+@[simp]
 public theorem toList_keysIter [EquivBEq α] [LawfulHashable α] :
     m.keysIter.toList = m.keys := by
   simp [keysIter, DHashMap.toList_keysIter, keys_inner]
 
+@[simp]
 public theorem toListRev_keysIter [EquivBEq α] [LawfulHashable α] :
     m.keysIter.toListRev = m.keys.reverse := by
   simp [keysIter, DHashMap.toListRev_keysIter, keys_inner]
 
+@[simp]
 public theorem toArray_keysIter [EquivBEq α] [LawfulHashable α] :
     m.keysIter.toArray = m.keysArray := by
   simp [← Iter.toArray_toList, keysIter, keysArray, DHashMap.toList_keysIter]
@@ -140,14 +155,17 @@ section ValuesIter
 
 variable {α : Type u} {β : Type u} [BEq α] [Hashable α] {m : HashMap α β}
 
+@[simp]
 public theorem toList_valuesIter_eq_toList_map_snd :
     m.valuesIter.toList = m.toList.map Prod.snd := by
   simp [valuesIter, DHashMap.toList_valuesIter_eq_toList_map_snd, toList_inner]
 
+@[simp]
 public theorem toListRev_valuesIter :
     m.valuesIter.toListRev = (m.toList.map Prod.snd).reverse := by
   simp [Iter.toListRev_eq, toList_valuesIter_eq_toList_map_snd]
 
+@[simp]
 public theorem toArray_valuesIter :
     m.valuesIter.toArray = (m.toList.map Prod.snd).toArray := by
   simp [← Iter.toArray_toList, toList_valuesIter_eq_toList_map_snd]

src/Std/Data/HashSet/IteratorLemmas.lean

@@ -22,15 +22,18 @@ open Std.Iterators
 
 variable {α : Type u} {m : Raw α}
 
+@[simp]
 public theorem toList_iter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.iter.toList = m.toList := by
   simp [toList, iter, DHashMap.Raw.toList_iter,
     ← HashMap.Raw.map_fst_toList_eq_keys h.out, HashMap.Raw.toList_inner]
 
+@[simp]
 public theorem toListRev_iter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.iter.toListRev = m.toList.reverse := by
   simp [Iter.toListRev_eq, toList_iter h]
 
+@[simp]
 public theorem toArray_iter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.iter.toArray = m.toArray := by
   simp [← Iter.toArray_toList, ← Raw.toArray_toList h, toList_iter h]
@@ -42,14 +45,17 @@ open Std.Iterators
 
 variable {α : Type u} [BEq α] [Hashable α] {m : HashSet α}
 
+@[simp]
 public theorem toList_iter [EquivBEq α] [LawfulHashable α] :
     m.iter.toList = m.toList := by
   simp [iter, DHashMap.toList_iter, toList, HashMap.keys_inner]
 
+@[simp]
 public theorem toListRev_iter [EquivBEq α] [LawfulHashable α] :
     m.iter.toListRev = m.toList.reverse := by
   simp [iter, DHashMap.toListRev_iter, toList, HashMap.keys_inner]
 
+@[simp]
 public theorem toArray_iter [EquivBEq α] [LawfulHashable α] :
     m.iter.toArray = m.toArray := by
   simp [iter, DHashMap.toArray_iter, toArray, HashMap.keysArray]