∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → Bool} {dropping : Bool},
  (Std.IterM.Intermediate.dropWhile P dropping it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        if h' : dropping = true then
          match hP : P out with
          | true =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhile P true it') ⋯))
          | false =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhile P false it') out ⋯))
        else
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhile P false it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhile P dropping it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))