theorem Std.Iterators.Iter.dropWhile_eq_intermediateDropWhile {α β : Type u_1} [Iterator α Id β] {P : β → Bool} {it : Iter β} : dropWhile P it = Intermediate.dropWhile P true it

theorem Std.Iterators.Iter.Intermediate.dropWhile_eq_dropWhile_toIterM {α β : Type u_1} [Iterator α Id β] {P : β → Bool} {it : Iter β} {dropping : Bool} : dropWhile P dropping it = (IterM.Intermediate.dropWhile P dropping it.toIterM).toIter

theorem Std.Iterators.Iter.dropWhile_eq_dropWhile_toIterM {α β : Type u_1} [Iterator α Id β] {P : β → Bool} {it : Iter β} : dropWhile P it = (IterM.dropWhile P it.toIterM).toIter

theorem Std.Iterators.Iter.step_intermediateDropWhile {α β : Type u_1} [Iterator α Id β] {it : Iter β} {P : β → Bool} {dropping : Bool} : (Intermediate.dropWhile P dropping it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => if h' : dropping = true then match P out with | true => PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯ | false => PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯ else PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (Intermediate.dropWhile P dropping it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

theorem Std.Iterators.Iter.step_dropWhile {α β : Type u_1} [Iterator α Id β] {P : β → Bool} {it : Iter β} : (dropWhile P it).step = match it.step with | ⟨IterStep.yield it' out, h⟩ => match P out with | true => PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯ | false => PlausibleIterStep.yield (Intermediate.dropWhile P false it') out ⋯ | ⟨IterStep.skip it', h⟩ => PlausibleIterStep.skip (Intermediate.dropWhile P true it') ⋯ | ⟨IterStep.done, h⟩ => PlausibleIterStep.done ⋯

theorem Std.Iterators.Iter.toList_intermediateDropWhile_of_finite {α β : Type u_1} [Iterator α Id β] {P : β → Bool} {dropping : Bool} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (Intermediate.dropWhile P dropping it).toList = if dropping = true then List.dropWhile P it.toList else it.toList

@[simp]

theorem Std.Iterators.Iter.toList_dropWhile_of_finite {α β : Type u_1} [Iterator α Id β] {P : β → Bool} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (dropWhile P it).toList = List.dropWhile P it.toList

@[simp]

theorem Std.Iterators.Iter.toArray_dropWhile_of_finite {α β : Type u_1} [Iterator α Id β] {P : β → Bool} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (dropWhile P it).toArray = (List.dropWhile P it.toList).toArray

@[simp]

theorem Std.Iterators.Iter.toListRev_dropWhile_of_finite {α β : Type u_1} [Iterator α Id β] {P : β → Bool} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} : (dropWhile P it).toListRev = (List.dropWhile P it.toList).reverse