fixes after rebase

Author: datokrat

src/Std/Data/DHashMap/Internal/AssocList/Iterator.lean

@@ -32,8 +32,8 @@ public instance : Iterator (α := AssocListIterator α β) Id ((a : α) × β a)
     | .skip _ => False
     | .done => it.internalState.l = .nil
   step it := pure (match it with
-        | ⟨⟨.nil⟩⟩ => ⟨.done, rfl⟩
-        | ⟨⟨.cons k v l⟩⟩ => ⟨.yield (toIterM ⟨l⟩ Id _) ⟨k, v⟩, rfl⟩)
+        | ⟨⟨.nil⟩⟩ => .deflate ⟨.done, rfl⟩
+        | ⟨⟨.cons k v l⟩⟩ => .deflate ⟨.yield (toIterM ⟨l⟩ Id _) ⟨k, v⟩, rfl⟩)
 
 def AssocListIterator.finitenessRelation :
     FinitenessRelation (AssocListIterator α β) Id where

src/Std/Data/DHashMap/IteratorLemmas.lean

@@ -22,13 +22,13 @@ open Std.Iterators
 
 @[simp]
 public theorem step_iter_nil {α : Type u} {β : α → Type v} :
-    ((.nil : AssocList α β).iter).step = ⟨.done, rfl⟩ :=
-  (rfl)
+    ((.nil : AssocList α β).iter).step = ⟨.done, rfl⟩ := by
+  simp [Iter.step, IterM.step, Iterator.step, Iter.toIterM, iter]
 
 @[simp]
 public theorem step_iter_cons {α : Type u} {β : α → Type v} {k v} {l : AssocList α β} :
-    ((AssocList.cons k v l).iter).step = ⟨.yield l.iter ⟨k, v⟩, rfl⟩ :=
-  (rfl)
+    ((AssocList.cons k v l).iter).step = ⟨.yield l.iter ⟨k, v⟩, rfl⟩ := by
+  simp [Iter.step, IterM.step, Iterator.step, Iter.toIterM, iter, toIterM, IterM.toIter]
 
 @[simp]
 public theorem toList_iter {α : Type u} {β : α → Type v} {l : AssocList α β} :