cleanups

Author: datokrat

src/Std/Data/Iterators/Basic.lean

@@ -234,9 +234,9 @@ An inductive type that makes it easier to apply the `cases` tactic to a
 -/
 inductive PlausibleIterStep.CasesHelper {IsPlausibleStep : IterStep α β → Prop} :
     PlausibleIterStep IsPlausibleStep → Type _ where
-  | yield (it' out h) : CasesHelper (.yield it' out h)
-  | skip (it' h) : CasesHelper (.skip it' h)
-  | done (h) : CasesHelper (.done h)
+  | yield (it' out h) : CasesHelper ⟨.yield it' out, h⟩
+  | skip (it' h) : CasesHelper ⟨.skip it', h⟩
+  | done (h) : CasesHelper ⟨.done, h⟩
 
 /--
 Because `PlausibleIterStep` is a subtype of `IterStep`, it is tedious to use

src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean

@@ -65,8 +65,7 @@ theorem Iter.toArray_of_step {α β} [Iterator α Id β] [Finite α Id] [Iterato
   rw [IterM.toArray_of_step]
   simp only [Id.map_eq, Id.pure_eq, Id.bind_eq, Id.run]
   generalize it.toIterM.step = step
-  obtain ⟨step, h⟩ := step
-  cases step <;> simp
+  cases step.casesHelper <;> simp
 
 theorem Iter.toList_of_step {α β} [Iterator α Id β] [Finite α Id] [IteratorCollect α Id]
     [LawfulIteratorCollect α Id] {it : Iter (α := α) β} :