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

theorem Std.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.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.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 hP : 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.Iter.val_step_intermediateDropWhile {α β : Type u_1} [Iterator α Id β] {it : Iter β} {P : β → Bool} {dropping : Bool} : (Intermediate.dropWhile P dropping it).step.val = match it.step.val with | IterStep.yield it' out => if dropping = true then match P out with | true => IterStep.skip (Intermediate.dropWhile P true it') | false => IterStep.yield (Intermediate.dropWhile P false it') out else IterStep.yield (Intermediate.dropWhile P false it') out | IterStep.skip it' => IterStep.skip (Intermediate.dropWhile P dropping it') | IterStep.done => IterStep.done

theorem Std.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 hP : 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.Iter.val_step_dropWhile {α β : Type u_1} [Iterator α Id β] {P : β → Bool} {it : Iter β} : (dropWhile P it).step.val = match it.step.val with | IterStep.yield it' out => match P out with | true => IterStep.skip (Intermediate.dropWhile P true it') | false => IterStep.yield (Intermediate.dropWhile P false it') out | IterStep.skip it' => IterStep.skip (Intermediate.dropWhile P true it') | IterStep.done => IterStep.done

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

@[simp]

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

@[simp]

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

@[simp]

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