theorem Std.IterM.Intermediate.dropWhileM_eq_dropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [MonadAttach m] [Iterator α m β] {it : IterM m β} {P : β → m (ULift Bool)} {dropping : Bool} : dropWhileM P dropping it = dropWhileWithPostcondition (Iterators.PostconditionT.attachLift ∘ P) dropping it

theorem Std.IterM.Intermediate.dropWhile_eq_dropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : β → Bool} {dropping : Bool} : dropWhile P dropping it = dropWhileWithPostcondition (pure ∘ ULift.up ∘ P) dropping it

theorem Std.IterM.dropWhileWithPostcondition_eq_intermediateDropWhileWithPostcondition {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] {it : IterM m β} {P : β → Iterators.PostconditionT m (ULift Bool)} : dropWhileWithPostcondition P it = Intermediate.dropWhileWithPostcondition P true it

theorem Std.IterM.dropWhileM_eq_intermediateDropWhileM {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [MonadAttach m] [Iterator α m β] {it : IterM m β} {P : β → m (ULift Bool)} : dropWhileM P it = Intermediate.dropWhileM P true it

theorem Std.IterM.dropWhile_eq_intermediateDropWhile {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [Iterator α m β] {it : IterM m β} {P : β → Bool} : dropWhile P it = Intermediate.dropWhile P true it

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

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

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

theorem Std.IterM.step_dropWhileM {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] [MonadAttach m] [LawfulMonad m] [Iterator α m β] {it : IterM m β} {P : β → m (ULift Bool)} : (dropWhileM P it).step = do let __do_lift ← it.step match __do_lift.inflate with | ⟨IterStep.yield it' out, h⟩ => do let __do_lift ← MonadAttach.attach (P out) match __do_lift with | ⟨{ down := true }, hP⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ⋯)) | ⟨{ down := false }, hP⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (Intermediate.dropWhileM P false it') out ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (Intermediate.dropWhileM P true it') ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

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

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