∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)},
  (Std.IterM.dropWhileWithPostcondition P it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← (P out).operation
        match __do_lift with
          | ⟨{ down := true }, h''⟩ =>
            pure
              (Std.Shrink.deflate
                (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileWithPostcondition P true it') ⋯))
          | ⟨{ down := false }, h''⟩ =>
            pure
              (Std.Shrink.deflate
                (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhileWithPostcondition P false it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure
          (Std.Shrink.deflate
            (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileWithPostcondition P true it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))